From 617bd621e93d088f03c36c1b2e9993c705f5d059 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 25 Jul 2025 12:04:07 +0100 Subject: [PATCH 1/6] =?UTF-8?q?refactor:=20make=20`n=E2=89=A2i=20:=20n=20?= =?UTF-8?q?=E2=89=A2=20to=E2=84=95=20i`=20argument=20to=20`lower=E2=82=81`?= =?UTF-8?q?=20irrelevant?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Fin/Base.agda | 8 ++++++-- src/Data/Fin/Properties.agda | 37 +++++++++++++++++++++--------------- 2 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index c502512448..c50e1a1002 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -20,6 +20,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Nullary.Recomputable using (¬-recompute) private variable @@ -116,8 +117,11 @@ inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n)) -- lower₁ "i" _ = "i". -lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n -lower₁ {zero} zero ne = contradiction refl ne +lower₁-¬0≢0 : ∀ {ℓ} {A : Set ℓ} → .(0 ≢ 0) → A +lower₁-¬0≢0 0≢0 = contradiction refl (¬-recompute 0≢0) + +lower₁ : ∀ (i : Fin (suc n)) → .(n ≢ toℕ i) → Fin n +lower₁ {zero} zero ne = lower₁-¬0≢0 ne lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f87eef534..263b5b69f5 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -47,6 +47,7 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡ 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.Recomputable using (¬-recompute) open import Relation.Nullary.Reflects using (Reflects; invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) @@ -506,30 +507,30 @@ inject!-< {suc n} {suc i} (suc k) = s≤s (inject!-< k) -- lower₁ ------------------------------------------------------------------------ -toℕ-lower₁ : ∀ i (p : n ≢ toℕ i) → toℕ (lower₁ i p) ≡ toℕ i -toℕ-lower₁ {ℕ.zero} zero p = contradiction refl p -toℕ-lower₁ {ℕ.suc m} zero p = refl -toℕ-lower₁ {ℕ.suc m} (suc i) p = cong ℕ.suc (toℕ-lower₁ i (p ∘ cong ℕ.suc)) +toℕ-lower₁ : ∀ i .(p : n ≢ toℕ i) → toℕ (lower₁ i p) ≡ toℕ i +toℕ-lower₁ {ℕ.zero} zero 0≢0 = lower₁-¬0≢0 0≢0 +toℕ-lower₁ {ℕ.suc m} zero _ = refl +toℕ-lower₁ {ℕ.suc m} (suc i) ne = cong ℕ.suc (toℕ-lower₁ i (ne ∘ cong ℕ.suc)) -lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} → +lower₁-injective : ∀ .{n≢i : n ≢ toℕ i} .{n≢j : n ≢ toℕ j} → lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j -lower₁-injective {zero} {zero} {_} {n≢i} {_} _ = contradiction refl n≢i -lower₁-injective {zero} {_} {zero} {_} {n≢j} _ = contradiction refl n≢j -lower₁-injective {suc n} {zero} {zero} {_} {_} refl = refl -lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq = +lower₁-injective {zero} {zero} {_} {0≢0} {_} _ = lower₁-¬0≢0 0≢0 +lower₁-injective {zero} {_} {zero} {_} {0≢0} _ = lower₁-¬0≢0 0≢0 +lower₁-injective {suc n} {zero} {zero} {_} {_} _ = refl +lower₁-injective {suc n} {suc i} {suc j} {_} {_} eq = cong suc (lower₁-injective (suc-injective eq)) ------------------------------------------------------------------------ -- inject₁ and lower₁ -inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → +inject₁-lower₁ : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → inject₁ (lower₁ i n≢i) ≡ i -inject₁-lower₁ {zero} zero 0≢0 = contradiction refl 0≢0 +inject₁-lower₁ {zero} zero 0≢0 = lower₁-¬0≢0 0≢0 inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) -lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → +lower₁-inject₁′ : ∀ (i : Fin n) .(n≢i : n ≢ toℕ (inject₁ i)) → lower₁ (inject₁ i) n≢i ≡ i lower₁-inject₁′ zero _ = refl lower₁-inject₁′ (suc i) n+1≢i+1 = @@ -539,15 +540,15 @@ lower₁-inject₁ : ∀ (i : Fin n) → lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i) -lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → +lower₁-irrelevant : ∀ (i : Fin (suc n)) .(n≢i₁ n≢i₂ : n ≢ toℕ i) → lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant {zero} zero 0≢0 _ = contradiction refl 0≢0 +lower₁-irrelevant {zero} zero 0≢0 _ = lower₁-¬0≢0 0≢0 lower₁-irrelevant {suc n} zero _ _ = refl lower₁-irrelevant {suc n} (suc i) _ _ = cong suc (lower₁-irrelevant i _ _) inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} → - (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i + .(n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) ------------------------------------------------------------------------ @@ -561,6 +562,12 @@ lower-injective {n = suc n} zero zero eq = refl lower-injective {n = suc n} (suc i) (suc j) eq = cong suc (lower-injective i j (suc-injective eq)) +lower₁≗lower : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → + lower₁ i n≢i ≡ lower i (ℕ.≤∧≢⇒< (toℕ≤pred[n]′ i) (n≢i ∘ sym)) +lower₁≗lower {n = zero} zero 0≢0 = lower₁-¬0≢0 0≢0 +lower₁≗lower {n = suc _ } zero _ = refl +lower₁≗lower {n = suc _ } (suc i) ne = cong suc (lower₁≗lower i (ne ∘ cong suc)) + ------------------------------------------------------------------------ -- inject≤ ------------------------------------------------------------------------ From 1f67bef42ac971782825f81feb2ee473b76cd88f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 25 Jul 2025 12:39:38 +0100 Subject: [PATCH 2/6] tightne imports --- src/Data/Fin/Properties.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 263b5b69f5..ed94784ab9 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -47,8 +47,7 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡ 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.Recomputable using (¬-recompute) -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?) From 156e93fb8b801bfd061de46a5f515e4ad3489c78 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 25 Jul 2025 12:51:48 +0100 Subject: [PATCH 3/6] second equivalence proof: pick one --- src/Data/Fin/Properties.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index ed94784ab9..6506d9bc85 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -567,6 +567,11 @@ lower₁≗lower {n = zero} zero 0≢0 = lower₁-¬0≢0 0≢0 lower₁≗lower {n = suc _ } zero _ = refl lower₁≗lower {n = suc _ } (suc i) ne = cong suc (lower₁≗lower i (ne ∘ cong suc)) +lower≗lower₁ : ∀ (i : Fin (suc n)) .(i Date: Fri, 25 Jul 2025 12:53:06 +0100 Subject: [PATCH 4/6] fix: uncommitted proof --- src/Data/Fin/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 6506d9bc85..c3f0486618 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -568,7 +568,7 @@ lower₁≗lower {n = suc _ } zero _ = refl lower₁≗lower {n = suc _ } (suc i) ne = cong suc (lower₁≗lower i (ne ∘ cong suc)) lower≗lower₁ : ∀ (i : Fin (suc n)) .(i Date: Sat, 26 Jul 2025 15:05:46 +0100 Subject: [PATCH 5/6] refactor: use `contradiction-irr` instead, following #2785 --- src/Data/Fin/Base.agda | 10 +++------- src/Data/Fin/Properties.agda | 17 +++++++++-------- src/Relation/Nullary/Negation/Core.agda | 4 ++-- 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index c50e1a1002..6b208a8a55 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -19,8 +19,7 @@ open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel) -open import Relation.Nullary.Negation.Core using (¬_; contradiction) -open import Relation.Nullary.Recomputable using (¬-recompute) +open import Relation.Nullary.Negation.Core using (¬_; contradiction-irr) private variable @@ -117,11 +116,8 @@ inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n)) -- lower₁ "i" _ = "i". -lower₁-¬0≢0 : ∀ {ℓ} {A : Set ℓ} → .(0 ≢ 0) → A -lower₁-¬0≢0 0≢0 = contradiction refl (¬-recompute 0≢0) - lower₁ : ∀ (i : Fin (suc n)) → .(n ≢ toℕ i) → Fin n -lower₁ {zero} zero ne = lower₁-¬0≢0 ne +lower₁ {zero} zero ne = contradiction-irr refl ne lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) @@ -257,7 +253,7 @@ opposite {suc n} (suc i) = inject₁ (opposite i) -- McBride's "First-order unification by structural recursion". punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n -punchOut {_} {zero} {zero} i≢j = contradiction refl i≢j +punchOut {_} {zero} {zero} i≢j = contradiction-irr refl i≢j punchOut {_} {zero} {suc j} _ = j punchOut {suc _} {suc i} {zero} _ = zero punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index c3f0486618..0bd3a09007 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -46,7 +46,8 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡ using (module ≡-Reasoning) 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.Negation.Core + using (¬_; contradiction; contradiction-irr) open import Relation.Nullary.Reflects using (invert) open import Relation.Unary as U using (U; Pred; Decidable; _⊆_; Satisfiable; Universal) @@ -506,15 +507,15 @@ inject!-< {suc n} {suc i} (suc k) = s≤s (inject!-< k) -- lower₁ ------------------------------------------------------------------------ -toℕ-lower₁ : ∀ i .(p : n ≢ toℕ i) → toℕ (lower₁ i p) ≡ toℕ i -toℕ-lower₁ {ℕ.zero} zero 0≢0 = lower₁-¬0≢0 0≢0 +toℕ-lower₁ : ∀ i .(n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i +toℕ-lower₁ {ℕ.zero} zero 0≢0 = contradiction-irr refl 0≢0 toℕ-lower₁ {ℕ.suc m} zero _ = refl toℕ-lower₁ {ℕ.suc m} (suc i) ne = cong ℕ.suc (toℕ-lower₁ i (ne ∘ cong ℕ.suc)) lower₁-injective : ∀ .{n≢i : n ≢ toℕ i} .{n≢j : n ≢ toℕ j} → lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j -lower₁-injective {zero} {zero} {_} {0≢0} {_} _ = lower₁-¬0≢0 0≢0 -lower₁-injective {zero} {_} {zero} {_} {0≢0} _ = lower₁-¬0≢0 0≢0 +lower₁-injective {zero} {zero} {_} {0≢0} {_} _ = contradiction-irr refl 0≢0 +lower₁-injective {zero} {_} {zero} {_} {0≢0} _ = contradiction-irr refl 0≢0 lower₁-injective {suc n} {zero} {zero} {_} {_} _ = refl lower₁-injective {suc n} {suc i} {suc j} {_} {_} eq = cong suc (lower₁-injective (suc-injective eq)) @@ -524,7 +525,7 @@ lower₁-injective {suc n} {suc i} {suc j} {_} {_} eq = inject₁-lower₁ : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → inject₁ (lower₁ i n≢i) ≡ i -inject₁-lower₁ {zero} zero 0≢0 = lower₁-¬0≢0 0≢0 +inject₁-lower₁ {zero} zero 0≢0 = contradiction-irr refl 0≢0 inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) @@ -541,7 +542,7 @@ lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i) lower₁-irrelevant : ∀ (i : Fin (suc n)) .(n≢i₁ n≢i₂ : n ≢ toℕ i) → lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant {zero} zero 0≢0 _ = lower₁-¬0≢0 0≢0 +lower₁-irrelevant {zero} zero 0≢0 _ = contradiction-irr refl 0≢0 lower₁-irrelevant {suc n} zero _ _ = refl lower₁-irrelevant {suc n} (suc i) _ _ = cong suc (lower₁-irrelevant i _ _) @@ -563,7 +564,7 @@ lower-injective {n = suc n} (suc i) (suc j) eq = lower₁≗lower : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → lower₁ i n≢i ≡ lower i (ℕ.≤∧≢⇒< (toℕ≤pred[n]′ i) (n≢i ∘ sym)) -lower₁≗lower {n = zero} zero 0≢0 = lower₁-¬0≢0 0≢0 +lower₁≗lower {n = zero} zero 0≢0 = contradiction-irr refl 0≢0 lower₁≗lower {n = suc _ } zero _ = refl lower₁≗lower {n = suc _ } (suc i) ne = cong suc (lower₁≗lower i (ne ∘ cong suc)) diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda index 73876e876c..b1e9425bf2 100644 --- a/src/Relation/Nullary/Negation/Core.agda +++ b/src/Relation/Nullary/Negation/Core.agda @@ -47,11 +47,11 @@ _¬-⊎_ = [_,_] ------------------------------------------------------------------------ -- Uses of negation -contradiction-irr : .A → ¬ A → Whatever +contradiction-irr : .A → .(¬ A) → Whatever contradiction-irr a ¬a = ⊥-elim-irr (¬a a) contradiction : A → ¬ A → Whatever -contradiction a = contradiction-irr a +contradiction a ¬a = contradiction-irr a ¬a contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a From e7b89f90136f88cdf6818ee70a56f7c71c458671 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 27 Jul 2025 09:12:17 +0100 Subject: [PATCH 6/6] fix: `CHANGELOG` --- CHANGELOG.md | 7 +++++++ src/Data/Fin/Properties.agda | 11 ----------- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3cf9a9ac90..a86cbb4b9c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,13 @@ Non-backwards compatible changes Minor improvements ------------------ +* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further + weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is + safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`. + +* As a consequence, the type of `Data.Fin.Base.lower₁` has been correspondingly + weakened so that the negated hypothesis `n≢i : n ≢ toℕ i` is marked irrelevant. + Deprecated modules ------------------ diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0bd3a09007..9e846b9c00 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -562,17 +562,6 @@ lower-injective {n = suc n} zero zero eq = refl lower-injective {n = suc n} (suc i) (suc j) eq = cong suc (lower-injective i j (suc-injective eq)) -lower₁≗lower : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) → - lower₁ i n≢i ≡ lower i (ℕ.≤∧≢⇒< (toℕ≤pred[n]′ i) (n≢i ∘ sym)) -lower₁≗lower {n = zero} zero 0≢0 = contradiction-irr refl 0≢0 -lower₁≗lower {n = suc _ } zero _ = refl -lower₁≗lower {n = suc _ } (suc i) ne = cong suc (lower₁≗lower i (ne ∘ cong suc)) - -lower≗lower₁ : ∀ (i : Fin (suc n)) .(i