From ac521f48a5512087e1018f979c26b3cb3fa66cb7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 11:46:57 +0100 Subject: [PATCH 01/16] =?UTF-8?q?simplified=20the=20analysis=20of=20`injec?= =?UTF-8?q?t=E2=82=81`=20and=20`lower=E2=82=81`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 2 ++ src/Data/Fin/Properties.agda | 37 +++++++++++++++++++----------------- 2 files changed, 22 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 420d85fddc..2bce9c9e48 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1174,6 +1174,8 @@ Deprecated names Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. + Additionally, `lower₁-inject₁′` has been deprecated in favour of `inject₁≡⇒lower₁≡`. + * In `Data.Fin.Permutation.Components`: ``` reverse ↦ Data.Fin.Base.opposite diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f520afda5..02d3465024 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -494,6 +494,13 @@ lower₁-injective {suc n} {zero} {zero} {_} {_} refl = refl lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq = cong suc (lower₁-injective (suc-injective eq)) +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 {suc n} zero _ _ = refl +lower₁-irrelevant {suc n} (suc i) _ _ = + cong suc (lower₁-irrelevant i _ _) + ------------------------------------------------------------------------ -- inject₁ and lower₁ @@ -504,26 +511,13 @@ 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) n≢i ≡ i -lower₁-inject₁′ zero _ = refl -lower₁-inject₁′ (suc i) n+1≢i+1 = - cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc)) +inject₁≡⇒lower₁≡ : ∀ {j : Fin (ℕ.suc n)} (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)) 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₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant {zero} zero 0≢0 _ = contradiction 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 -inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) +lower₁-inject₁ i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl ------------------------------------------------------------------------ -- inject≤ @@ -1165,3 +1159,12 @@ Please use <⇒<′ instead." "Warning: <′⇒≺ was deprecated in v2.0. Please use <′⇒< instead." #-} + +lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → + lower₁ (inject₁ i) n≢i ≡ i +lower₁-inject₁′ i n≢i = inject₁≡⇒lower₁≡ n≢i refl +{-# WARNING_ON_USAGE lower₁-inject₁′ +"Warning: lower₁-inject₁′ was deprecated in v2.0. +Please use inject₁≡⇒lower₁≡ instead." +#-} + From 5812f5bfd22c18978fd57e6cfda2f188d17dee80 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 13:42:42 +0100 Subject: [PATCH 02/16] =?UTF-8?q?draft=20revised=20versions=20of=20`lower?= =?UTF-8?q?=E2=82=81`=20defn=20and=20properties?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Lower.agda | 87 +++++++++++++++++++++ src/Data/Fin/Relation/Unary/TopREVISED.agda | 84 ++++++++++++++++++++ 2 files changed, 171 insertions(+) create mode 100644 README/Data/Fin/Relation/Unary/Lower.agda create mode 100644 src/Data/Fin/Relation/Unary/TopREVISED.agda diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda new file mode 100644 index 0000000000..138ef1dec5 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -0,0 +1,87 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example use of the 'top' view of Fin +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +-- +-- Using this view, we can redefine certain operations in `Data.Fin.Base`, +-- together with their corresponding properties in `Data.Fin.Properties`. +------------------------------------------------------------------------ + +--- NB this is a provisional commit, ahead of merging PR #1923 + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Relation.Unary.Lower where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) +open import Data.Fin.Properties + using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) +open import Data.Fin.Relation.Unary.TopREVISED +open import Level using (Level) +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred) + +private + variable + ℓ : Level + n : ℕ + i j : Fin n + +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Base.lower₁` and its properties + +-- definition of lower₁ + +lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n +lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = j + +------------------------------------------------------------------------ +-- properties of lower₁ + +toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i +toℕ-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = sym (toℕ-inject₁ 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 {i = i} {j = j} {n≢i} {n≢j} eq with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ i₁ with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ j₁ = cong inject₁ eq + +lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ +lower₁-irrelevant i n≢i₁ n≢i₂ with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ +... | ‵inject₁ j = refl + +------------------------------------------------------------------------ +-- inject₁ and lower₁ + +inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → + inject₁ (lower₁ i n≢i) ≡ i +inject₁-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = refl + +inject₁≡⇒lower₁≡ : {j : Fin (ℕ.suc n)} (n≢j : n ≢ toℕ j) → + inject₁ i ≡ j → lower₁ j n≢j ≡ i +inject₁≡⇒lower₁≡ {j = j} n≢j inject₁[i]≡j with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ j₁ = sym (inject₁-injective inject₁[i]≡j) + +lower₁-inject₁ : ∀ (i : Fin n) → + lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i +lower₁-inject₁ {n} i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl + diff --git a/src/Data/Fin/Relation/Unary/TopREVISED.agda b/src/Data/Fin/Relation/Unary/TopREVISED.agda new file mode 100644 index 0000000000..2f439e1c1b --- /dev/null +++ b/src/Data/Fin/Relation/Unary/TopREVISED.agda @@ -0,0 +1,84 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The 'top' view of Fin. +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Relation.Unary.TopREVISED where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁; toℕ) +open import Data.Fin.Properties using (toℕ-fromℕ) +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Unary using (Pred) + +private + variable + n : ℕ + i : Fin n + +------------------------------------------------------------------------ +-- The View, considered as a unary relation on Fin n + +-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following +-- inductively defined family on `Fin n` has constructors which target +-- *disjoint* instances of the family (moreover at indices `n = suc _`); +-- hence the interpretations of the View constructors will also be disjoint. + +data View : (i : Fin n) → Set where + ‵fromℕ : View (fromℕ n) + ‵inj₁ : View i → View (inject₁ i) + +pattern ‵inject₁ i = ‵inj₁ {i = i} _ + +-- The view covering function, witnessing soundness of the view + +view : (i : Fin n) → View i +view zero = view-zero where + view-zero : View (zero {n}) + view-zero {n = zero} = ‵fromℕ + view-zero {n = suc _} = ‵inj₁ view-zero +view (suc i) with view i +... | ‵fromℕ = ‵fromℕ +... | ‵inject₁ j = ‵inj₁ (view (suc j)) + +-- Interpretation of the view constructors + +⟦_⟧ : {i : Fin n} → View i → Fin n +⟦ ‵fromℕ ⟧ = fromℕ _ +⟦ ‵inject₁ i ⟧ = inject₁ i + +-- Completeness of the view + +view-complete : (v : View i) → ⟦ v ⟧ ≡ i +view-complete ‵fromℕ = refl +view-complete (‵inject₁ _) = refl + +-- 'Computational' behaviour of the covering function + +view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ +view-fromℕ zero = refl +view-fromℕ (suc n) rewrite view-fromℕ n = refl + +view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) +view-inject₁ zero = refl +view-inject₁ (suc i) rewrite view-inject₁ i = refl + +-- Uniqueness of the view + +view-unique : (v : View i) → view i ≡ v +view-unique ‵fromℕ = view-fromℕ _ +view-unique (‵inj₁ {i = i} v) = begin + view (inject₁ i) ≡⟨ view-inject₁ i ⟩ + ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ + ‵inj₁ v ∎ where open ≡-Reasoning + + From 30217290543656182e6bec5507f44b020198f532 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 13:45:26 +0100 Subject: [PATCH 03/16] fix-whitespace --- src/Data/Fin/Relation/Unary/TopREVISED.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/TopREVISED.agda b/src/Data/Fin/Relation/Unary/TopREVISED.agda index 2f439e1c1b..ae6f14ffa9 100644 --- a/src/Data/Fin/Relation/Unary/TopREVISED.agda +++ b/src/Data/Fin/Relation/Unary/TopREVISED.agda @@ -81,4 +81,3 @@ view-unique (‵inj₁ {i = i} v) = begin ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ ‵inj₁ v ∎ where open ≡-Reasoning - From 29693e412b84ba234821abb5ae8ae2419743faad Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 14:00:53 +0100 Subject: [PATCH 04/16] fix-whitespace --- README/Data/Fin/Relation/Unary/Lower.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 138ef1dec5..03f727a0c4 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -34,6 +34,18 @@ private n : ℕ i j : Fin n +------------------------------------------------------------------------ +-- Derived induction principle + +module _ (P : ∀ {n} → Pred (Fin (suc n)) ℓ) where + + view-inject₁-case : (Pinject₁[_] : (j : Fin n) → P (inject₁ j)) → + ∀ {i : Fin (suc n)} → n ≢ toℕ i → P i + view-inject₁-case Pinject₁[_] {i} n≢i with view i + ... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i + ... | ‵inject₁ j = Pinject₁[ j ] + + ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.lower₁` and its properties From 759bba2169675f238963efa39fa4555720c2948a Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Mon, 18 Sep 2023 01:58:38 +0100 Subject: [PATCH 05/16] Add a recursive view of `Fin n` (#1923) --- CHANGELOG.md | 7 ++ README/Data/Fin/Relation/Unary/Top.agda | 100 ++++++++++++++++++++++++ src/Data/Fin/Properties.agda | 3 + src/Data/Fin/Relation/Unary/Top.agda | 79 +++++++++++++++++++ 4 files changed, 189 insertions(+) create mode 100644 README/Data/Fin/Relation/Unary/Top.agda create mode 100644 src/Data/Fin/Relation/Unary/Top.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 420d85fddc..b1e8ab2fa6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1585,6 +1585,11 @@ New modules Data.Default ``` +* A small library defining a structurally recursive view of `Fin n`: + ``` + Data.Fin.Relation.Unary.Top + ``` + * A small library for a non-empty fresh list: ``` Data.List.Fresh.NonEmpty @@ -2146,6 +2151,8 @@ Additions to existing modules cast-is-id : cast eq k ≡ k subst-is-cast : subst Fin eq k ≡ cast eq k cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k + + fromℕ≢inject₁ : {i : Fin n} → fromℕ n ≢ inject₁ i ``` * Added new functions in `Data.Integer.Base`: diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..e602932827 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,100 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example use of the 'top' view of Fin +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +-- +-- Using this view, we can redefine certain operations in `Data.Fin.Base`, +-- together with their corresponding properties in `Data.Fin.Properties`. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Relation.Unary.Top where + +open import Data.Nat.Base using (ℕ; zero; suc; _∸_; _≤_) +open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc; ≤-reflexive) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁; _>_) +open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-weakInduction) +open import Data.Fin.Relation.Unary.Top +import Induction.WellFounded as WF +open import Level using (Level) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred) + +private + variable + ℓ : Level + n : ℕ + +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Base.opposite`, and its properties + +-- Definition + +opposite : Fin n → Fin n +opposite {suc n} i with view i +... | ‵fromℕ = zero +... | ‵inject₁ j = suc (opposite {n} j) + +-- Properties + +opposite-zero≡fromℕ : ∀ n → opposite {suc n} zero ≡ fromℕ n +opposite-zero≡fromℕ zero = refl +opposite-zero≡fromℕ (suc n) = cong suc (opposite-zero≡fromℕ n) + +opposite-fromℕ≡zero : ∀ n → opposite {suc n} (fromℕ n) ≡ zero +opposite-fromℕ≡zero n rewrite view-fromℕ n = refl + +opposite-suc≡inject₁-opposite : (j : Fin n) → + opposite (suc j) ≡ inject₁ (opposite j) +opposite-suc≡inject₁-opposite {suc n} i with view i +... | ‵fromℕ = refl +... | ‵inject₁ j = cong suc (opposite-suc≡inject₁-opposite {n} j) + +opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j +opposite-involutive {suc n} zero + rewrite opposite-zero≡fromℕ n + | view-fromℕ n = refl +opposite-involutive {suc n} (suc i) + rewrite opposite-suc≡inject₁-opposite i + | view-inject₁ (opposite i) = cong suc (opposite-involutive i) + +opposite-suc : (j : Fin n) → toℕ (opposite (suc j)) ≡ toℕ (opposite j) +opposite-suc j = begin + toℕ (opposite (suc j)) ≡⟨ cong toℕ (opposite-suc≡inject₁-opposite j) ⟩ + toℕ (inject₁ (opposite j)) ≡⟨ toℕ-inject₁ (opposite j) ⟩ + toℕ (opposite j) ∎ where open ≡-Reasoning + +opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) +opposite-prop {suc n} i with view i +... | ‵fromℕ rewrite toℕ-fromℕ n | n∸n≡0 n = refl +... | ‵inject₁ j = begin + suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩ + suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 (toℕ-weakInduction` + +open WF using (Acc; acc) + +>-weakInduction : (P : Pred (Fin (suc n)) ℓ) → + P (fromℕ n) → + (∀ i → P (suc i) → P (inject₁ i)) → + ∀ i → P i +>-weakInduction P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i) + where + induct : ∀ {i} → Acc _>_ i → P i + induct {i} (acc rec) with view i + ... | ‵fromℕ = Pₙ + ... | ‵inject₁ j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) + where + inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) ≤ toℕ (suc j) + inject₁[j]+1≤[j+1] = ≤-reflexive (toℕ-inject₁ (suc j)) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f520afda5..bcb1cd4745 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -449,6 +449,9 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j) -- inject₁ ------------------------------------------------------------------------ +fromℕ≢inject₁ : fromℕ n ≢ inject₁ i +fromℕ≢inject₁ {i = suc i} eq = fromℕ≢inject₁ {i = i} (suc-injective eq) + inject₁-injective : inject₁ i ≡ inject₁ j → i ≡ j inject₁-injective {i = zero} {zero} i≡j = refl inject₁-injective {i = suc i} {suc j} i≡j = diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..b6a567a9a8 --- /dev/null +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,79 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The 'top' view of Fin. +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Relation.Unary.Top where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁) +open import Relation.Binary.PropositionalEquality.Core + +private + variable + n : ℕ + i : Fin n + +------------------------------------------------------------------------ +-- The View, considered as a unary relation on Fin n + +-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following +-- inductively defined family on `Fin n` has constructors which target +-- *disjoint* instances of the family (moreover at indices `n = suc _`); +-- hence the interpretations of the View constructors will also be disjoint. + +data View : (i : Fin n) → Set where + ‵fromℕ : View (fromℕ n) + ‵inj₁ : View i → View (inject₁ i) + +pattern ‵inject₁ i = ‵inj₁ {i = i} _ + +-- The view covering function, witnessing soundness of the view + +view : (i : Fin n) → View i +view zero = view-zero where + view-zero : View (zero {n}) + view-zero {n = zero} = ‵fromℕ + view-zero {n = suc _} = ‵inj₁ view-zero +view (suc i) with view i +... | ‵fromℕ = ‵fromℕ +... | ‵inject₁ i = ‵inj₁ (view (suc i)) + +-- Interpretation of the view constructors + +⟦_⟧ : {i : Fin n} → View i → Fin n +⟦ ‵fromℕ ⟧ = fromℕ _ +⟦ ‵inject₁ i ⟧ = inject₁ i + +-- Completeness of the view + +view-complete : (v : View i) → ⟦ v ⟧ ≡ i +view-complete ‵fromℕ = refl +view-complete (‵inj₁ _) = refl + +-- 'Computational' behaviour of the covering function + +view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ +view-fromℕ zero = refl +view-fromℕ (suc n) rewrite view-fromℕ n = refl + +view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) +view-inject₁ zero = refl +view-inject₁ (suc i) rewrite view-inject₁ i = refl + +-- Uniqueness of the view + +view-unique : (v : View i) → view i ≡ v +view-unique ‵fromℕ = view-fromℕ _ +view-unique (‵inj₁ {i = i} v) = begin + view (inject₁ i) ≡⟨ view-inject₁ i ⟩ + ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ + ‵inj₁ v ∎ where open ≡-Reasoning From 2327fc7f39e24db152c54039f8f493b1284328f9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 11:46:57 +0100 Subject: [PATCH 06/16] =?UTF-8?q?simplified=20the=20analysis=20of=20`injec?= =?UTF-8?q?t=E2=82=81`=20and=20`lower=E2=82=81`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 2 ++ src/Data/Fin/Properties.agda | 37 +++++++++++++++++++----------------- 2 files changed, 22 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b1e8ab2fa6..0d5ca18934 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1174,6 +1174,8 @@ Deprecated names Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. + Additionally, `lower₁-inject₁′` has been deprecated in favour of `inject₁≡⇒lower₁≡`. + * In `Data.Fin.Permutation.Components`: ``` reverse ↦ Data.Fin.Base.opposite diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index bcb1cd4745..9c94958033 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -497,6 +497,13 @@ lower₁-injective {suc n} {zero} {zero} {_} {_} refl = refl lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq = cong suc (lower₁-injective (suc-injective eq)) +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 {suc n} zero _ _ = refl +lower₁-irrelevant {suc n} (suc i) _ _ = + cong suc (lower₁-irrelevant i _ _) + ------------------------------------------------------------------------ -- inject₁ and lower₁ @@ -507,26 +514,13 @@ 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) n≢i ≡ i -lower₁-inject₁′ zero _ = refl -lower₁-inject₁′ (suc i) n+1≢i+1 = - cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc)) +inject₁≡⇒lower₁≡ : ∀ {j : Fin (ℕ.suc n)} (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)) 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₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant {zero} zero 0≢0 _ = contradiction 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 -inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) +lower₁-inject₁ i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl ------------------------------------------------------------------------ -- inject≤ @@ -1168,3 +1162,12 @@ Please use <⇒<′ instead." "Warning: <′⇒≺ was deprecated in v2.0. Please use <′⇒< instead." #-} + +lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → + lower₁ (inject₁ i) n≢i ≡ i +lower₁-inject₁′ i n≢i = inject₁≡⇒lower₁≡ n≢i refl +{-# WARNING_ON_USAGE lower₁-inject₁′ +"Warning: lower₁-inject₁′ was deprecated in v2.0. +Please use inject₁≡⇒lower₁≡ instead." +#-} + From a60a140ad199de76fdcf4f4fcc0f3b14a7a67c80 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 13:42:42 +0100 Subject: [PATCH 07/16] =?UTF-8?q?draft=20revised=20versions=20of=20`lower?= =?UTF-8?q?=E2=82=81`=20defn=20and=20properties?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Lower.agda | 87 +++++++++++++++++++++ src/Data/Fin/Relation/Unary/TopREVISED.agda | 84 ++++++++++++++++++++ 2 files changed, 171 insertions(+) create mode 100644 README/Data/Fin/Relation/Unary/Lower.agda create mode 100644 src/Data/Fin/Relation/Unary/TopREVISED.agda diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda new file mode 100644 index 0000000000..138ef1dec5 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -0,0 +1,87 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example use of the 'top' view of Fin +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +-- +-- Using this view, we can redefine certain operations in `Data.Fin.Base`, +-- together with their corresponding properties in `Data.Fin.Properties`. +------------------------------------------------------------------------ + +--- NB this is a provisional commit, ahead of merging PR #1923 + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Relation.Unary.Lower where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) +open import Data.Fin.Properties + using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) +open import Data.Fin.Relation.Unary.TopREVISED +open import Level using (Level) +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred) + +private + variable + ℓ : Level + n : ℕ + i j : Fin n + +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Base.lower₁` and its properties + +-- definition of lower₁ + +lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n +lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = j + +------------------------------------------------------------------------ +-- properties of lower₁ + +toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i +toℕ-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = sym (toℕ-inject₁ 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 {i = i} {j = j} {n≢i} {n≢j} eq with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ i₁ with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ j₁ = cong inject₁ eq + +lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ +lower₁-irrelevant i n≢i₁ n≢i₂ with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ +... | ‵inject₁ j = refl + +------------------------------------------------------------------------ +-- inject₁ and lower₁ + +inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → + inject₁ (lower₁ i n≢i) ≡ i +inject₁-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = refl + +inject₁≡⇒lower₁≡ : {j : Fin (ℕ.suc n)} (n≢j : n ≢ toℕ j) → + inject₁ i ≡ j → lower₁ j n≢j ≡ i +inject₁≡⇒lower₁≡ {j = j} n≢j inject₁[i]≡j with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ j₁ = sym (inject₁-injective inject₁[i]≡j) + +lower₁-inject₁ : ∀ (i : Fin n) → + lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i +lower₁-inject₁ {n} i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl + diff --git a/src/Data/Fin/Relation/Unary/TopREVISED.agda b/src/Data/Fin/Relation/Unary/TopREVISED.agda new file mode 100644 index 0000000000..2f439e1c1b --- /dev/null +++ b/src/Data/Fin/Relation/Unary/TopREVISED.agda @@ -0,0 +1,84 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The 'top' view of Fin. +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Relation.Unary.TopREVISED where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁; toℕ) +open import Data.Fin.Properties using (toℕ-fromℕ) +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Unary using (Pred) + +private + variable + n : ℕ + i : Fin n + +------------------------------------------------------------------------ +-- The View, considered as a unary relation on Fin n + +-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following +-- inductively defined family on `Fin n` has constructors which target +-- *disjoint* instances of the family (moreover at indices `n = suc _`); +-- hence the interpretations of the View constructors will also be disjoint. + +data View : (i : Fin n) → Set where + ‵fromℕ : View (fromℕ n) + ‵inj₁ : View i → View (inject₁ i) + +pattern ‵inject₁ i = ‵inj₁ {i = i} _ + +-- The view covering function, witnessing soundness of the view + +view : (i : Fin n) → View i +view zero = view-zero where + view-zero : View (zero {n}) + view-zero {n = zero} = ‵fromℕ + view-zero {n = suc _} = ‵inj₁ view-zero +view (suc i) with view i +... | ‵fromℕ = ‵fromℕ +... | ‵inject₁ j = ‵inj₁ (view (suc j)) + +-- Interpretation of the view constructors + +⟦_⟧ : {i : Fin n} → View i → Fin n +⟦ ‵fromℕ ⟧ = fromℕ _ +⟦ ‵inject₁ i ⟧ = inject₁ i + +-- Completeness of the view + +view-complete : (v : View i) → ⟦ v ⟧ ≡ i +view-complete ‵fromℕ = refl +view-complete (‵inject₁ _) = refl + +-- 'Computational' behaviour of the covering function + +view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ +view-fromℕ zero = refl +view-fromℕ (suc n) rewrite view-fromℕ n = refl + +view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) +view-inject₁ zero = refl +view-inject₁ (suc i) rewrite view-inject₁ i = refl + +-- Uniqueness of the view + +view-unique : (v : View i) → view i ≡ v +view-unique ‵fromℕ = view-fromℕ _ +view-unique (‵inj₁ {i = i} v) = begin + view (inject₁ i) ≡⟨ view-inject₁ i ⟩ + ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ + ‵inj₁ v ∎ where open ≡-Reasoning + + From d4ba13d8fdf721bd5ce3d77196e4c84cf9f7021e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 13:45:26 +0100 Subject: [PATCH 08/16] fix-whitespace --- src/Data/Fin/Relation/Unary/TopREVISED.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/TopREVISED.agda b/src/Data/Fin/Relation/Unary/TopREVISED.agda index 2f439e1c1b..ae6f14ffa9 100644 --- a/src/Data/Fin/Relation/Unary/TopREVISED.agda +++ b/src/Data/Fin/Relation/Unary/TopREVISED.agda @@ -81,4 +81,3 @@ view-unique (‵inj₁ {i = i} v) = begin ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ ‵inj₁ v ∎ where open ≡-Reasoning - From 754b88d0588420fe314017e772b62c5094f3b88b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 14:00:53 +0100 Subject: [PATCH 09/16] fix-whitespace --- README/Data/Fin/Relation/Unary/Lower.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 138ef1dec5..03f727a0c4 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -34,6 +34,18 @@ private n : ℕ i j : Fin n +------------------------------------------------------------------------ +-- Derived induction principle + +module _ (P : ∀ {n} → Pred (Fin (suc n)) ℓ) where + + view-inject₁-case : (Pinject₁[_] : (j : Fin n) → P (inject₁ j)) → + ∀ {i : Fin (suc n)} → n ≢ toℕ i → P i + view-inject₁-case Pinject₁[_] {i} n≢i with view i + ... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i + ... | ‵inject₁ j = Pinject₁[ j ] + + ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.lower₁` and its properties From 69c2fcf051ed08f73d1632dfad1eeee714f53a53 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 06:48:42 +0100 Subject: [PATCH 10/16] =?UTF-8?q?rebase,=20then=20develop=20derived=20view?= =?UTF-8?q?=20and=20`inject=E2=82=81=E2=81=BB=C2=B9`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Lower.agda | 111 ++++++++++++++------ src/Data/Fin/Relation/Unary/TopREVISED.agda | 83 --------------- 2 files changed, 76 insertions(+), 118 deletions(-) delete mode 100644 src/Data/Fin/Relation/Unary/TopREVISED.agda diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 03f727a0c4..7aff3bc812 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -18,11 +18,11 @@ module README.Data.Fin.Relation.Unary.Lower where -open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Base using (ℕ; zero; suc; pred) open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) -open import Data.Fin.Relation.Unary.TopREVISED +import Data.Fin.Relation.Unary.Top as Top open import Level using (Level) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality @@ -35,65 +35,106 @@ private i j : Fin n ------------------------------------------------------------------------ --- Derived induction principle +-- EXPERIMENTAL: Derived induction principles from the view, via another view! -module _ (P : ∀ {n} → Pred (Fin (suc n)) ℓ) where +-- The idea being, that in what follows, a call pattern is repeated over +-- and over again, so should be reified as induction over a revised view, +-- obtained from `Top.view` by restricting the domain - view-inject₁-case : (Pinject₁[_] : (j : Fin n) → P (inject₁ j)) → - ∀ {i : Fin (suc n)} → n ≢ toℕ i → P i - view-inject₁-case Pinject₁[_] {i} n≢i with view i - ... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i - ... | ‵inject₁ j = Pinject₁[ j ] +data View : {i : Fin (suc n)} → n ≢ toℕ i → Set where + ‵inject₁ : (j : Fin n) {n≢j : n ≢ toℕ (inject₁ j)} → View n≢j + +view : {i : Fin (suc n)} (n≢i : n ≢ toℕ i) → View n≢i +view {i = i} n≢i with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ j = ‵inject₁ j ------------------------------------------------------------------------ --- Reimplementation of `Data.Fin.Base.lower₁` and its properties +-- Reimplementation of `Data.Fin.Base.lower₁` and its properties, +-- together with the streamlined version obtained from the view. --- definition of lower₁ +-- definition of lower₁/inject₁⁻¹ lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n -lower₁ i n≢i with view i -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | ‵inject₁ j = j +lower₁ i n≢i with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ j = j + +inject₁⁻¹ : ∀ (i : Fin (suc n)) → (n ≢ toℕ i) → Fin n +inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = j ------------------------------------------------------------------------ --- properties of lower₁ +-- properties of lower₁/inject₁⁻¹ toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i -toℕ-lower₁ i n≢i with view i -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | ‵inject₁ j = sym (toℕ-inject₁ j) +toℕ-lower₁ i n≢i with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ j = sym (toℕ-inject₁ j) + +toℕ-inject₁⁻¹ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (inject₁⁻¹ i n≢i) ≡ toℕ i +toℕ-inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = sym (toℕ-inject₁ 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 {i = i} {j = j} {n≢i} {n≢j} eq with view i -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | ‵inject₁ i₁ with view j -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j -... | ‵inject₁ j₁ = cong inject₁ eq +lower₁-injective {i = i} {j = j} {n≢i} {n≢j} eq with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ _ with Top.view j +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | Top.‵inject₁ _ = cong inject₁ eq + +inject₁⁻¹-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} → + inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j → i ≡ j +inject₁⁻¹-injective {i = i} {j = j} {n≢i} {n≢j} eq + with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = cong inject₁ eq lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant i n≢i₁ n≢i₂ with view i -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ -... | ‵inject₁ j = refl +lower₁-irrelevant i n≢i₁ n≢i₂ with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ +... | Top.‵inject₁ _ = refl + +-- here we need/use a helper function, in order to avoid having +-- to appeal to injectivity of inject₁ in the unifier +inject₁⁻¹-irrelevant′ : ∀ {i j : Fin (suc n)} (i≡j : i ≡ j) → + (n≢i : n ≢ toℕ i) (n≢j : n ≢ toℕ j) → + inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j +inject₁⁻¹-irrelevant′ eq n≢i n≢j + with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = inject₁-injective eq + +inject₁⁻¹-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + inject₁⁻¹ i n≢i₁ ≡ inject₁⁻¹ i n≢i₂ +inject₁⁻¹-irrelevant i = inject₁⁻¹-irrelevant′ refl ------------------------------------------------------------------------ --- inject₁ and lower₁ +-- inject₁ and lower₁/inject₁⁻¹ inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → inject₁ (lower₁ i n≢i) ≡ i -inject₁-lower₁ i n≢i with view i -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | ‵inject₁ j = refl +inject₁-lower₁ i n≢i with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ _ = refl -inject₁≡⇒lower₁≡ : {j : Fin (ℕ.suc n)} (n≢j : n ≢ toℕ j) → - inject₁ i ≡ j → lower₁ j n≢j ≡ i -inject₁≡⇒lower₁≡ {j = j} n≢j inject₁[i]≡j with view j -... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j -... | ‵inject₁ j₁ = sym (inject₁-injective inject₁[i]≡j) +inject₁-inject₁⁻¹ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → + inject₁ (inject₁⁻¹ i n≢i) ≡ i +inject₁-inject₁⁻¹ i n≢i with ‵inject₁ _ ← view n≢i = refl + +inject₁≡⇒lower₁≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → + inject₁ j ≡ i → lower₁ i n≢i ≡ j +inject₁≡⇒lower₁≡ {i = i} n≢i inject₁[j]≡i with Top.view i +... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | Top.‵inject₁ _ = sym (inject₁-injective inject₁[j]≡i) + +inject₁≡⇒inject₁⁻¹≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → + inject₁ j ≡ i → inject₁⁻¹ i n≢i ≡ j +inject₁≡⇒inject₁⁻¹≡ {i = i} n≢i inject₁[j]≡i with ‵inject₁ _ ← view n≢i + = sym (inject₁-injective inject₁[j]≡i) lower₁-inject₁ : ∀ (i : Fin n) → lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i lower₁-inject₁ {n} i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl +inject₁⁻¹-inject₁ : ∀ (i : Fin n) → + inject₁⁻¹ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i +inject₁⁻¹-inject₁ {n} i = inject₁≡⇒inject₁⁻¹≡ (toℕ-inject₁-≢ i) refl + diff --git a/src/Data/Fin/Relation/Unary/TopREVISED.agda b/src/Data/Fin/Relation/Unary/TopREVISED.agda deleted file mode 100644 index ae6f14ffa9..0000000000 --- a/src/Data/Fin/Relation/Unary/TopREVISED.agda +++ /dev/null @@ -1,83 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- The 'top' view of Fin. --- --- This is an example of a view of (elements of) a datatype, --- here i : Fin (suc n), which exhibits every such i as --- * either, i = fromℕ n --- * or, i = inject₁ j for a unique j : Fin n ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -module Data.Fin.Relation.Unary.TopREVISED where - -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁; toℕ) -open import Data.Fin.Properties using (toℕ-fromℕ) -open import Relation.Binary.PropositionalEquality.Core -open import Relation.Nullary.Negation.Core using (contradiction) -open import Relation.Unary using (Pred) - -private - variable - n : ℕ - i : Fin n - ------------------------------------------------------------------------- --- The View, considered as a unary relation on Fin n - --- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following --- inductively defined family on `Fin n` has constructors which target --- *disjoint* instances of the family (moreover at indices `n = suc _`); --- hence the interpretations of the View constructors will also be disjoint. - -data View : (i : Fin n) → Set where - ‵fromℕ : View (fromℕ n) - ‵inj₁ : View i → View (inject₁ i) - -pattern ‵inject₁ i = ‵inj₁ {i = i} _ - --- The view covering function, witnessing soundness of the view - -view : (i : Fin n) → View i -view zero = view-zero where - view-zero : View (zero {n}) - view-zero {n = zero} = ‵fromℕ - view-zero {n = suc _} = ‵inj₁ view-zero -view (suc i) with view i -... | ‵fromℕ = ‵fromℕ -... | ‵inject₁ j = ‵inj₁ (view (suc j)) - --- Interpretation of the view constructors - -⟦_⟧ : {i : Fin n} → View i → Fin n -⟦ ‵fromℕ ⟧ = fromℕ _ -⟦ ‵inject₁ i ⟧ = inject₁ i - --- Completeness of the view - -view-complete : (v : View i) → ⟦ v ⟧ ≡ i -view-complete ‵fromℕ = refl -view-complete (‵inject₁ _) = refl - --- 'Computational' behaviour of the covering function - -view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ -view-fromℕ zero = refl -view-fromℕ (suc n) rewrite view-fromℕ n = refl - -view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) -view-inject₁ zero = refl -view-inject₁ (suc i) rewrite view-inject₁ i = refl - --- Uniqueness of the view - -view-unique : (v : View i) → view i ≡ v -view-unique ‵fromℕ = view-fromℕ _ -view-unique (‵inj₁ {i = i} v) = begin - view (inject₁ i) ≡⟨ view-inject₁ i ⟩ - ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ - ‵inj₁ v ∎ where open ≡-Reasoning - From ef777ea0c16b83c346b67f9d66151abb3a86034e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 06:51:09 +0100 Subject: [PATCH 11/16] tidy up --- README/Data/Fin/Relation/Unary/Lower.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 7aff3bc812..254c9cf580 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -35,7 +35,7 @@ private i j : Fin n ------------------------------------------------------------------------ --- EXPERIMENTAL: Derived induction principles from the view, via another view! +-- Derived induction principles from the Top view, via another view! -- The idea being, that in what follows, a call pattern is repeated over -- and over again, so should be reified as induction over a revised view, @@ -52,7 +52,7 @@ view {i = i} n≢i with Top.view i ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.lower₁` and its properties, --- together with the streamlined version obtained from the view. +-- together with the streamlined versions obtained from the view. -- definition of lower₁/inject₁⁻¹ From 6eef39ef88c4cfd9411b7c35c90f3445683852be Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 10:32:14 +0100 Subject: [PATCH 12/16] tightened `import`s --- README/Data/Fin/Relation/Unary/Lower.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 254c9cf580..69c477d3ca 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -25,8 +25,7 @@ open import Data.Fin.Properties import Data.Fin.Relation.Unary.Top as Top open import Level using (Level) open import Relation.Nullary.Negation.Core using (contradiction) -open import Relation.Binary.PropositionalEquality -open import Relation.Unary using (Pred) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong) private variable From 967882257475719af222282c0ef3aafdd11c4a7d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 16:41:02 +0100 Subject: [PATCH 13/16] `Top` now completelyself-contained, and exports both views happily, with dependency on --- README/Data/Fin/Relation/Unary/Lower.agda | 70 +++++++++-------------- src/Data/Fin/Relation/Unary/Top.agda | 49 +++++++++++++++- 2 files changed, 75 insertions(+), 44 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 69c477d3ca..9a739eec5c 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -22,7 +22,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; pred) open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) -import Data.Fin.Relation.Unary.Top as Top +open import Data.Fin.Relation.Unary.Top using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) open import Level using (Level) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong) @@ -33,22 +33,6 @@ private n : ℕ i j : Fin n ------------------------------------------------------------------------- --- Derived induction principles from the Top view, via another view! - --- The idea being, that in what follows, a call pattern is repeated over --- and over again, so should be reified as induction over a revised view, --- obtained from `Top.view` by restricting the domain - -data View : {i : Fin (suc n)} → n ≢ toℕ i → Set where - ‵inject₁ : (j : Fin n) {n≢j : n ≢ toℕ (inject₁ j)} → View n≢j - -view : {i : Fin (suc n)} (n≢i : n ≢ toℕ i) → View n≢i -view {i = i} n≢i with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ j = ‵inject₁ j - - ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.lower₁` and its properties, -- together with the streamlined versions obtained from the view. @@ -56,42 +40,42 @@ view {i = i} n≢i with Top.view i -- definition of lower₁/inject₁⁻¹ lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n -lower₁ i n≢i with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ j = j +lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = j inject₁⁻¹ : ∀ (i : Fin (suc n)) → (n ≢ toℕ i) → Fin n -inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = j +inject₁⁻¹ i n≢i with ‵inj₁ j ← view≢ n≢i = j ------------------------------------------------------------------------ -- properties of lower₁/inject₁⁻¹ toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i -toℕ-lower₁ i n≢i with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ j = sym (toℕ-inject₁ j) +toℕ-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = sym (toℕ-inject₁ j) toℕ-inject₁⁻¹ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (inject₁⁻¹ i n≢i) ≡ toℕ i -toℕ-inject₁⁻¹ i n≢i with ‵inject₁ j ← view n≢i = sym (toℕ-inject₁ j) +toℕ-inject₁⁻¹ i n≢i with ‵inj₁ j ← view≢ n≢i = sym (toℕ-inject₁ 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 {i = i} {j = j} {n≢i} {n≢j} eq with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ _ with Top.view j -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j -... | Top.‵inject₁ _ = cong inject₁ eq +lower₁-injective {i = i} {j = j} {n≢i} {n≢j} eq with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ _ = cong inject₁ eq inject₁⁻¹-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} → inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j → i ≡ j inject₁⁻¹-injective {i = i} {j = j} {n≢i} {n≢j} eq - with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = cong inject₁ eq + with ‵inj₁ _ ← view≢ n≢i | ‵inj₁ _ ← view≢ n≢j = cong inject₁ eq lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant i n≢i₁ n≢i₂ with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ -... | Top.‵inject₁ _ = refl +lower₁-irrelevant i n≢i₁ n≢i₂ with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ +... | ‵inject₁ _ = refl -- here we need/use a helper function, in order to avoid having -- to appeal to injectivity of inject₁ in the unifier @@ -99,7 +83,7 @@ inject₁⁻¹-irrelevant′ : ∀ {i j : Fin (suc n)} (i≡j : i ≡ j) → (n≢i : n ≢ toℕ i) (n≢j : n ≢ toℕ j) → inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j inject₁⁻¹-irrelevant′ eq n≢i n≢j - with ‵inject₁ _ ← view n≢i | ‵inject₁ _ ← view n≢j = inject₁-injective eq + with ‵inj₁ _ ← view≢ n≢i | ‵inj₁ _ ← view≢ n≢j = inject₁-injective eq inject₁⁻¹-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → inject₁⁻¹ i n≢i₁ ≡ inject₁⁻¹ i n≢i₂ @@ -110,23 +94,23 @@ inject₁⁻¹-irrelevant i = inject₁⁻¹-irrelevant′ refl inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → inject₁ (lower₁ i n≢i) ≡ i -inject₁-lower₁ i n≢i with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ _ = refl +inject₁-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ = refl inject₁-inject₁⁻¹ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → inject₁ (inject₁⁻¹ i n≢i) ≡ i -inject₁-inject₁⁻¹ i n≢i with ‵inject₁ _ ← view n≢i = refl +inject₁-inject₁⁻¹ i n≢i with ‵inj₁ _ ← view≢ n≢i = refl inject₁≡⇒lower₁≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → inject₁ j ≡ i → lower₁ i n≢i ≡ j -inject₁≡⇒lower₁≡ {i = i} n≢i inject₁[j]≡i with Top.view i -... | Top.‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i -... | Top.‵inject₁ _ = sym (inject₁-injective inject₁[j]≡i) +inject₁≡⇒lower₁≡ {i = i} n≢i inject₁[j]≡i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ = sym (inject₁-injective inject₁[j]≡i) inject₁≡⇒inject₁⁻¹≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → inject₁ j ≡ i → inject₁⁻¹ i n≢i ≡ j -inject₁≡⇒inject₁⁻¹≡ {i = i} n≢i inject₁[j]≡i with ‵inject₁ _ ← view n≢i +inject₁≡⇒inject₁⁻¹≡ {i = i} n≢i inject₁[j]≡i with ‵inj₁ _ ← view≢ n≢i = sym (inject₁-injective inject₁[j]≡i) lower₁-inject₁ : ∀ (i : Fin n) → diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index b6a567a9a8..a9e425b855 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -14,8 +14,10 @@ module Data.Fin.Relation.Unary.Top where open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁) +open import Data.Fin.Base as Fin using (Fin; zero; suc; fromℕ; inject₁) +open import Function.Base using (_∘_) open import Relation.Binary.PropositionalEquality.Core +open import Relation.Nullary.Negation.Core using (contradiction) private variable @@ -77,3 +79,48 @@ view-unique (‵inj₁ {i = i} v) = begin view (inject₁ i) ≡⟨ view-inject₁ i ⟩ ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ ‵inj₁ v ∎ where open ≡-Reasoning + +-- An important distinguished observer and its properties + +toℕ : {i : Fin n} → View i → ℕ +toℕ (‵fromℕ {n}) = n +toℕ (‵inj₁ v) = toℕ v + +toℕ[view[suc]]≡suc[toℕ[view]] : (i : Fin n) → + toℕ (view (suc i)) ≡ suc (toℕ (view i)) +toℕ[view[suc]]≡suc[toℕ[view]] i with view i +... | ‵fromℕ {n} = refl +... | ‵inj₁ {i = j} v = trans (toℕ[view[suc]]≡suc[toℕ[view]] j) + (cong (suc ∘ toℕ) (view-unique v)) + +toℕ[view]≡Fin[toℕ] : (i : Fin n) → toℕ (view i) ≡ Fin.toℕ i +toℕ[view]≡Fin[toℕ] {n = suc n} zero = toℕ[view[zero]]≡Fin[toℕ[zero]] n + where + toℕ[view[zero]]≡Fin[toℕ[zero]] : ∀ n → toℕ (view (zero {n})) ≡ zero + toℕ[view[zero]]≡Fin[toℕ[zero]] zero = refl + toℕ[view[zero]]≡Fin[toℕ[zero]] (suc n) = toℕ[view[zero]]≡Fin[toℕ[zero]] n +toℕ[view]≡Fin[toℕ] {n = suc n} (suc i) + rewrite toℕ[view[suc]]≡suc[toℕ[view]] i = cong suc (toℕ[view]≡Fin[toℕ] i) + +-- independent reimplementation of Data.Fin.Properties.toℕ-fromℕ +n≡Fin[toℕ[fromℕ]] : ∀ n → n ≡ Fin.toℕ (fromℕ n) +n≡Fin[toℕ[fromℕ]] n = begin -- toℕ[view]≡Fin[toℕ] i + n ≡⟨⟩ + toℕ (‵fromℕ {n}) ≡⟨ sym (cong toℕ (view-fromℕ n)) ⟩ + toℕ (view (fromℕ n)) ≡⟨ toℕ[view]≡Fin[toℕ] (fromℕ n) ⟩ + Fin.toℕ (fromℕ n) ∎ where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Derived induction principle from the Top view, via another view! + +-- The idea being, that in what follows, a call pattern is repeated over +-- and over again, so should be reified as induction over a revised view, +-- `View≢`/`view≢`obtained from `View`/`view` by restricting the domain. + +data View≢ : {i : Fin (suc n)} → n ≢ Fin.toℕ i → Set where + ‵inj₁ : (j : Fin n) {n≢j : n ≢ Fin.toℕ (inject₁ j)} → View≢ n≢j + +view≢ : {i : Fin (suc n)} (n≢i : n ≢ Fin.toℕ i) → View≢ n≢i +view≢ {i = i} n≢ with view i +... | ‵fromℕ {n} = contradiction (n≡Fin[toℕ[fromℕ]] n) n≢ +... | ‵inject₁ j = ‵inj₁ j From 1630feb5c26f0e139522b8915941e4365ce2e12a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 17:46:18 +0100 Subject: [PATCH 14/16] tightened `import`s --- README/Data/Fin/Relation/Unary/Lower.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 9a739eec5c..e20ae326c4 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -18,11 +18,12 @@ module README.Data.Fin.Relation.Unary.Lower where -open import Data.Nat.Base using (ℕ; zero; suc; pred) +open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) -open import Data.Fin.Relation.Unary.Top using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) +open import Data.Fin.Relation.Unary.Top + using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) hiding (toℕ) open import Level using (Level) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong) From 066ba846e628d482361b1e5c67fe2aa2a03234f5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 17:47:02 +0100 Subject: [PATCH 15/16] tightened `import`s; oops --- README/Data/Fin/Relation/Unary/Lower.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index e20ae326c4..38be789126 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -23,7 +23,7 @@ open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) open import Data.Fin.Relation.Unary.Top - using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) hiding (toℕ) + using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) open import Level using (Level) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong) From 0cb8ff2d716dee48d45d21a97d95998e26af2d1e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 18 Sep 2023 17:52:35 +0100 Subject: [PATCH 16/16] no longer (very) provisional... --- README/Data/Fin/Relation/Unary/Lower.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda index 38be789126..f71b02cfa2 100644 --- a/README/Data/Fin/Relation/Unary/Lower.agda +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -12,8 +12,6 @@ -- together with their corresponding properties in `Data.Fin.Properties`. ------------------------------------------------------------------------ ---- NB this is a provisional commit, ahead of merging PR #1923 - {-# OPTIONS --cubical-compatible --safe #-} module README.Data.Fin.Relation.Unary.Lower where