From 43ace4d856470a37d1e58510c3f2c2aa3a3545f8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 31 Aug 2023 12:53:15 +0100 Subject: [PATCH 1/3] addresses #2075: removal of symmetry assumption --- CHANGELOG.md | 27 +++++++++++++++++++ .../Product/Relation/Binary/Lex/Strict.agda | 15 ++++++----- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 4 +-- src/Induction/WellFounded.agda | 13 +++++---- 4 files changed, 45 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9e34dba19a..57ee69aa38 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -781,6 +781,28 @@ Non-backwards compatible changes properties about the orderings themselves the second index must be provided explicitly. +* Issue #2075 (Johannes Waldmann): wellfoundedness of the lexicographic ordering + on products, defined in `Data.Product.Relation.Binary.Lex.Strict`, no longer + requires the assumption of symmetry for the first equality relation `_≈₁_`, + and so the type of the auxiliary proof `×-wellFounded'` now reads: + ```agda + ×-wellFounded' : Transitive _≈₁_ → + _<₁_ Respectsʳ _≈₁_ → + WellFounded _<₁_ → + WellFounded _<₂_ → + WellFounded _<ₗₑₓ_ + ``` + leading to: + upstream requirement for a new lemma in `Induction.WellFounded` with weaker assumptions; + downstream consequence for `Data.Vec.Relation.Binary.Lex.Strict.<-wellFounded`, + with change of type to: + ```agda + <-wellFounded : (≈-trans : Transitive _≈_) → + (≺-respʳ : _≺_ Respectsʳ _≈_ ) → + (≺-wf : WellFounded _≺_) → + ∀ {n} → WellFounded (_<_ {n}) + ``` + * The operation `SymClosure` on relations in `Relation.Binary.Construct.Closure.Symmetric` has been reimplemented as a data type `SymClosure _⟶_ a b` that is parameterized by the @@ -3354,6 +3376,11 @@ This is a full list of proofs that have changed form to use irrelevant instance ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys ``` +* Added new proof to `Induction.WellFounded` + ```agda + Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_ + ``` + * Added new file `Relation.Binary.Reasoning.Base.Apartness` This is how to use it: diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index d0a09fa4ac..97a3d5bd46 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -186,12 +186,12 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ private _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_ - ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → + ×-wellFounded' : Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ - ×-wellFounded' sym trans resp wf₁ wf₂ (x , y) = acc (×-acc (wf₁ x) (wf₂ y)) + ×-wellFounded' trans resp wf₁ wf₂ (x , y) = acc (×-acc (wf₁ x) (wf₂ y)) where ×-acc : ∀ {x y} → Acc _<₁_ x → Acc _<₂_ y → @@ -199,10 +199,11 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u Date: Thu, 31 Aug 2023 13:48:16 +0100 Subject: [PATCH 2/3] simplified `CHANGELOG` --- CHANGELOG.md | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 57ee69aa38..b994002de6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -784,24 +784,8 @@ Non-backwards compatible changes * Issue #2075 (Johannes Waldmann): wellfoundedness of the lexicographic ordering on products, defined in `Data.Product.Relation.Binary.Lex.Strict`, no longer requires the assumption of symmetry for the first equality relation `_≈₁_`, - and so the type of the auxiliary proof `×-wellFounded'` now reads: - ```agda - ×-wellFounded' : Transitive _≈₁_ → - _<₁_ Respectsʳ _≈₁_ → - WellFounded _<₁_ → - WellFounded _<₂_ → - WellFounded _<ₗₑₓ_ - ``` - leading to: - upstream requirement for a new lemma in `Induction.WellFounded` with weaker assumptions; - downstream consequence for `Data.Vec.Relation.Binary.Lex.Strict.<-wellFounded`, - with change of type to: - ```agda - <-wellFounded : (≈-trans : Transitive _≈_) → - (≺-respʳ : _≺_ Respectsʳ _≈_ ) → - (≺-wf : WellFounded _≺_) → - ∀ {n} → WellFounded (_<_ {n}) - ``` + leading to a new lemma `Induction.WellFounded.Acc-resp-flip-≈`, and refactoring + of the previous proof `Induction.WellFounded.Acc-resp-≈`. * The operation `SymClosure` on relations in `Relation.Binary.Construct.Closure.Symmetric` has been reimplemented @@ -2535,13 +2519,13 @@ Other minor changes ×-≡,≡←≡ : p₁ ≡ p₂ → (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ``` -* Added new proof to `Data.Product.Relation.Binary.Lex.Strict` +* Added new proofs to `Data.Product.Relation.Binary.Lex.Strict` ```agda ×-respectsʳ : Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ - ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → + ×-wellFounded' : Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ ``` @@ -2706,7 +2690,7 @@ Other minor changes ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_ <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ → ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_ - <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → + <-wellFounded : Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → ∀ {n} → WellFounded (_<_ {n}) ``` From b3e653f0a2d73450fcd57454182a34da9755df96 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 31 Aug 2023 17:33:37 +0100 Subject: [PATCH 3/3] tidying up redundant whitespace/parentheses --- src/Data/Product/Relation/Binary/Lex/Strict.agda | 8 ++++---- src/Induction/WellFounded.agda | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index 97a3d5bd46..1a13bdb228 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -22,7 +22,7 @@ open import Level open import Relation.Nullary.Decidable open import Relation.Binary open import Relation.Binary.Consequences -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) private variable @@ -198,10 +198,10 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y) ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u