Skip to content

[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant #2783

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant #2783

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
617bd62
refactor: make `n≢i : n ≢ toℕ i` argument to `lower₁` irrelevant
jamesmckinna Jul 25, 2025
1f67bef
tightne imports
jamesmckinna Jul 25, 2025
156e93f
second equivalence proof: pick one
jamesmckinna Jul 25, 2025
c7bb4ca
fix: uncommitted proof
jamesmckinna Jul 25, 2025
31633ff
refactor: use `contradiction-irr` instead, following #2785
jamesmckinna Jul 26, 2025
e7b89f9
fix: `CHANGELOG`
jamesmckinna Jul 27, 2025
8cfb3f5
Merge branch 'master' into Fin-lower-properties
jamesmckinna Jul 31, 2025
2b3aa99
Merge branch 'master' into Fin-lower-properties
jamesmckinna Aug 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ Minor improvements
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.

* Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
```agda
README.Data.Fin.Relation.Unary.Top
Expand Down
8 changes: 4 additions & 4 deletions src/Data/Fin/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +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.Negation.Core using (¬_; contradiction-irr)

private
variable
Expand Down Expand Up @@ -116,8 +116,8 @@ 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₁ : ∀ (i : Fin (suc n)) → .(n ≢ toℕ i) → Fin n
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))

Expand Down Expand Up @@ -253,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))
Expand Down
33 changes: 17 additions & 16 deletions src/Data/Fin/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,8 @@ open import Relation.Binary.PropositionalEquality as ≡
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)
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)
Expand Down Expand Up @@ -521,30 +522,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 .(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₁-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} {_} _ = 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))

------------------------------------------------------------------------
-- 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 = 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))

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 =
Expand All @@ -554,15 +555,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 _ = contradiction-irr refl 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))

------------------------------------------------------------------------
Expand Down