From 5619f17b4a2d22c1da649591f412f68322873790 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 21 Jun 2025 15:46:14 +0100 Subject: [PATCH 01/22] add: lemmas for decidable equality on `Fin`, plus backport to `Nat` --- CHANGELOG.md | 13 ++++++++++++- src/Data/Fin/Properties.agda | 13 ++++++++++++- src/Data/Nat/Properties.agda | 3 +++ 3 files changed, 27 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a75fdaee8..16e8093aa8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -237,13 +237,19 @@ Additions to existing modules ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b ``` +* In `Data.Fin.Properties`: + ```agda + ≡-irrelevant : Irrelevant {A = Fin n} _≡_ + ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq + ≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl + ``` + * In `Data.Fin.Subset`: ```agda _⊇_ : Subset n → Subset n → Set _⊉_ : Subset n → Subset n → Set _⊃_ : Subset n → Subset n → Set _⊅_ : Subset n → Subset n → Set - ``` * In `Data.Fin.Subset.Induction`: @@ -278,6 +284,11 @@ Additions to existing modules filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys ``` +* In `Data.Nat.Properties`: + ```agda + ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl + ``` + * In `Data.Product.Function.Dependent.Propositional`: ```agda Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index e1f2d25d24..c5dffe54a9 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -11,6 +11,7 @@ module Data.Fin.Properties where open import Axiom.Extensionality.Propositional +open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP) open import Algebra.Definitions using (Involutive) open import Effect.Applicative using (RawApplicative) open import Effect.Functor using (RawFunctor) @@ -44,10 +45,11 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_) open import Relation.Binary.PropositionalEquality.Properties as ≡ using (module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality using (≡-≟-identity) open import Relation.Nullary.Decidable as Dec using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Nullary.Reflects using (Reflects; invert) +open import Relation.Nullary.Reflects using (invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) open import Relation.Unary.Properties using (U?) @@ -100,6 +102,15 @@ zero ≟ suc y = no λ() suc x ≟ zero = no λ() suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) +≡-irrelevant : Irrelevant {A = Fin n} _≡_ +≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ + +≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq +≟-diag = ≡-≟-identity _≟_ + +≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl +≟-diag-refl _ = ≟-diag refl + ------------------------------------------------------------------------ -- Structures diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 5cadc91273..309d530257 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -110,6 +110,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq ≟-diag = ≡-≟-identity _≟_ +≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl +≟-diag-refl _ = ≟-diag refl + ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) ≡-isDecEquivalence = record { isEquivalence = isEquivalence From 84c94202277315cdb015f450496267f8d5cf2073 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 21 Jun 2025 15:46:43 +0100 Subject: [PATCH 02/22] refactor: knock-ons --- src/Data/Fin/Permutation.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 794b93f76b..885dfdfac4 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) open import Data.Fin.Patterns using (0F) open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn; - punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0) + punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; ≟-diag-refl) import Data.Fin.Permutation.Components as PC open import Data.Nat.Base using (ℕ; suc; zero) open import Data.Product.Base using (_,_; proj₂) @@ -197,7 +197,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ k with i ≟ k - ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k + ... | yes i≡k rewrite ≟-diag-refl j = i≡k ... | no i≢k with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k @@ -210,7 +210,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ k with j ≟ k - ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k + ... | yes j≡k rewrite ≟-diag-refl i = j≡k ... | no j≢k with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k From 8ad7b41febb166ec94dda6fdd26a0e9c6b497201 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 21 Jun 2025 15:53:38 +0100 Subject: [PATCH 03/22] fix: `import`s --- src/Data/Fin/Permutation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 885dfdfac4..20d0a7ca3f 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -26,7 +26,7 @@ open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Nullary using (does; ¬_; yes; no) -open import Relation.Nullary.Decidable using (dec-yes; dec-no) +open import Relation.Nullary.Decidable using (dec-no) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂) From c781fc18e2269c72854fc954f444b9e23c7e8eb9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 08:46:29 +0100 Subject: [PATCH 04/22] tighten up --- src/Data/Fin/Properties.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index c5dffe54a9..6610ca2d3b 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -45,7 +45,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_) open import Relation.Binary.PropositionalEquality.Properties as ≡ using (module ≡-Reasoning) -open import Relation.Binary.PropositionalEquality using (≡-≟-identity) +open import Relation.Binary.PropositionalEquality as ≡ + using (≡-≟-identity) open import Relation.Nullary.Decidable as Dec using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Negation.Core using (¬_; contradiction) From 5279af11bb5fce3d4fa4b85552fe78a910d72572 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 08:47:59 +0100 Subject: [PATCH 05/22] refactor: add new lemmas, simplify old proof --- CHANGELOG.md | 8 ++++ src/Data/Fin/Permutation/Components.agda | 49 ++++++++++++++---------- 2 files changed, 36 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 16e8093aa8..49071c07cb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -237,6 +237,14 @@ Additions to existing modules ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b ``` +* In `Data.Fin.Permutation.Components`: + ```agda + transpose-iij : (i j : Fin n) → transpose i i j ≡ j + transpose-ijj : (i j : Fin n) → transpose i j j ≡ i + transpose-iji : (i j : Fin n) → transpose i j i ≡ j + transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k + ``` + * In `Data.Fin.Properties`: ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index 2d2f34deb7..6a4ad9e6b9 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -11,25 +11,18 @@ module Data.Fin.Permutation.Components where open import Data.Bool.Base using (Bool; true; false) open import Data.Fin.Base using (Fin; suc; opposite; toℕ) open import Data.Fin.Properties - using (_≟_; opposite-prop; opposite-involutive; opposite-suc) -open import Data.Nat.Base as ℕ using (zero; suc; _∸_) -open import Data.Product.Base using (proj₂) -open import Function.Base using (_∘_) + using (_≟_; ≟-diag; ≟-diag-refl + ; opposite-prop; opposite-involutive; opposite-suc) open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary using (does; _because_; yes; no) -open import Relation.Nullary.Decidable using (dec-true; dec-false) +open import Relation.Nullary.Decidable.Core using (does; _because_) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; sym; trans) -open import Relation.Binary.PropositionalEquality.Properties - using (module ≡-Reasoning) -open import Algebra.Definitions using (Involutive) -open ≡-Reasoning + using (_≡_; refl; sym) ------------------------------------------------------------------------ -- Functions ------------------------------------------------------------------------ --- 'tranpose i j' swaps the places of 'i' and 'j'. +-- 'transpose i j' swaps the places of 'i' and 'j'. transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n transpose i j k with does (k ≟ i) @@ -42,17 +35,31 @@ transpose i j k with does (k ≟ i) -- Properties ------------------------------------------------------------------------ +transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j +transpose-iij i j with j ≟ i in j≟i +... | true because [j≡i] = sym (invert [j≡i]) +... | false because _ rewrite j≟i = refl + +transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i +transpose-ijj i j with j ≟ i +... | true because [j≡i] = invert [j≡i] +... | false because _ rewrite ≟-diag-refl j = refl + +transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j +transpose-iji i j rewrite ≟-diag-refl i = refl + +transpose-transpose : ∀ {n} {i j k l : Fin n} → + transpose i j k ≡ l → transpose j i l ≡ k +transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i +... | true because [k≡i] rewrite ≟-diag (sym eq) = sym (invert [k≡i]) +... | false because [k≢i] with k ≟ j in k≟j +... | true because [k≡j] rewrite eq | transpose-ijj j l = sym (invert [k≡j]) +... | false because [k≢j] rewrite eq | k≟j | k≟i = refl + transpose-inverse : ∀ {n} (i j : Fin n) {k} → transpose i j (transpose j i k) ≡ k -transpose-inverse i j {k} with k ≟ j -... | true because [k≡j] rewrite dec-true (i ≟ i) refl = sym (invert [k≡j]) -... | false because [k≢j] with k ≟ i -... | true because [k≡i] - rewrite dec-false (j ≟ i) (invert [k≢j] ∘ trans (invert [k≡i]) ∘ sym) - | dec-true (j ≟ j) refl - = sym (invert [k≡i]) -... | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i]) - | dec-false (k ≟ j) (invert [k≢j]) = refl +transpose-inverse i j = transpose-transpose refl + ------------------------------------------------------------------------ -- DEPRECATED NAMES From 61da9a62b98dacde5736b6fca8b8692fb22a3a75 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 10:52:03 +0100 Subject: [PATCH 06/22] refactor: additional instantiated lemmas --- CHANGELOG.md | 1 + src/Data/Fin/Properties.agda | 6 +++++- src/Data/Nat/Properties.agda | 3 +++ 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 49071c07cb..f94f1434a5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -250,6 +250,7 @@ Additions to existing modules ≡-irrelevant : Irrelevant {A = Fin n} _≡_ ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq ≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl + ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j ``` * In `Data.Fin.Subset`: diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 6610ca2d3b..ba3a534f1d 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -46,7 +46,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡ open import Relation.Binary.PropositionalEquality.Properties as ≡ using (module ≡-Reasoning) open import Relation.Binary.PropositionalEquality as ≡ - using (≡-≟-identity) + using (≡-≟-identity; ≢-≟-identity) open import Relation.Nullary.Decidable as Dec using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′) open import Relation.Nullary.Negation.Core using (¬_; contradiction) @@ -112,6 +112,10 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) ≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl ≟-diag-refl _ = ≟-diag refl +≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j +≟-off-diag = ≢-≟-identity _≟_ + + ------------------------------------------------------------------------ -- Structures diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 309d530257..3e93abcfb5 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -113,6 +113,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl ≟-diag-refl _ = ≟-diag refl +≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n +≟-off-diag = ≢-≟-identity _≟_ + ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) ≡-isDecEquivalence = record { isEquivalence = isEquivalence From 5c1c29e2b09f63a8200215e35e48daa2e202cf14 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 10:57:41 +0100 Subject: [PATCH 07/22] refactor: further streamlining of proofs and `import`s --- src/Data/Fin/Permutation.agda | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 20d0a7ca3f..63fbff0bf7 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -11,11 +11,13 @@ module Data.Fin.Permutation where open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) open import Data.Fin.Patterns using (0F) -open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn; - punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; ≟-diag-refl) +open import Data.Fin.Properties + using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag + ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut + ; punchOut-cong; punchOut-cong′) import Data.Fin.Permutation.Components as PC open import Data.Nat.Base using (ℕ; suc; zero) -open import Data.Product.Base using (_,_; proj₂) +open import Data.Product.Base using (_,_) open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′) open import Function.Construct.Composition using (_↔-∘_) open import Function.Construct.Identity using (↔-id) @@ -25,9 +27,8 @@ open import Function.Properties.Inverse using (↔⇒↣) open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) -open import Relation.Nullary using (does; ¬_; yes; no) -open import Relation.Nullary.Decidable using (dec-no) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Decidable.Core using (does; yes; no) +open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂) open import Relation.Binary.PropositionalEquality.Properties @@ -200,7 +201,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ ... | yes i≡k rewrite ≟-diag-refl j = i≡k ... | no i≢k with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym - rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k + rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k = begin punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ @@ -213,7 +214,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ ... | yes j≡k rewrite ≟-diag-refl i = j≡k ... | no j≢k with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym - rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k + rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k = begin punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ @@ -296,9 +297,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j π ⟨$⟩ʳ j ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π -remove-insert i j π k with i ≟ i -... | no i≢i = contradiction refl i≢i -... | yes _ = begin +remove-insert i j π k rewrite ≟-diag-refl i = begin punchOut {i = j} _ ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩ punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) From 1df6eef74431c07a7b242bb34de592825eb7a78e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 10:58:49 +0100 Subject: [PATCH 08/22] `CHANGELOG` --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f94f1434a5..66fc571ede 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -250,7 +250,7 @@ Additions to existing modules ≡-irrelevant : Irrelevant {A = Fin n} _≡_ ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq ≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j + ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j ``` * In `Data.Fin.Subset`: @@ -296,6 +296,7 @@ Additions to existing modules * In `Data.Nat.Properties`: ```agda ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl + ≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n ``` * In `Data.Product.Function.Dependent.Propositional`: From 4f4be18607e7d8c1f2bb0e80995d8bae2b5ba84e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 22 Jun 2025 11:33:47 +0100 Subject: [PATCH 09/22] whitespace --- src/Data/Fin/Properties.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index ba3a534f1d..846a3ba8c0 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -115,7 +115,6 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j ≟-off-diag = ≢-≟-identity _≟_ - ------------------------------------------------------------------------ -- Structures From 842a3bbb98a932fab4f2e5181a9e6346de6ccb38 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Jun 2025 10:35:30 +0100 Subject: [PATCH 10/22] fix: #2743 --- src/Data/Fin/Permutation/Components.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index 6a4ad9e6b9..4f38ab0da6 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -76,20 +76,20 @@ Please use opposite from Data.Fin.Base instead." #-} reverse-prop = opposite-prop -{-# WARNING_ON_USAGE reverse +{-# WARNING_ON_USAGE reverse-prop "Warning: reverse-prop was deprecated in v2.0. Please use opposite-prop from Data.Fin.Properties instead." #-} reverse-involutive = opposite-involutive -{-# WARNING_ON_USAGE reverse +{-# WARNING_ON_USAGE reverse-involutive "Warning: reverse-involutive was deprecated in v2.0. Please use opposite-involutive from Data.Fin.Properties instead." #-} reverse-suc : ∀ {n} {i : Fin n} → toℕ (opposite (suc i)) ≡ toℕ (opposite i) reverse-suc {i = i} = opposite-suc i -{-# WARNING_ON_USAGE reverse +{-# WARNING_ON_USAGE reverse-suc "Warning: reverse-suc was deprecated in v2.0. Please use opposite-suc from Data.Fin.Properties instead." #-} From 5373f2f7502ac417772ead86ee67f551da2d7c2c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Jun 2025 10:56:19 +0100 Subject: [PATCH 11/22] fix: deprecation bug --- src/Data/Fin/Permutation.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 63fbff0bf7..359e96f745 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -13,6 +13,7 @@ open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) open import Data.Fin.Patterns using (0F) open import Data.Fin.Properties using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag + ; opposite-involutive ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut ; punchOut-cong; punchOut-cong′) import Data.Fin.Permutation.Components as PC @@ -98,7 +99,7 @@ transpose i j = permutation (PC.transpose i j) (PC.transpose j i) (λ _ → PC.t -- Reverse the order of indices reverse : Permutation′ n -reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involutive +reverse = permutation opposite opposite opposite-involutive opposite-involutive ------------------------------------------------------------------------ -- Operations From e966871038ad15744fc479923777ae67d38433f8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Jun 2025 11:42:37 +0100 Subject: [PATCH 12/22] fix: equational reaosning layout --- src/Data/Fin/Permutation.agda | 74 +++++++++++++++++++++++------------ 1 file changed, 48 insertions(+), 26 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 359e96f745..dface3cf2a 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -147,19 +147,27 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ j = begin - from (to j) ≡⟨⟩ - punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ - punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩ - punchOut {i = i} {punchIn i j} _ ≡⟨ punchOut-punchIn i ⟩ - j ∎ + from (to j) + ≡⟨⟩ + punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ + ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ + punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ + ≡⟨ punchOut-cong i (inverseˡ π) ⟩ + punchOut {i = i} {punchIn i j} _ + ≡⟨ punchOut-punchIn i ⟩ + j ∎ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ j = begin - to (from j) ≡⟨⟩ - punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ - punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ - punchOut {i = πʳ i} {punchIn (πʳ i) j} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩ - j ∎ + to (from j) + ≡⟨⟩ + punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ + ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ + punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ + ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ + punchOut {i = πʳ i} {punchIn (πʳ i) j} _ + ≡⟨ punchOut-punchIn (πʳ i) ⟩ + j ∎ -- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n) -- by mapping 0 to 0 and applying the input permutation to everything else @@ -204,11 +212,15 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k = begin - punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ - punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ - punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k)) ≡⟨ cong (punchIn i) (inverseˡ π) ⟩ - punchIn i (punchOut i≢k) ≡⟨ punchIn-punchOut i≢k ⟩ - k ∎ + punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) + ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ + punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) + ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ + punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k)) + ≡⟨ cong (punchIn i) (inverseˡ π) ⟩ + punchIn i (punchOut i≢k) + ≡⟨ punchIn-punchOut i≢k ⟩ + k ∎ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ k with j ≟ k @@ -217,11 +229,15 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k = begin - punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ - punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ - punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k)) ≡⟨ cong (punchIn j) (inverseʳ π) ⟩ - punchIn j (punchOut j≢k) ≡⟨ punchIn-punchOut j≢k ⟩ - k ∎ + punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) + ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ + punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) + ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ + punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k)) + ≡⟨ cong (punchIn j) (inverseʳ π) ⟩ + punchIn j (punchOut j≢k) + ≡⟨ punchIn-punchOut j≢k ⟩ + k ∎ ------------------------------------------------------------------------ -- Other properties @@ -285,17 +301,23 @@ insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ pu insert-punchIn i j π k with i ≟ punchIn i k ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k) ... | no i≢punchInᵢk = begin - punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ - punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ - punchIn j (π ⟨$⟩ʳ k) ∎ + punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk) + ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ + punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) + ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ + punchIn j (π ⟨$⟩ʳ k) + ∎ insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π insert-remove {m = m} {n = n} i π j with i ≟ j ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j ... | no i≢j = begin - punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ - π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ - π ⟨$⟩ʳ j ∎ + punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) + ≡⟨ punchIn-punchOut _ ⟩ + π ⟨$⟩ʳ punchIn i (punchOut i≢j) + ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ + π ⟨$⟩ʳ j + ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π remove-insert i j π k rewrite ≟-diag-refl i = begin From 075efe3c80c468a0d8b3abb83453a5d379352520 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Jun 2025 07:44:09 +0100 Subject: [PATCH 13/22] fix: merge conflicts --- src/Data/Fin/Permutation.agda | 22 +++++----------------- 1 file changed, 5 insertions(+), 17 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 86c2f00498..b5935f57f1 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -9,20 +9,13 @@ module Data.Fin.Permutation where open import Data.Bool.Base using (true; false) -<<<<<<< refactor-Fin-properties -open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut) -open import Data.Fin.Patterns using (0F) +open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut) +open import Data.Fin.Patterns using (0F; 1F) open import Data.Fin.Properties using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag - ; opposite-involutive + ; cast-involutive; opposite-involutive ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut ; punchOut-cong; punchOut-cong′) -======= -open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut) -open import Data.Fin.Patterns using (0F; 1F) -open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn; - punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive) ->>>>>>> master import Data.Fin.Permutation.Components as PC open import Data.Nat.Base using (ℕ; suc; zero) open import Data.Product.Base using (_,_) @@ -106,13 +99,8 @@ flip = ↔-sym infixr 9 _∘ₚ_ -<<<<<<< refactor-Fin-properties -reverse : Permutation′ n -reverse = permutation opposite opposite opposite-involutive opposite-involutive -======= _∘ₚ_ : Permutation m n → Permutation n o → Permutation m o π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁ ->>>>>>> master ------------------------------------------------------------------------ -- Non-trivial identity @@ -144,8 +132,8 @@ reverse : Permutation n n reverse = permutation opposite opposite - PC.reverse-involutive - PC.reverse-involutive + opposite-involutive + opposite-involutive ------------------------------------------------------------------------ -- Element removal From c4fe9947e7c222f761e2bb9aa064d1d4f753e28e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Jun 2025 05:06:17 +0100 Subject: [PATCH 14/22] fix: equation alignment --- src/Data/Fin/Permutation.agda | 55 ++++++++++++----------------------- 1 file changed, 19 insertions(+), 36 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index b5935f57f1..b85c8f0b9f 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -242,15 +242,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k = begin - punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) - ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ - punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) - ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ - punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k)) - ≡⟨ cong (punchIn i) (inverseˡ π) ⟩ - punchIn i (punchOut i≢k) - ≡⟨ punchIn-punchOut i≢k ⟩ - k ∎ + punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ + punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ + punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k)) ≡⟨ cong (punchIn i) (inverseˡ π) ⟩ + punchIn i (punchOut i≢k) ≡⟨ punchIn-punchOut i≢k ⟩ + k ∎ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ k with j ≟ k @@ -259,15 +255,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k = begin - punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) - ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ - punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) - ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ - punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k)) - ≡⟨ cong (punchIn j) (inverseʳ π) ⟩ - punchIn j (punchOut j≢k) - ≡⟨ punchIn-punchOut j≢k ⟩ - k ∎ + punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ + punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ + punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k)) ≡⟨ cong (punchIn j) (inverseʳ π) ⟩ + punchIn j (punchOut j≢k) ≡⟨ punchIn-punchOut j≢k ⟩ + k ∎ ------------------------------------------------------------------------ -- Swapping @@ -343,29 +335,20 @@ insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ pu insert-punchIn i j π k with i ≟ punchIn i k ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k) ... | no i≢punchInᵢk = begin - punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk) - ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ - punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) - ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ - punchIn j (π ⟨$⟩ʳ k) - ∎ + punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ + punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ + punchIn j (π ⟨$⟩ʳ k) ∎ insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π insert-remove {m = m} {n = n} i π j with i ≟ j ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j ... | no i≢j = begin - punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) - ≡⟨ punchIn-punchOut _ ⟩ - π ⟨$⟩ʳ punchIn i (punchOut i≢j) - ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ - π ⟨$⟩ʳ j - ∎ + punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ + π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ + π ⟨$⟩ʳ j ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π remove-insert i j π k rewrite ≟-diag-refl i = begin - punchOut {i = j} _ - ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩ - punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) - ≡⟨ punchOut-punchIn j ⟩ - π ⟨$⟩ʳ k - ∎ + punchOut {i = j} _ ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩ + punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩ + π ⟨$⟩ʳ k ∎ From 30ccfa9f0737b8eba587e0c43914c0f2ced99e03 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Jun 2025 05:16:09 +0100 Subject: [PATCH 15/22] fix: equation alignment --- src/Data/Fin/Permutation.agda | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index b85c8f0b9f..5f7f3c7728 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -168,27 +168,19 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ j = begin - from (to j) - ≡⟨⟩ - punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ - ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ - punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ - ≡⟨ punchOut-cong i (inverseˡ π) ⟩ - punchOut {i = i} {punchIn i j} _ - ≡⟨ punchOut-punchIn i ⟩ - j ∎ + from (to j) ≡⟨⟩ + punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ + punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩ + punchOut {i = i} {punchIn i j} _ ≡⟨ punchOut-punchIn i ⟩ + j ∎ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ j = begin - to (from j) - ≡⟨⟩ - punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ - ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ - punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ - ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ - punchOut {i = πʳ i} {punchIn (πʳ i) j} _ - ≡⟨ punchOut-punchIn (πʳ i) ⟩ - j ∎ + to (from j) ≡⟨⟩ + punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ + punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ + punchOut {i = πʳ i} {punchIn (πʳ i) j} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩ + j ∎ ------------------------------------------------------------------------ -- Lifting From 8a54c1c4715f54929241aef837d6df8dd4e6c627 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Jun 2025 05:23:10 +0100 Subject: [PATCH 16/22] refactor: `yes` and `no` --- src/Data/Fin/Permutation/Components.agda | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index 4f38ab0da6..ca9cd9ed19 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -13,8 +13,7 @@ open import Data.Fin.Base using (Fin; suc; opposite; toℕ) open import Data.Fin.Properties using (_≟_; ≟-diag; ≟-diag-refl ; opposite-prop; opposite-involutive; opposite-suc) -open import Relation.Nullary.Reflects using (invert) -open import Relation.Nullary.Decidable.Core using (does; _because_) +open import Relation.Nullary.Decidable.Core using (does; yes; no) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) @@ -37,13 +36,13 @@ transpose i j k with does (k ≟ i) transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j transpose-iij i j with j ≟ i in j≟i -... | true because [j≡i] = sym (invert [j≡i]) -... | false because _ rewrite j≟i = refl +... | yes j≡i = sym j≡i +... | no _ rewrite j≟i = refl transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i transpose-ijj i j with j ≟ i -... | true because [j≡i] = invert [j≡i] -... | false because _ rewrite ≟-diag-refl j = refl +... | yes j≡i = j≡i +... | no _ rewrite ≟-diag-refl j = refl transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j transpose-iji i j rewrite ≟-diag-refl i = refl @@ -51,10 +50,10 @@ transpose-iji i j rewrite ≟-diag-refl i = refl transpose-transpose : ∀ {n} {i j k l : Fin n} → transpose i j k ≡ l → transpose j i l ≡ k transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i -... | true because [k≡i] rewrite ≟-diag (sym eq) = sym (invert [k≡i]) -... | false because [k≢i] with k ≟ j in k≟j -... | true because [k≡j] rewrite eq | transpose-ijj j l = sym (invert [k≡j]) -... | false because [k≢j] rewrite eq | k≟j | k≟i = refl +... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i +... | no k≢i with k ≟ j in k≟j +... | yes k≡j rewrite eq | transpose-ijj j l = sym k≡j +... | no k≢j rewrite eq | k≟j | k≟i = refl transpose-inverse : ∀ {n} (i j : Fin n) {k} → transpose i j (transpose j i k) ≡ k From f9fc5de905f26ad63e90d5b2a80a2161fc534251 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 30 Jun 2025 08:44:11 +0100 Subject: [PATCH 17/22] fix\; remove Fairbairn violation --- CHANGELOG.md | 1 - src/Data/Nat/Properties.agda | 3 --- 2 files changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 26fe09d71a..757b86385e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -350,7 +350,6 @@ Additions to existing modules * In `Data.Nat.Properties`: ```agda - ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl ≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n ``` diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 3e93abcfb5..907a215ee8 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -110,9 +110,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq ≟-diag = ≡-≟-identity _≟_ -≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl -≟-diag-refl _ = ≟-diag refl - ≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n ≟-off-diag = ≢-≟-identity _≟_ From 3a5b6cd4fa3644fc5d892a0fae7790a9f0ae62ec Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 07:58:14 +0100 Subject: [PATCH 18/22] rename: `transpose` lemmas --- CHANGELOG.md | 6 +++--- src/Data/Fin/Permutation/Components.agda | 14 +++++++------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 459b84a269..8ba65ea8bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -323,9 +323,9 @@ Additions to existing modules * In `Data.Fin.Permutation.Components`: ```agda - transpose-iij : (i j : Fin n) → transpose i i j ≡ j - transpose-ijj : (i j : Fin n) → transpose i j j ≡ i - transpose-iji : (i j : Fin n) → transpose i j i ≡ j + transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j + transpose[i,j,j]≡i : (i j : Fin n) → transpose i j j ≡ i + transpose[i,j,i]≡j : (i j : Fin n) → transpose i j i ≡ j transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k ``` diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index ca9cd9ed19..f126906600 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -34,25 +34,25 @@ transpose i j k with does (k ≟ i) -- Properties ------------------------------------------------------------------------ -transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j -transpose-iij i j with j ≟ i in j≟i +transpose[i,i,j]≡j : ∀ {n} (i j : Fin n) → transpose i i j ≡ j +transpose[i,i,j]≡j i j with j ≟ i in j≟i ... | yes j≡i = sym j≡i ... | no _ rewrite j≟i = refl -transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i -transpose-ijj i j with j ≟ i +transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i +transpose[i,j,j]≡i i j with j ≟ i ... | yes j≡i = j≡i ... | no _ rewrite ≟-diag-refl j = refl -transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j -transpose-iji i j rewrite ≟-diag-refl i = refl +transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j +transpose[i,j,i]≡j i j rewrite ≟-diag-refl i = refl transpose-transpose : ∀ {n} {i j k l : Fin n} → transpose i j k ≡ l → transpose j i l ≡ k transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i ... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i ... | no k≢i with k ≟ j in k≟j -... | yes k≡j rewrite eq | transpose-ijj j l = sym k≡j +... | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j ... | no k≢j rewrite eq | k≟j | k≟i = refl transpose-inverse : ∀ {n} (i j : Fin n) {k} → From a5b574e6162c8689c4880b09fdb468af647fc40c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:05:50 +0100 Subject: [PATCH 19/22] rename: decidable equality lemmas --- CHANGELOG.md | 8 ++++---- src/Data/Fin/Properties.agda | 12 ++++++------ src/Data/Nat/Properties.agda | 4 ++-- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8ba65ea8bf..b47f8dcdf9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -332,9 +332,9 @@ Additions to existing modules * In `Data.Fin.Properties`: ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq - ≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j + ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq + ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl + ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k inject!-injective : Injective _≡_ _≡_ inject! inject!-< : (k : Fin′ i) → inject! k < i @@ -424,7 +424,7 @@ Additions to existing modules * In `Data.Nat.Properties`: ```agda - ≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n + ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n ``` * In `Data.Product.Function.Dependent.Propositional`: diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index ab76ac8043..f78b652a85 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -106,14 +106,14 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y) ≡-irrelevant : Irrelevant {A = Fin n} _≡_ ≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ -≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq -≟-diag = ≡-≟-identity _≟_ +≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq +≟-≡ = ≡-≟-identity _≟_ -≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl -≟-diag-refl _ = ≟-diag refl +≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl +≟-≡-refl _ = ≟-≡ refl -≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j -≟-off-diag = ≢-≟-identity _≟_ +≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j +≟-≢ = ≢-≟-identity _≟_ ------------------------------------------------------------------------ -- Structures diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index f639ff8944..7f32b78089 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -114,8 +114,8 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq ≟-diag = ≡-≟-identity _≟_ -≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n -≟-off-diag = ≢-≟-identity _≟_ +≟-≡ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n +≟-≡ = ≢-≟-identity _≟_ ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) ≡-isDecEquivalence = record From 4b183660104354852aea8c7d1d9d864a7a9c917a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:11:35 +0100 Subject: [PATCH 20/22] fix: use of new names --- src/Data/Fin/Permutation.agda | 12 ++++++------ src/Data/Fin/Permutation/Components.agda | 8 ++++---- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 7838763246..5606d3773b 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false) open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut) open import Data.Fin.Patterns using (0F; 1F) open import Data.Fin.Properties - using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag + using (¬Fin0; _≟_; ≟-≡-refl; ≟-≢ ; cast-involutive; opposite-involutive ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut ; punchOut-cong; punchOut-cong′) @@ -229,10 +229,10 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ inverseʳ′ : StrictlyInverseʳ _≡_ to from inverseʳ′ k with i ≟ k - ... | yes i≡k rewrite ≟-diag-refl j = i≡k + ... | yes i≡k rewrite ≟-≡-refl j = i≡k ... | no i≢k with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym - rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k + rewrite ≟-≢ j≢punchInⱼπʳpunchOuti≢k = begin punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩ punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩ @@ -242,10 +242,10 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′ inverseˡ′ : StrictlyInverseˡ _≡_ to from inverseˡ′ k with j ≟ k - ... | yes j≡k rewrite ≟-diag-refl i = j≡k + ... | yes j≡k rewrite ≟-≡-refl i = j≡k ... | no j≢k with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym - rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k + rewrite ≟-≢ i≢punchInᵢπˡpunchOutj≢k = begin punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩ punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩ @@ -340,7 +340,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j π ⟨$⟩ʳ j ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π -remove-insert i j π k rewrite ≟-diag-refl i = begin +remove-insert i j π k rewrite ≟-≡-refl i = begin punchOut {i = j} _ ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩ punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩ π ⟨$⟩ʳ k ∎ diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index f126906600..b8597674f8 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/src/Data/Fin/Permutation/Components.agda @@ -11,7 +11,7 @@ module Data.Fin.Permutation.Components where open import Data.Bool.Base using (Bool; true; false) open import Data.Fin.Base using (Fin; suc; opposite; toℕ) open import Data.Fin.Properties - using (_≟_; ≟-diag; ≟-diag-refl + using (_≟_; ≟-≡; ≟-≡-refl ; opposite-prop; opposite-involutive; opposite-suc) open import Relation.Nullary.Decidable.Core using (does; yes; no) open import Relation.Binary.PropositionalEquality.Core @@ -42,15 +42,15 @@ transpose[i,i,j]≡j i j with j ≟ i in j≟i transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i transpose[i,j,j]≡i i j with j ≟ i ... | yes j≡i = j≡i -... | no _ rewrite ≟-diag-refl j = refl +... | no _ rewrite ≟-≡-refl j = refl transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j -transpose[i,j,i]≡j i j rewrite ≟-diag-refl i = refl +transpose[i,j,i]≡j i j rewrite ≟-≡-refl i = refl transpose-transpose : ∀ {n} {i j k l : Fin n} → transpose i j k ≡ l → transpose j i l ≡ k transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i -... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i +... | yes k≡i rewrite ≟-≡ (sym eq) = sym k≡i ... | no k≢i with k ≟ j in k≟j ... | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j ... | no k≢j rewrite eq | k≟j | k≟i = refl From a8dfef9087e714b12628c629669d695dcaedfe32 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:13:52 +0100 Subject: [PATCH 21/22] restore: original alignment --- src/Data/Fin/Permutation.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 5606d3773b..078e53c3bb 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -335,9 +335,9 @@ insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$ insert-remove {m = m} {n = n} i π j with i ≟ j ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j ... | no i≢j = begin - punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ - π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ - π ⟨$⟩ʳ j ∎ + punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩ + π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩ + π ⟨$⟩ʳ j ∎ remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π remove-insert i j π k rewrite ≟-≡-refl i = begin From ba97e414f6d1207abad8e238133b4a9ba69f80b4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 21 Jul 2025 21:18:52 +0100 Subject: [PATCH 22/22] fix: `CHANGELOG` --- CHANGELOG.md | 525 +-------------------------------------------------- 1 file changed, 2 insertions(+), 523 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b47f8dcdf9..6a236351f9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.3-dev +Version 2.4-dev =============== -The library has been tested using Agda 2.7.0 and 2.7.0.1. +The library has been tested using Agda 2.8.0. Highlights ---------- @@ -9,318 +9,24 @@ Highlights Bug-fixes --------- -* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` - to `#-sym` in order to avoid overloaded projection. - `irrefl` and `cotrans` are similarly renamed for the sake of consistency. - -* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`, - the record constructors `_,_` incorrectly had no declared fixity. They have been given - the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. - -* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a - `RightInverse`. - This has been deprecated in favor or `rightInverse`, and a corrected (and - correctly-named) function `leftInverse` has been added. - -* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` - has been modified to correctly support equational reasoning at the beginning and the end. - The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors - of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps - are changed, this modification is non-backwards compatible. - Non-backwards compatible changes -------------------------------- -* The implementation of `≤-total` in `Data.Nat.Properties` has been altered - to use operations backed by primitives, rather than recursion, making it - significantly faster. However, its reduction behaviour on open terms may have - changed. - Minor improvements ------------------ -* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary` - to its own dedicated module `Relation.Nullary.Irrelevant`. - Deprecated modules ------------------ Deprecated names ---------------- -* In `Algebra.Definitions.RawMagma`: - ```agda - _∣∣_ ↦ _∥_ - _∤∤_ ↦ _∦_ - ``` - -* In `Algebra.Lattice.Properties.BooleanAlgebra` - ```agda - ⊥≉⊤ ↦ ¬⊥≈⊤ - ⊤≉⊥ ↦ ¬⊤≈⊥ - ``` - -* In `Algebra.Module.Consequences` - ```agda - *ₗ-assoc+comm⇒*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ᵣ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - *ᵣ-assoc+comm⇒*ₗ-assoc ↦ *ᵣ-assoc∧comm⇒*ₗ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - ``` - -* In `Algebra.Modules.Structures.IsLeftModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Modules.Structures.IsRightModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣∣-sym ↦ ∥-sym - ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ - ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ - ∣∣-resp-≈ ↦ ∥-resp-≈ - ∤∤-sym -≈ ↦ ∦-sym - ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ - ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ - ∤∤-resp-≈ ↦ ∦-resp-≈ - ∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈ - ∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈ - ∣-resp-≈ ↦ ∣ʳ-resp-≈ - x∣yx ↦ x∣ʳyx - xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ∣∣-refl ↦ ∥-refl - ∣∣-reflexive ↦ ∥-reflexive - ∣∣-isEquivalence ↦ ∥-isEquivalence - ε∣_ ↦ ε∣ʳ_ - ∣-refl ↦ ∣ʳ-refl - ∣-reflexive ↦ ∣ʳ-reflexive - ∣-isPreorder ↦ ∣ʳ-isPreorder - ∣-preorder ↦ ∣ʳ-preorder - ``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣∣-trans ↦ ∥-trans - ∣-trans ↦ ∣ʳ-trans - ``` - -* In `Algebra.Structures.Group`: - ```agda - uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique - uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique - ``` - -* In `Data.List.Base`: - ```agda - and ↦ Data.Bool.ListAction.and - or ↦ Data.Bool.ListAction.or - any ↦ Data.Bool.ListAction.any - all ↦ Data.Bool.ListAction.all - sum ↦ Data.Nat.ListAction.sum - product ↦ Data.Nat.ListAction.product - ``` - -* In `Data.List.Properties`: - ```agda - sum-++ ↦ Data.Nat.ListAction.Properties.sum-++ - ∈⇒∣product ↦ Data.Nat.ListAction.Properties.∈⇒∣product - product≢0 ↦ Data.Nat.ListAction.Properties.product≢0 - ∈⇒≤product ↦ Data.Nat.ListAction.Properties.∈⇒≤product - ∷-ʳ++-eqFree ↦ Data.List.Properties.ʳ++-ʳ++-eqFree - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - sum-↭ ↦ Data.Nat.ListAction.Properties.sum-↭ - product-↭ ↦ Data.Nat.ListAction.Properties.product-↭ - ``` - -* In `Data.Product.Function.Dependent.Setoid`: - ```agda - left-inverse ↦ rightInverse - ``` - -* In `Data.Product.Nary.NonDependent`: - ```agda - Allₙ ↦ Pointwiseₙ - ``` - New modules ----------- -* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. - -* `Algebra.Morphism.Construct.DirectProduct`. - -* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. - -* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. - -* `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid. - -* `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid. - -* `Data.List.Sort.InsertionSort.{agda|Base|Properties}` defines insertion sort and proves properties of insertion sort such as Sorted and Permutation properties. - -* `Data.List.Sort.MergenSort.{agda|Base|Properties}` is a refactor of the previous `Data.List.Sort.MergenSort`. - -* `Data.Sign.Show` to show a sign. - -* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`. - -* `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER - -* `Relation.Nullary.Recomputable.Core` - Additions to existing modules ----------------------------- -* In `Algebra.Consequences.Base`: - ```agda - module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) - where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Consequences.Setoid`: - ```agda - module Congruence (cong : Congruent₂ _≈_ _∙_) where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Construct.Pointwise`: - ```agda - isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → - IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# → - IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# → - IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# → - IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#) - isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# → - IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# → - IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#) - commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ) - nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ) - semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ) - idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ) - kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ) - quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) - commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) - ``` - -* In `Algebra.Modules.Properties`: - ```agda - inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y - inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ - ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ - ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ - x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y - xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ε∣ˡ_ : ∀ x → ε ∣ˡ x - ∣ˡ-refl : Reflexive _∣ˡ_ - ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ - ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ - ∣ˡ-preorder : Preorder a ℓ _ - ``` - -* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups - -``` - uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w - uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x - uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) - uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) - uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) - uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) - uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z - uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y)) - [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x) - [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x) - [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x) - uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x - uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) - uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) -``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣ˡ-trans : Transitive _∣ˡ_ - x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y - x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z - x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y - x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z - ``` - -* In `Algebra.Properties.CommutativeSemigroup.Divisibility`: - ```agda - ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b - ``` - -* In `Data.Bool.Properties`: - ```agda - if-eta : ∀ b → (if b then x else x) ≡ x - if-idem-then : ∀ b → (if b then (if b then x else y) else y) ≡ (if b then x else y) - if-idem-else : ∀ b → (if b then x else (if b then x else y)) ≡ (if b then x else y) - if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y) - if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) - if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x) - if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) - if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) - if-xor : ∀ b → (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y)) - if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y) - if-cong-then : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y) - if-cong-else : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z) - if-cong₂ : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w) - ``` - -* In `Data.Fin.Base`: - ```agda - _≰_ : Rel (Fin n) 0ℓ - _≮_ : Rel (Fin n) 0ℓ - lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n - ``` - -* In `Data.Fin.Permutation`: - ```agda - cast-id : .(m ≡ n) → Permutation m n - swap : Permutation m n → Permutation (2+ m) (2+ n) - ``` - * In `Data.Fin.Permutation.Components`: ```agda transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j @@ -335,236 +41,9 @@ Additions to existing modules ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j - cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k - inject!-injective : Injective _≡_ _≡_ inject! - inject!-< : (k : Fin′ i) → inject! k < i - lower-injective : lower i i