From 75fa9d075e5965ed24c6bcbecf068c25e16c73b1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 9 Feb 2023 10:15:16 +0000 Subject: [PATCH 01/42] a view of `Fin (suc n)` --- CHANGELOG.md | 5 + src/Data/Fin/Relation/Unary/Top.agda | 194 +++++++++++++++++++++++++++ 2 files changed, 199 insertions(+) create mode 100644 src/Data/Fin/Relation/Unary/Top.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 93b707d2ba..4d787bb539 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1402,6 +1402,11 @@ New modules Data.Default ``` +* A small library defining a structurally inductive view of `Fin (suc n)`: + ``` + Data.Fin.Relation.Unary.Top + ``` + * A small library for a non-empty fresh list: ``` Data.List.Fresh.NonEmpty diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..41a45675b1 --- /dev/null +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,194 @@ +------------------------------------------------------------------------ +-- 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 --without-K --safe #-} + +module Data.Fin.Relation.Unary.Top where + +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Nat.Base as Nat +open import Data.Fin.Base as Fin + using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) +open import Data.Fin.Properties as Fin + using (suc-injective; inject₁-injective; toℕ-fromℕ; toℕ Date: Thu, 9 Feb 2023 11:22:49 +0000 Subject: [PATCH 02/42] documentation --- src/Data/Fin/Relation/Unary/Top.agda | 49 ++++++++++++++++------------ 1 file changed, 29 insertions(+), 20 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 41a45675b1..0bc8859343 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -2,7 +2,6 @@ -- 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 @@ -15,25 +14,29 @@ module Data.Fin.Relation.Unary.Top where open import Data.Empty using (⊥; ⊥-elim) -open import Data.Nat.Base as Nat -open import Data.Fin.Base as Fin - using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) +open import Data.Nat.Base using (ℕ; zero; suc; _<_) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) open import Data.Fin.Properties as Fin using (suc-injective; inject₁-injective; toℕ-fromℕ; toℕ Date: Thu, 9 Feb 2023 16:41:20 +0000 Subject: [PATCH 03/42] theory of `opposite` also --- src/Data/Fin/Relation/Unary/Top.agda | 56 +++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 0bc8859343..2c653b9cec 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -14,7 +14,8 @@ module Data.Fin.Relation.Unary.Top where open import Data.Empty using (⊥; ⊥-elim) -open import Data.Nat.Base using (ℕ; zero; suc; _<_) +open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_) +open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc) open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) open import Data.Fin.Properties as Fin using (suc-injective; inject₁-injective; toℕ-fromℕ; toℕ Date: Thu, 9 Feb 2023 16:44:16 +0000 Subject: [PATCH 04/42] tweak --- src/Data/Fin/Relation/Unary/Top.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 2c653b9cec..0df3b53b1a 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -144,7 +144,7 @@ private module Examples {n} where -- Similarly, we can redefine certain operations in `Data.Fin.Base`, -- together with their corresponding properties in `Data.Fin.Properties` --- Here: the reimplementation of the function `lower₁` and its properties, +-- First: the reimplementation of the function `lower₁` and its properties, -- specified as a partial inverse to `inject₁`, defined on the domain given -- by `n ≢ toℕ i`, equivalently `i ≢ from ℕ n`, ie `IsInj {n} (view i)` From d2173fbc359c0f444409632b17305582221612df Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 10 Feb 2023 17:53:19 +0000 Subject: [PATCH 05/42] first of Jacques' review changes --- CHANGELOG.md | 2 ++ src/Data/Fin/Properties.agda | 3 +++ 2 files changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4d787bb539..4ab0253eef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1918,6 +1918,8 @@ Other minor changes 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₁ : (j : Fin n) → fromℕ n ≢ inject₁ j ``` * Added new functions in `Data.Integer.Base`: diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 232a44a7bb..356b78df61 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -443,6 +443,9 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j) -- inject₁ ------------------------------------------------------------------------ +fromℕ≢inject₁ : (j : Fin n) → fromℕ n ≢ inject₁ j +fromℕ≢inject₁ (suc j) eq = fromℕ≢inject₁ j (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 = From 6e0c4bec97360a4e420aac696d11c4ad8e82e9c9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 10 Feb 2023 20:07:43 +0000 Subject: [PATCH 06/42] refactored according to Jacques' prescriptions; renamed the inverse --- README/Data/Fin/Relation/Unary/Top.agda | 126 +++++++++++++++++++++ src/Data/Fin/Relation/Unary/Top.agda | 139 +----------------------- 2 files changed, 132 insertions(+), 133 deletions(-) create mode 100644 README/Data/Fin/Relation/Unary/Top.agda diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..92d8d74f37 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,126 @@ +------------------------------------------------------------------------ +-- 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 --without-K --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) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) +open import Data.Fin.Properties using (toℕ-fromℕ; toℕ Date: Fri, 10 Feb 2023 20:28:27 +0000 Subject: [PATCH 07/42] fix whitespace --- README/Data/Fin/Relation/Unary/Top.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 92d8d74f37..cfff907f5a 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -36,7 +36,7 @@ private -- * pattern matching of the form `... inj j ← view {n} i` ensures that -- `i ≟ inject₁ j`, and hence that `j` is, *definitionally*, an image -- under a hypothetical inverse to `inject₁`; --- +-- -- * such patterns are irrefutable *precisely* when `i` is in the codomain -- of `inject₁`, which by property `fromℕ≢inject₁`, is equivalent to the -- condition `i ≢ fromℕ n`, or again equivalently, `toℕ i ≢ n`, each From a870d694f279a30ab221dac052a8138589de949c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 10 Feb 2023 22:13:58 +0000 Subject: [PATCH 08/42] tightened imports --- src/Data/Fin/Relation/Unary/Top.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index be792b4e53..51f3edc7da 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -18,7 +18,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_) open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc) open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) open import Data.Fin.Properties as Fin - using (suc-injective; inject₁-injective; toℕ-fromℕ; toℕ Date: Sat, 11 Feb 2023 11:46:07 +0000 Subject: [PATCH 09/42] tightened imports --- src/Data/Fin/Relation/Unary/Top.agda | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 51f3edc7da..fa727c9c5e 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -13,12 +13,11 @@ module Data.Fin.Relation.Unary.Top where -open import Data.Empty using (⊥; ⊥-elim) -open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_) -open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc) -open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; fromℕ<; inject₁) +open import Data.Empty using (⊥-elim) +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 as Fin - using (inject₁-injective; toℕ-fromℕ; toℕ Date: Sat, 11 Feb 2023 11:47:37 +0000 Subject: [PATCH 10/42] tightened imports --- src/Data/Fin/Relation/Unary/Top.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index fa727c9c5e..7ba0878403 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -17,7 +17,7 @@ open import Data.Empty using (⊥-elim) 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 as Fin - using (toℕ-fromℕ; toℕ Date: Sat, 11 Feb 2023 12:40:24 +0000 Subject: [PATCH 11/42] cosmetics --- README/Data/Fin/Relation/Unary/Top.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index cfff907f5a..28753b7513 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -55,12 +55,6 @@ inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view {n} i inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} inject₁⁻¹-irrelevant i with inj ii ← view i = refl -inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → - .{{ii₁ : IsInj (view {n} i₁)}} → - .{{ii₂ : IsInj (view {n} i₂)}} → - inject₁⁻¹ i₁ {{ii₁}} ≡ inject₁⁻¹ i₂ {{ii₂}} → i₁ ≡ i₂ -inject₁⁻¹-injective i₁ i₂ with inj _ ← view i₁ | inj _ ← view i₂ = cong inject₁ - inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view {n} i)}} → inject₁ (inject₁⁻¹ i {{ii}}) ≡ i inject₁-inject₁⁻¹ i with inj ii ← view i = refl @@ -72,6 +66,12 @@ inject₁≡⇒inject₁⁻¹≡ : ∀ {j : Fin n} {i : Fin (suc n)} (eq : injec inject₁⁻¹ i {{inject₁≡⁺ {eq = eq}}} ≡ j inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ +inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → + .{{ii₁ : IsInj (view {n} i₁)}} → + .{{ii₂ : IsInj (view {n} i₂)}} → + inject₁⁻¹ i₁ {{ii₁}} ≡ inject₁⁻¹ i₂ {{ii₂}} → i₁ ≡ i₂ +inject₁⁻¹-injective i₁ i₂ with inj _ ← view i₁ | inj _ ← view i₂ = cong inject₁ + toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view {n} i)}} → toℕ (inject₁⁻¹ i {{ii}}) ≡ toℕ i toℕ-inject₁⁻¹ i with inj j ← view i = sym (toℕ-inject₁ j) From 8eff5d637fcdc0abf61a0e0c948695c604878bbb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 11 Feb 2023 15:20:23 +0000 Subject: [PATCH 12/42] rmeoved redundant --- src/Data/Fin/Relation/Unary/Top.agda | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 7ba0878403..0d397e1c7e 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -119,11 +119,9 @@ open Instances public -- witnessed by, but can also serve as proxy replacements for, -- the corresponding properties in `Data.Fin.Properties` -module _ {n} where +view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n +view-top-toℕ {n = n} i with top ← view i = toℕ-fromℕ n - view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n - view-top-toℕ i with top ← view i = toℕ-fromℕ n - - view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n - view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j +view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n +view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j From 6576fe54209a90b4bc43354c7b9db197f84be544 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 11 Feb 2023 15:28:13 +0000 Subject: [PATCH 13/42] made `Instances` not public --- README/Data/Fin/Relation/Unary/Top.agda | 2 ++ src/Data/Fin/Relation/Unary/Top.agda | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 28753b7513..1c54f7042c 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -27,6 +27,8 @@ private variable n : ℕ +open Instances + ------------------------------------------------------------------------ -- Inverting inject₁ diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 0d397e1c7e..c4ca186d64 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -112,7 +112,7 @@ module Instances {n} where toℕ (inject₁ (fromℕ n)) ∎)) where open ≡-Reasoning ... | inj j = inj j -open Instances public +open Instances ------------------------------------------------------------------------ -- As a corollary, we obtain two useful properties, which are From c18173c633c46f04728452acb0c6cfd6c0893341 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 11 Feb 2023 15:54:09 +0000 Subject: [PATCH 14/42] slight refactor --- src/Data/Fin/Relation/Unary/Top.agda | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index c4ca186d64..c4863daf7c 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -13,7 +13,6 @@ module Data.Fin.Relation.Unary.Top where -open import Data.Empty using (⊥-elim) 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 as Fin @@ -83,6 +82,14 @@ view-inj (suc j) rewrite view-inj j = refl module Instances {n} where + private + + lemma : toℕ (inject₁ (fromℕ n)) ≡ n + lemma = begin + toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ + toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ + n ∎ where open ≡-Reasoning + data IsTop : ∀ {i} → View {n} i → Set where top : IsTop top @@ -106,10 +113,7 @@ module Instances {n} where inject₁≢n⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {n} i) inject₁≢n⁺ {i} {n≢i} with view i - ... | top = ⊥-elim (n≢i (begin - n ≡˘⟨ toℕ-fromℕ n ⟩ - toℕ (fromℕ n) ≡˘⟨ toℕ-inject₁ (fromℕ n) ⟩ - toℕ (inject₁ (fromℕ n)) ∎)) where open ≡-Reasoning + ... | top with () ← n≢i (sym lemma) ... | inj j = inj j open Instances From d4069e92390cfa2e92f1efc00f896171d93aa95e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 11 Feb 2023 15:55:38 +0000 Subject: [PATCH 15/42] symmetry typo --- src/Data/Fin/Relation/Unary/Top.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index c4863daf7c..81f4fa5d22 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -84,11 +84,11 @@ module Instances {n} where private - lemma : toℕ (inject₁ (fromℕ n)) ≡ n - lemma = begin + lemma : n ≡ toℕ (inject₁ (fromℕ n)) + lemma = sym (begin toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎ where open ≡-Reasoning + n ∎) where open ≡-Reasoning data IsTop : ∀ {i} → View {n} i → Set where @@ -113,7 +113,7 @@ module Instances {n} where inject₁≢n⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {n} i) inject₁≢n⁺ {i} {n≢i} with view i - ... | top with () ← n≢i (sym lemma) + ... | top with () ← n≢i lemma ... | inj j = inj j open Instances From 6d4cc58de7d337be7de41ffbd89564680518e41d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 11 Feb 2023 15:57:05 +0000 Subject: [PATCH 16/42] imports --- src/Data/Fin/Relation/Unary/Top.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 81f4fa5d22..7053b1e221 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -15,8 +15,7 @@ module Data.Fin.Relation.Unary.Top 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 as Fin - using (toℕ-fromℕ; toℕ-inject₁; inject₁ℕ<) +open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁; inject₁ℕ<) open import Relation.Binary.PropositionalEquality private From 0e6db5e639782bcd5822834531465a4865f665dc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 14 Feb 2023 16:42:02 +0000 Subject: [PATCH 17/42] =?UTF-8?q?other=20use=20of=20`lower=E2=82=81`=20in?= =?UTF-8?q?=20`Data.Fin.Induction`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Top.agda | 29 ++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 1c54f7042c..a767aaeed3 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -16,15 +16,20 @@ 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) -open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) +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 +open 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 : ℕ open Instances @@ -126,3 +131,21 @@ opposite-prop {suc n} i with view i n ∸ toℕ j ≡˘⟨ cong (n ∸_) (toℕ-inject₁ j) ⟩ n ∸ toℕ (inject₁ j) ∎ where open ≡-Reasoning +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Induction.>-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 {n = n} P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i) + where + induct : ∀ {i} → Acc _>_ i → P i + induct {i} (acc rec) with view i + ... | top = Pₙ + ... | inj j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) + where + inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) Data.Nat.Base.≤ toℕ (suc j) + inject₁[j]+1≤[j+1] = Data.Nat.Properties.≤-reflexive (toℕ-inject₁ (suc j)) From fa28f4c7ff472efa7bc0cdc10aa74ab3677b208f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 15 Feb 2023 10:13:50 +0000 Subject: [PATCH 18/42] previously uncommitted comment on the `View` itself --- src/Data/Fin/Relation/Unary/Top.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 7053b1e221..b68b7497f3 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -25,6 +25,11 @@ private ------------------------------------------------------------------------ -- The View, considered as a unary relation on Fin (suc n) +-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following +-- inductively defined family on `Fin (suc n)` has constructors which +-- target *disjoint* instances of the family; and hence the interpretations +-- of the View constructors will also be disjoint + data View : (i : Fin (suc n)) → Set where top : View (fromℕ n) From c51dd63901ed66b1f35d371dc53f1be129ec5fb9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 17 Apr 2023 17:49:31 +0100 Subject: [PATCH 19/42] tidied up imports for `Top` view --- README/Data/Fin/Relation/Unary/Top.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index a767aaeed3..786f0383b9 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -56,7 +56,7 @@ open Instances inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInj (view {n} i)}} → Fin n inject₁⁻¹ i with inj j ← view i = j --- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties +-- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties` inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view {n} i)}} → inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} @@ -147,5 +147,5 @@ open WF using (Acc; acc) ... | top = Pₙ ... | inj j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) where - inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) Data.Nat.Base.≤ toℕ (suc j) - inject₁[j]+1≤[j+1] = Data.Nat.Properties.≤-reflexive (toℕ-inject₁ (suc j)) + inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) ≤ toℕ (suc j) + inject₁[j]+1≤[j+1] = ≤-reflexive (toℕ-inject₁ (suc j)) From 904fdbed8502242632784adb48810eb3d26f829e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 17 Apr 2023 17:53:51 +0100 Subject: [PATCH 20/42] made `--cubical-compatible` --- README/Data/Fin/Relation/Unary/Top.agda | 2 +- src/Data/Fin/Relation/Unary/Top.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 786f0383b9..60aa372c94 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -12,7 +12,7 @@ -- together with their corresponding properties in `Data.Fin.Properties` ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module README.Data.Fin.Relation.Unary.Top where diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index b68b7497f3..63a35e2ae5 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -9,7 +9,7 @@ -- * or, i = inject₁ j for a unique j : Fin n ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Relation.Unary.Top where From f3550ade60a1936f31ec01949fe17c59d69dd494 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 12 May 2023 16:01:37 +0100 Subject: [PATCH 21/42] better use of `variable`s --- README/Data/Fin/Relation/Unary/Top.agda | 12 ++++--- src/Data/Fin/Relation/Unary/Top.agda | 42 +++++++++++++------------ 2 files changed, 29 insertions(+), 25 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 60aa372c94..a651974bcb 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -31,6 +31,8 @@ private variable ℓ : Level n : ℕ + i : Fin (suc n) + j : Fin n open Instances @@ -69,7 +71,7 @@ inject₁-inject₁⁻¹ i with inj ii ← view i = refl inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) {{inj⁺}} ≡ j inject₁⁻¹-inject₁ j rewrite view-inj j = refl -inject₁≡⇒inject₁⁻¹≡ : ∀ {j : Fin n} {i : Fin (suc n)} (eq : inject₁ j ≡ i) → +inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → inject₁⁻¹ i {{inject₁≡⁺ {eq = eq}}} ≡ j inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ @@ -88,7 +90,7 @@ toℕ-inject₁⁻¹ i with inj j ← view i = sym (toℕ-inject₁ j) -- Definition -opposite : ∀ {n} → Fin n → Fin n +opposite : Fin n → Fin n opposite {suc n} i with view i ... | top = zero ... | inj j = suc (opposite {n} j) @@ -102,13 +104,13 @@ opposite-zero≡top (suc n) = cong suc (opposite-zero≡top n) opposite-top≡zero : ∀ n → opposite {suc n} (fromℕ n) ≡ zero opposite-top≡zero n rewrite view-top n = refl -opposite-suc≡inject₁-opposite : ∀ {n} (j : Fin n) → +opposite-suc≡inject₁-opposite : (j : Fin n) → opposite (suc j) ≡ inject₁ (opposite j) opposite-suc≡inject₁-opposite {suc n} i with view i ... | top = refl ... | inj j = cong suc (opposite-suc≡inject₁-opposite {n} j) -opposite-involutive : ∀ {n} (j : Fin n) → opposite (opposite j) ≡ j +opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j opposite-involutive {suc n} zero rewrite opposite-zero≡top n | view-top n = refl @@ -122,7 +124,7 @@ opposite-suc j = begin toℕ (inject₁ (opposite j)) ≡⟨ toℕ-inject₁ (opposite j) ⟩ toℕ (opposite j) ∎ where open ≡-Reasoning -opposite-prop : ∀ {n} (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) +opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) opposite-prop {suc n} i with view i ... | top rewrite toℕ-fromℕ n | n∸n≡0 n = refl ... | inj j = begin diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 63a35e2ae5..586c2eb156 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -17,10 +17,13 @@ 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₁; inject₁ℕ<) open import Relation.Binary.PropositionalEquality +open import Relation.Nullary.Negation using (contradiction) private variable n : ℕ + i : Fin (suc n) + j : Fin n ------------------------------------------------------------------------ -- The View, considered as a unary relation on Fin (suc n) @@ -32,12 +35,12 @@ private data View : (i : Fin (suc n)) → Set where - top : View (fromℕ n) + top : View (fromℕ n) inj : (j : Fin n) → View (inject₁ j) -- The view covering function, witnessing soundness of the view -view : ∀ {n} i → View {n} i +view : ∀ i → View {n} i view {n = zero} zero = top view {n = suc _} zero = inj _ view {n = suc n} (suc i) with view {n} i @@ -46,13 +49,13 @@ view {n = suc n} (suc i) with view {n} i -- Interpretation of the view constructors -⟦_⟧ : ∀ {i} → View {n} i → Fin (suc n) +⟦_⟧ : View {n} i → Fin (suc n) ⟦ top ⟧ = fromℕ _ ⟦ inj j ⟧ = inject₁ j -- Completeness of the view -view-complete : ∀ {i} (v : View {n} i) → ⟦ v ⟧ ≡ i +view-complete : (v : View {n} i) → ⟦ v ⟧ ≡ i view-complete top = refl view-complete (inj j) = refl @@ -71,14 +74,14 @@ view-inj (suc j) rewrite view-inj j = refl -- -- Because we work --without-K, Agda's unifier will complain about -- attempts to match `refl` against hypotheses of the form --- `view {n] i ≡ v` +-- `view {n} i ≡ v` -- or gets stuck trying to solve unification problems of the form -- (inferred index ≟ expected index) -- even when these problems are *provably* solvable. -- -- So the two predicates on values of the view defined below -- are extensionally equivalent to the assertions --- `view {n] i ≡ top` and `view {n] i ≡ inj j` +-- `view {n} i ≡ top` and `view {n} i ≡ inj j` -- -- But such assertions can only ever have a unique (irrelevant) proof -- so we introduce instances to witness them, themselves given in @@ -86,15 +89,7 @@ view-inj (suc j) rewrite view-inj j = refl module Instances {n} where - private - - lemma : n ≡ toℕ (inject₁ (fromℕ n)) - lemma = sym (begin - toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ - toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎) where open ≡-Reasoning - - data IsTop : ∀ {i} → View {n} i → Set where + data IsTop : View {n} i → Set where top : IsTop top @@ -103,21 +98,28 @@ module Instances {n} where top⁺ : IsTop {i = fromℕ n} (view (fromℕ n)) top⁺ rewrite view-top n = top - data IsInj : ∀ {i} → View {n} i → Set where + data IsInj : View {n} i → Set where inj : ∀ j → IsInj (inj j) instance - inj⁺ : ∀ {j} → IsInj (view (inject₁ j)) + inj⁺ : IsInj (view (inject₁ j)) inj⁺ {j} rewrite view-inj j = inj j - inject₁≡⁺ : ∀ {i} {j} {eq : inject₁ i ≡ j} → IsInj (view j) + inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInj (view i) inject₁≡⁺ {eq = refl} = inj⁺ - inject₁≢n⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {n} i) + inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {n} i) inject₁≢n⁺ {i} {n≢i} with view i - ... | top with () ← n≢i lemma + ... | top = contradiction n≡i n≢i + where + open ≡-Reasoning + n≡i : n ≡ toℕ (inject₁ (fromℕ n)) + n≡i = sym (begin + toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ + toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ + n ∎) ... | inj j = inj j open Instances From 9a0d6ad1f1ba7387a4d612d41de77945438dc322 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 14 May 2023 09:23:01 +0100 Subject: [PATCH 22/42] (vertical) whitespace) --- src/Data/Fin/Relation/Unary/Top.agda | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 586c2eb156..ed91de3acb 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -34,7 +34,6 @@ private -- of the View constructors will also be disjoint data View : (i : Fin (suc n)) → Set where - top : View (fromℕ n) inj : (j : Fin n) → View (inject₁ j) @@ -90,7 +89,6 @@ view-inj (suc j) rewrite view-inj j = refl module Instances {n} where data IsTop : View {n} i → Set where - top : IsTop top instance @@ -99,7 +97,6 @@ module Instances {n} where top⁺ rewrite view-top n = top data IsInj : View {n} i → Set where - inj : ∀ j → IsInj (inj j) instance From 1dd382e37a45b601c1d8d40783785487497f3e78 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 7 Aug 2023 13:02:59 +0100 Subject: [PATCH 23/42] made the view recursive; with simplifications --- CHANGELOG.md | 2 +- README/Data/Fin/Relation/Unary/Top.agda | 36 +++++++------- src/Data/Fin/Relation/Unary/Top.agda | 65 +++++++++++++------------ 3 files changed, 54 insertions(+), 49 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4ab0253eef..38ed5db72f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1402,7 +1402,7 @@ New modules Data.Default ``` -* A small library defining a structurally inductive view of `Fin (suc n)`: +* A small library defining a structurally inductive view of `Fin n`: ``` Data.Fin.Relation.Unary.Top ``` diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index a651974bcb..76dc9234c4 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -9,7 +9,7 @@ -- * 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` +-- together with their corresponding properties in `Data.Fin.Properties`: ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -55,18 +55,18 @@ open Instances -- -- Rather than redefine `lower₁` of `Data.Fin.Base`, we instead define -inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInj (view {n} i)}} → Fin n -inject₁⁻¹ i with inj j ← view i = j +inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInj (view i)}} → Fin n +inject₁⁻¹ i with inj₁ j ← view i = j -- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties` -inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view {n} i)}} → +inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view i)}} → inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} -inject₁⁻¹-irrelevant i with inj ii ← view i = refl +inject₁⁻¹-irrelevant i with inj _ ← view i = refl -inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view {n} i)}} → +inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view i)}} → inject₁ (inject₁⁻¹ i {{ii}}) ≡ i -inject₁-inject₁⁻¹ i with inj ii ← view i = refl +inject₁-inject₁⁻¹ i with inj _ ← view i = refl inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) {{inj⁺}} ≡ j inject₁⁻¹-inject₁ j rewrite view-inj j = refl @@ -76,14 +76,14 @@ inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → - .{{ii₁ : IsInj (view {n} i₁)}} → - .{{ii₂ : IsInj (view {n} i₂)}} → + .{{ii₁ : IsInj (view i₁)}} → + .{{ii₂ : IsInj (view i₂)}} → inject₁⁻¹ i₁ {{ii₁}} ≡ inject₁⁻¹ i₂ {{ii₂}} → i₁ ≡ i₂ inject₁⁻¹-injective i₁ i₂ with inj _ ← view i₁ | inj _ ← view i₂ = cong inject₁ -toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view {n} i)}} → +toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view i)}} → toℕ (inject₁⁻¹ i {{ii}}) ≡ toℕ i -toℕ-inject₁⁻¹ i with inj j ← view i = sym (toℕ-inject₁ j) +toℕ-inject₁⁻¹ i with inj₁ j ← view i = sym (toℕ-inject₁ j) ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.opposite`, and its properties @@ -92,8 +92,8 @@ toℕ-inject₁⁻¹ i with inj j ← view i = sym (toℕ-inject₁ j) opposite : Fin n → Fin n opposite {suc n} i with view i -... | top = zero -... | inj j = suc (opposite {n} j) +... | top = zero +... | inj₁ j = suc (opposite {n} j) -- Properties @@ -107,8 +107,8 @@ opposite-top≡zero n rewrite view-top 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 -... | top = refl -... | inj j = cong suc (opposite-suc≡inject₁-opposite {n} j) +... | top = refl +... | inj₁ j = cong suc (opposite-suc≡inject₁-opposite {n} j) opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j opposite-involutive {suc n} zero @@ -126,8 +126,8 @@ opposite-suc j = begin opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) opposite-prop {suc n} i with view i -... | top rewrite toℕ-fromℕ n | n∸n≡0 n = refl -... | inj j = begin +... | top rewrite toℕ-fromℕ n | n∸n≡0 n = refl +... | inj₁ j = begin suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩ suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 {n} {suc (toℕ j)} (toℕ_ i → P i induct {i} (acc rec) with view i ... | top = Pₙ - ... | inj j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) + ... | inj₁ 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/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index ed91de3acb..0693fca885 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -16,7 +16,7 @@ module Data.Fin.Relation.Unary.Top 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₁; inject₁ℕ<) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core open import Relation.Nullary.Negation using (contradiction) private @@ -26,46 +26,51 @@ private j : Fin n ------------------------------------------------------------------------ --- The View, considered as a unary relation on Fin (suc 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 (suc n)` has constructors which --- target *disjoint* instances of the family; and hence the interpretations --- of the View constructors will also be disjoint +-- inductively defined family on `Fin n` has constructors which target +-- *disjoint* instances of the family (at index {suc n}); and hence the +-- interpretations of the View constructors will also be disjoint -data View : (i : Fin (suc n)) → Set where +data View : ∀ {n} (j : Fin n) → Set where top : View (fromℕ n) - inj : (j : Fin n) → View (inject₁ j) + inj : {j : Fin n} → View j → View (inject₁ j) + +pattern inj₁ {n} j = inj {n = n} {j = j} _ -- The view covering function, witnessing soundness of the view -view : ∀ i → View {n} i -view {n = zero} zero = top -view {n = suc _} zero = inj _ +view-zero : ∀ n → View {suc n} zero +view-zero zero = top +view-zero (suc n) = inj (view-zero n) + +view : ∀ j → View {n} j +view {n = suc n} zero = view-zero n view {n = suc n} (suc i) with view {n} i -... | top = top -... | inj j = inj (suc j) +... | top = top +... | inj₁ j = inj (view (suc j)) -- Interpretation of the view constructors -⟦_⟧ : View {n} i → Fin (suc n) -⟦ top ⟧ = fromℕ _ -⟦ inj j ⟧ = inject₁ j +⟦_⟧ : View {n} j → Fin n +⟦ top ⟧ = fromℕ _ +⟦ inj₁ j ⟧ = inject₁ j -- Completeness of the view -view-complete : (v : View {n} i) → ⟦ v ⟧ ≡ i +view-complete : (v : View {n} j) → ⟦ v ⟧ ≡ j view-complete top = refl -view-complete (inj j) = refl +view-complete (inj _) = refl -- 'Computational' behaviour of the covering function -view-top : ∀ n → view {n} (fromℕ n) ≡ top -view-top zero = refl +view-top : ∀ n → view (fromℕ n) ≡ top +view-top zero = refl view-top (suc n) rewrite view-top n = refl -view-inj : ∀ j → view {n} (inject₁ j) ≡ inj j -view-inj zero = refl +view-inj : ∀ j → view (inject₁ j) ≡ inj (view {n} j) +view-inj zero = refl view-inj (suc j) rewrite view-inj j = refl ------------------------------------------------------------------------ @@ -80,7 +85,7 @@ view-inj (suc j) rewrite view-inj j = refl -- -- So the two predicates on values of the view defined below -- are extensionally equivalent to the assertions --- `view {n} i ≡ top` and `view {n} i ≡ inj j` +-- `view {n} i ≡ top` and `view {n} i ≡ inj₁ j` -- -- But such assertions can only ever have a unique (irrelevant) proof -- so we introduce instances to witness them, themselves given in @@ -88,26 +93,26 @@ view-inj (suc j) rewrite view-inj j = refl module Instances {n} where - data IsTop : View {n} i → Set where + data IsTop : View {suc n} i → Set where top : IsTop top instance - top⁺ : IsTop {i = fromℕ n} (view (fromℕ n)) + top⁺ : IsTop (view (fromℕ n)) top⁺ rewrite view-top n = top - data IsInj : View {n} i → Set where - inj : ∀ j → IsInj (inj j) + data IsInj : View {suc n} i → Set where + inj : ∀ {j} (v : View {n} j) → IsInj (inj v) instance inj⁺ : IsInj (view (inject₁ j)) - inj⁺ {j} rewrite view-inj j = inj j + inj⁺ {j} rewrite view-inj j = inj _ inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInj (view i) inject₁≡⁺ {eq = refl} = inj⁺ - inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {n} i) + inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view i) inject₁≢n⁺ {i} {n≢i} with view i ... | top = contradiction n≡i n≢i where @@ -117,7 +122,7 @@ module Instances {n} where toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ n ∎) - ... | inj j = inj j + ... | inj v = inj v open Instances @@ -130,5 +135,5 @@ view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n view-top-toℕ {n = n} i with top ← view i = toℕ-fromℕ n view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n -view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j +view-inj-toℕ< i with inj₁ j ← view i = inject₁ℕ< j From f10cb3f213a34dc7bb7925c9a8e01cea142dbd3a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 7 Aug 2023 13:24:57 +0100 Subject: [PATCH 24/42] final tweaks; use of variable `{n}` still needed in places --- CHANGELOG.md | 2 +- src/Data/Fin/Relation/Unary/Top.agda | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 38ed5db72f..6cca33ee22 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1402,7 +1402,7 @@ New modules Data.Default ``` -* A small library defining a structurally inductive view of `Fin n`: +* A small library defining a structurally recursive view of `Fin n`: ``` Data.Fin.Relation.Unary.Top ``` diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 0693fca885..9c06aa8d72 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -46,8 +46,8 @@ view-zero zero = top view-zero (suc n) = inj (view-zero n) view : ∀ j → View {n} j -view {n = suc n} zero = view-zero n -view {n = suc n} (suc i) with view {n} i +view zero = view-zero _ +view (suc i) with view i ... | top = top ... | inj₁ j = inj (view (suc j)) @@ -59,7 +59,7 @@ view {n = suc n} (suc i) with view {n} i -- Completeness of the view -view-complete : (v : View {n} j) → ⟦ v ⟧ ≡ j +view-complete : (v : View j) → ⟦ v ⟧ ≡ j view-complete top = refl view-complete (inj _) = refl @@ -69,7 +69,7 @@ view-top : ∀ n → view (fromℕ n) ≡ top view-top zero = refl view-top (suc n) rewrite view-top n = refl -view-inj : ∀ j → view (inject₁ j) ≡ inj (view {n} j) +view-inj : ∀ j → view {suc n} (inject₁ j) ≡ inj (view j) view-inj zero = refl view-inj (suc j) rewrite view-inj j = refl @@ -85,7 +85,7 @@ view-inj (suc j) rewrite view-inj j = refl -- -- So the two predicates on values of the view defined below -- are extensionally equivalent to the assertions --- `view {n} i ≡ top` and `view {n} i ≡ inj₁ j` +-- `view {suc n} i ≡ top` and `view {suc n} i ≡ inj₁ j` -- -- But such assertions can only ever have a unique (irrelevant) proof -- so we introduce instances to witness them, themselves given in From d878b2c408b38a33250ca41324cfacd32b82016c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 7 Aug 2023 13:44:13 +0100 Subject: [PATCH 25/42] streamlined use of instances --- README/Data/Fin/Relation/Unary/Top.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 76dc9234c4..de133bfb41 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -64,8 +64,8 @@ inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view i)}} inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} inject₁⁻¹-irrelevant i with inj _ ← view i = refl -inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view i)}} → - inject₁ (inject₁⁻¹ i {{ii}}) ≡ i +inject₁-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInj (view i)}} → + inject₁ (inject₁⁻¹ i) ≡ i inject₁-inject₁⁻¹ i with inj _ ← view i = refl inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) {{inj⁺}} ≡ j @@ -76,13 +76,13 @@ inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → - .{{ii₁ : IsInj (view i₁)}} → - .{{ii₂ : IsInj (view i₂)}} → - inject₁⁻¹ i₁ {{ii₁}} ≡ inject₁⁻¹ i₂ {{ii₂}} → i₁ ≡ i₂ + .{{_ : IsInj (view i₁)}} → + .{{_ : IsInj (view i₂)}} → + inject₁⁻¹ i₁ ≡ inject₁⁻¹ i₂ → i₁ ≡ i₂ inject₁⁻¹-injective i₁ i₂ with inj _ ← view i₁ | inj _ ← view i₂ = cong inject₁ -toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{ii : IsInj (view i)}} → - toℕ (inject₁⁻¹ i {{ii}}) ≡ toℕ i +toℕ-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInj (view i)}} → + toℕ (inject₁⁻¹ i) ≡ toℕ i toℕ-inject₁⁻¹ i with inj₁ j ← view i = sym (toℕ-inject₁ j) ------------------------------------------------------------------------ From c0d5651047e8eb168e64c83317b84e2c74ec0bd6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 8 Aug 2023 10:41:22 +0100 Subject: [PATCH 26/42] revised names, as per discusison --- src/Data/Fin/Relation/Unary/Top.agda | 83 ++++++++++++++-------------- 1 file changed, 42 insertions(+), 41 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 9c06aa8d72..e0812b7df1 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -16,7 +16,7 @@ module Data.Fin.Relation.Unary.Top 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₁; inject₁ℕ<) -open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Negation using (contradiction) private @@ -26,52 +26,52 @@ private j : Fin n ------------------------------------------------------------------------ --- The View, considered as a unary relation on Fin n +-- The View, considered as a unary relation on Fin (suc 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 (at index {suc n}); and hence the --- interpretations of the View constructors will also be disjoint +-- inductively defined family on `Fin (suc n)` has constructors which +-- target *disjoint* instances of the family; and hence the interpretations +-- of the View constructors will also be disjoint data View : ∀ {n} (j : Fin n) → Set where - top : View (fromℕ n) - inj : {j : Fin n} → View j → View (inject₁ j) + ‵fromℕ : View (fromℕ n) + ‵inj₁ : {j : Fin n} → View j → View (inject₁ j) -pattern inj₁ {n} j = inj {n = n} {j = j} _ +pattern ‵inject₁ {n} j = ‵inj₁ {n = n} {j = j} _ -- The view covering function, witnessing soundness of the view view-zero : ∀ n → View {suc n} zero -view-zero zero = top -view-zero (suc n) = inj (view-zero n) +view-zero zero = ‵fromℕ +view-zero (suc n) = ‵inj₁ (view-zero n) view : ∀ j → View {n} j -view zero = view-zero _ -view (suc i) with view i -... | top = top -... | inj₁ j = inj (view (suc j)) +view {n = suc n} zero = view-zero n +view {n = suc n} (suc i) with view {n} i +... | ‵fromℕ = ‵fromℕ +... | ‵inject₁ j = ‵inj₁ (view (suc j)) -- Interpretation of the view constructors ⟦_⟧ : View {n} j → Fin n -⟦ top ⟧ = fromℕ _ -⟦ inj₁ j ⟧ = inject₁ j +⟦ ‵fromℕ ⟧ = fromℕ _ +⟦ ‵inject₁ j ⟧ = inject₁ j -- Completeness of the view -view-complete : (v : View j) → ⟦ v ⟧ ≡ j -view-complete top = refl -view-complete (inj _) = refl +view-complete : (v : View {n} j) → ⟦ v ⟧ ≡ j +view-complete ‵fromℕ = refl +view-complete (‵inj₁ _) = refl -- 'Computational' behaviour of the covering function -view-top : ∀ n → view (fromℕ n) ≡ top -view-top zero = refl -view-top (suc n) rewrite view-top n = refl +view-fromℕ : ∀ n → view {suc n} (fromℕ n) ≡ ‵fromℕ +view-fromℕ zero = refl +view-fromℕ (suc n) rewrite view-fromℕ n = refl -view-inj : ∀ j → view {suc n} (inject₁ j) ≡ inj (view j) -view-inj zero = refl -view-inj (suc j) rewrite view-inj j = refl +view-inject₁ : ∀ j → view {suc n} (inject₁ j) ≡ ‵inj₁ (view {n} j) +view-inject₁ zero = refl +view-inject₁ (suc j) rewrite view-inject₁ j = refl ------------------------------------------------------------------------ -- Experimental @@ -85,36 +85,36 @@ view-inj (suc j) rewrite view-inj j = refl -- -- So the two predicates on values of the view defined below -- are extensionally equivalent to the assertions --- `view {suc n} i ≡ top` and `view {suc n} i ≡ inj₁ j` +-- `view {n} i ≡ ‵fromℕ` and `view {n} i ≡ ‵inject₁ j` -- -- But such assertions can only ever have a unique (irrelevant) proof -- so we introduce instances to witness them, themselves given in --- terms of the functions `view-top` and `view-inj` defined above +-- terms of the functions `view-fromℕ` and `view-inject₁` defined above module Instances {n} where - data IsTop : View {suc n} i → Set where - top : IsTop top + data IsFromℕ : View {suc n} i → Set where + ‵fromℕ : IsFromℕ ‵fromℕ instance - top⁺ : IsTop (view (fromℕ n)) - top⁺ rewrite view-top n = top + ‵fromℕ⁺ : IsFromℕ (view (fromℕ n)) + ‵fromℕ⁺ rewrite view-fromℕ n = ‵fromℕ data IsInj : View {suc n} i → Set where - inj : ∀ {j} (v : View {n} j) → IsInj (inj v) + ‵inj₁ : ∀ {j} (v : View {n} j) → IsInj (‵inj₁ v) instance inj⁺ : IsInj (view (inject₁ j)) - inj⁺ {j} rewrite view-inj j = inj _ + inj⁺ {j} rewrite view-inject₁ j = ‵inj₁ _ inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInj (view i) inject₁≡⁺ {eq = refl} = inj⁺ - inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view i) + inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {suc n} i) inject₁≢n⁺ {i} {n≢i} with view i - ... | top = contradiction n≡i n≢i + ... | ‵fromℕ = contradiction n≡i n≢i where open ≡-Reasoning n≡i : n ≡ toℕ (inject₁ (fromℕ n)) @@ -122,7 +122,9 @@ module Instances {n} where toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ n ∎) - ... | inj v = inj v + ... | ‵inj₁ v = ‵inj₁ v + + open Instances @@ -131,9 +133,8 @@ open Instances -- witnessed by, but can also serve as proxy replacements for, -- the corresponding properties in `Data.Fin.Properties` -view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n -view-top-toℕ {n = n} i with top ← view i = toℕ-fromℕ n - -view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n -view-inj-toℕ< i with inj₁ j ← view i = inject₁ℕ< j +view-fromℕ-toℕ : ∀ i → .{{IsFromℕ (view i)}} → toℕ i ≡ n +view-fromℕ-toℕ {n = n} i with ‵fromℕ ← view i = toℕ-fromℕ n +view-inject₁-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n +view-inject₁-toℕ< i with ‵inject₁ j ← view i = inject₁ℕ< j From 2c9442797e084b3d47067bf1c91ac1ef5713d23b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 8 Aug 2023 11:01:10 +0100 Subject: [PATCH 27/42] factored out `Instances`; revised `README` and `CHANGELOG` --- CHANGELOG.md | 1 + README/Data/Fin/Relation/Unary/Top.agda | 61 +++++++------ src/Data/Fin/Relation/Unary/Top.agda | 66 -------------- .../Fin/Relation/Unary/Top/Instances.agda | 89 +++++++++++++++++++ 4 files changed, 120 insertions(+), 97 deletions(-) create mode 100644 src/Data/Fin/Relation/Unary/Top/Instances.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 6cca33ee22..44bd20501e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1405,6 +1405,7 @@ New modules * A small library defining a structurally recursive view of `Fin n`: ``` Data.Fin.Relation.Unary.Top + Data.Fin.Relation.Unary.Top.Instances ``` * A small library for a non-empty fresh list: diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index de133bfb41..88d0f137b3 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -22,6 +22,7 @@ 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 +open import Data.Fin.Relation.Unary.Top.Instances open import Induction.WellFounded as WF open import Level using (Level) open import Relation.Binary.PropositionalEquality @@ -34,8 +35,6 @@ private i : Fin (suc n) j : Fin n -open Instances - ------------------------------------------------------------------------ -- Inverting inject₁ @@ -49,41 +48,41 @@ open Instances -- * such patterns are irrefutable *precisely* when `i` is in the codomain -- of `inject₁`, which by property `fromℕ≢inject₁`, is equivalent to the -- condition `i ≢ fromℕ n`, or again equivalently, `toℕ i ≢ n`, each --- equivalent to `IsInj {n} (view i)`, hence amenable to instance resolution +-- equivalent to `IsInject₁ {n} (view i)`, hence amenable to instance resolution -- -- Definition -- -- Rather than redefine `lower₁` of `Data.Fin.Base`, we instead define -inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInj (view i)}} → Fin n -inject₁⁻¹ i with inj₁ j ← view i = j +inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInject₁ (view i)}} → Fin n +inject₁⁻¹ i with ‵inject₁ j ← view i = j -- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties` -inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInj (view i)}} → +inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view i)}} → inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} -inject₁⁻¹-irrelevant i with inj _ ← view i = refl +inject₁⁻¹-irrelevant i with ‵inj₁_ ← view i = refl -inject₁-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInj (view i)}} → +inject₁-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInject₁ (view i)}} → inject₁ (inject₁⁻¹ i) ≡ i -inject₁-inject₁⁻¹ i with inj _ ← view i = refl +inject₁-inject₁⁻¹ i with ‵inj₁ _ ← view i = refl inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) {{inj⁺}} ≡ j -inject₁⁻¹-inject₁ j rewrite view-inj j = refl +inject₁⁻¹-inject₁ j rewrite view-inject₁ j = refl inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → inject₁⁻¹ i {{inject₁≡⁺ {eq = eq}}} ≡ j inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → - .{{_ : IsInj (view i₁)}} → - .{{_ : IsInj (view i₂)}} → + .{{_ : IsInject₁ (view i₁)}} → + .{{_ : IsInject₁ (view i₂)}} → inject₁⁻¹ i₁ ≡ inject₁⁻¹ i₂ → i₁ ≡ i₂ -inject₁⁻¹-injective i₁ i₂ with inj _ ← view i₁ | inj _ ← view i₂ = cong inject₁ +inject₁⁻¹-injective i₁ i₂ with ‵inj₁ _ ← view i₁ | ‵inj₁ _ ← view i₂ = cong inject₁ -toℕ-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInj (view i)}} → +toℕ-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInject₁ (view i)}} → toℕ (inject₁⁻¹ i) ≡ toℕ i -toℕ-inject₁⁻¹ i with inj₁ j ← view i = sym (toℕ-inject₁ j) +toℕ-inject₁⁻¹ i with ‵inject₁ j ← view i = sym (toℕ-inject₁ j) ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.opposite`, and its properties @@ -92,31 +91,31 @@ toℕ-inject₁⁻¹ i with inj₁ j ← view i = sym (toℕ-inject₁ j) opposite : Fin n → Fin n opposite {suc n} i with view i -... | top = zero -... | inj₁ j = suc (opposite {n} j) +... | ‵fromℕ = zero +... | ‵inject₁ j = suc (opposite {n} j) -- Properties -opposite-zero≡top : ∀ n → opposite {suc n} zero ≡ fromℕ n -opposite-zero≡top zero = refl -opposite-zero≡top (suc n) = cong suc (opposite-zero≡top n) +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-top≡zero : ∀ n → opposite {suc n} (fromℕ n) ≡ zero -opposite-top≡zero n rewrite view-top n = refl +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 -... | top = refl -... | inj₁ j = cong suc (opposite-suc≡inject₁-opposite {n} j) +... | ‵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≡top n - | view-top n = refl + rewrite opposite-zero≡fromℕ n + | view-fromℕ n = refl opposite-involutive {suc n} (suc i) rewrite opposite-suc≡inject₁-opposite i - | view-inj (opposite i) = cong suc (opposite-involutive 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 @@ -126,8 +125,8 @@ opposite-suc j = begin opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) opposite-prop {suc n} i with view i -... | top rewrite toℕ-fromℕ n | n∸n≡0 n = refl -... | inj₁ j = begin +... | ‵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 {n} {suc (toℕ j)} (toℕ_ i → P i induct {i} (acc rec) with view i - ... | top = Pₙ - ... | inj₁ j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) + ... | ‵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/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index e0812b7df1..2d54b57976 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -72,69 +72,3 @@ view-fromℕ (suc n) rewrite view-fromℕ n = refl view-inject₁ : ∀ j → view {suc n} (inject₁ j) ≡ ‵inj₁ (view {n} j) view-inject₁ zero = refl view-inject₁ (suc j) rewrite view-inject₁ j = refl - ------------------------------------------------------------------------- --- Experimental --- --- Because we work --without-K, Agda's unifier will complain about --- attempts to match `refl` against hypotheses of the form --- `view {n} i ≡ v` --- or gets stuck trying to solve unification problems of the form --- (inferred index ≟ expected index) --- even when these problems are *provably* solvable. --- --- So the two predicates on values of the view defined below --- are extensionally equivalent to the assertions --- `view {n} i ≡ ‵fromℕ` and `view {n} i ≡ ‵inject₁ j` --- --- But such assertions can only ever have a unique (irrelevant) proof --- so we introduce instances to witness them, themselves given in --- terms of the functions `view-fromℕ` and `view-inject₁` defined above - -module Instances {n} where - - data IsFromℕ : View {suc n} i → Set where - ‵fromℕ : IsFromℕ ‵fromℕ - - instance - - ‵fromℕ⁺ : IsFromℕ (view (fromℕ n)) - ‵fromℕ⁺ rewrite view-fromℕ n = ‵fromℕ - - data IsInj : View {suc n} i → Set where - ‵inj₁ : ∀ {j} (v : View {n} j) → IsInj (‵inj₁ v) - - instance - - inj⁺ : IsInj (view (inject₁ j)) - inj⁺ {j} rewrite view-inject₁ j = ‵inj₁ _ - - inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInj (view i) - inject₁≡⁺ {eq = refl} = inj⁺ - - inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view {suc n} i) - inject₁≢n⁺ {i} {n≢i} with view i - ... | ‵fromℕ = contradiction n≡i n≢i - where - open ≡-Reasoning - n≡i : n ≡ toℕ (inject₁ (fromℕ n)) - n≡i = sym (begin - toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ - toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎) - ... | ‵inj₁ v = ‵inj₁ v - - - -open Instances - ------------------------------------------------------------------------- --- As a corollary, we obtain two useful properties, which are --- witnessed by, but can also serve as proxy replacements for, --- the corresponding properties in `Data.Fin.Properties` - -view-fromℕ-toℕ : ∀ i → .{{IsFromℕ (view i)}} → toℕ i ≡ n -view-fromℕ-toℕ {n = n} i with ‵fromℕ ← view i = toℕ-fromℕ n - -view-inject₁-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n -view-inject₁-toℕ< i with ‵inject₁ j ← view i = inject₁ℕ< j diff --git a/src/Data/Fin/Relation/Unary/Top/Instances.agda b/src/Data/Fin/Relation/Unary/Top/Instances.agda new file mode 100644 index 0000000000..f02cb4633e --- /dev/null +++ b/src/Data/Fin/Relation/Unary/Top/Instances.agda @@ -0,0 +1,89 @@ +------------------------------------------------------------------------ +-- 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.Instances 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₁; inject₁ℕ<) +open import Data.Fin.Relation.Unary.Top +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Nullary.Negation using (contradiction) + +private + variable + n : ℕ + i : Fin (suc n) + j : Fin n + +------------------------------------------------------------------------ +-- Experimental +-- +-- Because we work --without-K, Agda's unifier will complain about +-- attempts to match `refl` against hypotheses of the form +-- `view {n} i ≡ v` +-- or gets stuck trying to solve unification problems of the form +-- (inferred index ≟ expected index) +-- even when these problems are *provably* solvable. +-- +-- So the two predicates on values of the view defined below +-- are extensionally equivalent to the assertions +-- `view {n} i ≡ ‵fromℕ` and `view {n} i ≡ ‵inject₁ j` +-- +-- But such assertions can only ever have a unique (irrelevant) proof +-- so we introduce instances to witness them, themselves given in +-- terms of the functions `view-fromℕ` and `view-inject₁` defined in +-- `Data.Fin.Relation.Unary.Top` + +data IsFromℕ : View {suc n} i → Set where + ‵fromℕ : IsFromℕ (‵fromℕ {n}) + +instance + + ‵fromℕ⁺ : IsFromℕ (view (fromℕ n)) + ‵fromℕ⁺ {n = n} rewrite view-fromℕ n = ‵fromℕ + +data IsInject₁ : View {suc n} i → Set where + ‵inj₁ : ∀ {j} (v : View {n} j) → IsInject₁ (‵inj₁ v) + +instance + + inj⁺ : IsInject₁ (view (inject₁ j)) + inj⁺ {j = j} rewrite view-inject₁ j = ‵inj₁ _ + + inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInject₁ (view i) + inject₁≡⁺ {eq = refl} = inj⁺ + + inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInject₁ (view {suc n} i) + inject₁≢n⁺ {n} {i} {n≢i} with view i + ... | ‵fromℕ = contradiction n≡i n≢i + where + open ≡-Reasoning + n≡i : n ≡ toℕ (inject₁ (fromℕ n)) + n≡i = sym (begin + toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ + toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ + n ∎) + ... | ‵inj₁ v = ‵inj₁ v + + +------------------------------------------------------------------------ +-- As corollaries, we obtain two useful properties, which are +-- witnessed by, but can also serve as proxy replacements for, +-- the corresponding properties in `Data.Fin.Properties` + +view-fromℕ-toℕ : ∀ i → .{{IsFromℕ (view i)}} → toℕ i ≡ n +view-fromℕ-toℕ {n = n} i with ‵fromℕ ← view i = toℕ-fromℕ n + +view-inject₁-toℕ< : ∀ i → .{{IsInject₁ (view i)}} → toℕ i < n +view-inject₁-toℕ< i with ‵inject₁ j ← view i = inject₁ℕ< j From 9bce07e1a4427c37624915a633ba5ad0c7f875e0 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 8 Aug 2023 12:25:32 +0100 Subject: [PATCH 28/42] followed Matthew's suggestion better; added uniqueness proof for the view; cosmetic tweaks --- src/Data/Fin/Relation/Unary/Top.agda | 18 ++++++++++++++---- src/Data/Fin/Relation/Unary/Top/Instances.agda | 18 +++++++++--------- 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 2d54b57976..87eab8225d 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -16,7 +16,7 @@ module Data.Fin.Relation.Unary.Top 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₁; inject₁ℕ<) -open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Core open import Relation.Nullary.Negation using (contradiction) private @@ -45,9 +45,9 @@ view-zero : ∀ n → View {suc n} zero view-zero zero = ‵fromℕ view-zero (suc n) = ‵inj₁ (view-zero n) -view : ∀ j → View {n} j -view {n = suc n} zero = view-zero n -view {n = suc n} (suc i) with view {n} i +view : (j : Fin n) → View j +view zero = view-zero _ +view (suc i) with view i ... | ‵fromℕ = ‵fromℕ ... | ‵inject₁ j = ‵inj₁ (view (suc j)) @@ -72,3 +72,13 @@ view-fromℕ (suc n) rewrite view-fromℕ n = refl view-inject₁ : ∀ j → view {suc n} (inject₁ j) ≡ ‵inj₁ (view {n} j) view-inject₁ zero = refl view-inject₁ (suc j) rewrite view-inject₁ j = refl + +-- Uniqeness of the view + +view-unique : (v : View {n} j) → view j ≡ v +view-unique ‵fromℕ = view-fromℕ _ +view-unique (‵inj₁ {j = j} v) = begin + view (inject₁ j) ≡⟨ view-inject₁ j ⟩ + ‵inj₁ (view j) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ + ‵inj₁ v ∎ where open ≡-Reasoning + diff --git a/src/Data/Fin/Relation/Unary/Top/Instances.agda b/src/Data/Fin/Relation/Unary/Top/Instances.agda index f02cb4633e..f25d87871b 100644 --- a/src/Data/Fin/Relation/Unary/Top/Instances.agda +++ b/src/Data/Fin/Relation/Unary/Top/Instances.agda @@ -50,30 +50,30 @@ data IsFromℕ : View {suc n} i → Set where instance - ‵fromℕ⁺ : IsFromℕ (view (fromℕ n)) - ‵fromℕ⁺ {n = n} rewrite view-fromℕ n = ‵fromℕ + fromℕ⁺ : IsFromℕ (view (fromℕ n)) + fromℕ⁺ {n = n} rewrite view-fromℕ n = ‵fromℕ data IsInject₁ : View {suc n} i → Set where ‵inj₁ : ∀ {j} (v : View {n} j) → IsInject₁ (‵inj₁ v) instance - inj⁺ : IsInject₁ (view (inject₁ j)) - inj⁺ {j = j} rewrite view-inject₁ j = ‵inj₁ _ + inject₁⁺ : IsInject₁ (view (inject₁ j)) + inject₁⁺ {j = j} rewrite view-inject₁ j = ‵inj₁ _ inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInject₁ (view i) - inject₁≡⁺ {eq = refl} = inj⁺ + inject₁≡⁺ {eq = refl} = inject₁⁺ inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInject₁ (view {suc n} i) inject₁≢n⁺ {n} {i} {n≢i} with view i - ... | ‵fromℕ = contradiction n≡i n≢i + ... | ‵fromℕ = contradiction (sym i≡n) n≢i where open ≡-Reasoning - n≡i : n ≡ toℕ (inject₁ (fromℕ n)) - n≡i = sym (begin + i≡n : toℕ (inject₁ (fromℕ n)) ≡ n + i≡n = begin toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎) + n ∎ ... | ‵inj₁ v = ‵inj₁ v From 9012225d50634950f55456b0ebd4af46bdb30262 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 8 Aug 2023 12:37:07 +0100 Subject: [PATCH 29/42] typo --- src/Data/Fin/Relation/Unary/Top.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 87eab8225d..8c59c0e996 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -73,7 +73,7 @@ view-inject₁ : ∀ j → view {suc n} (inject₁ j) ≡ ‵inj₁ (view {n} j) view-inject₁ zero = refl view-inject₁ (suc j) rewrite view-inject₁ j = refl --- Uniqeness of the view +-- Uniqueness of the view view-unique : (v : View {n} j) → view j ≡ v view-unique ‵fromℕ = view-fromℕ _ From c7e7c9e3af7ecc6b4faf7e99dee6109920c9f469 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 22:57:21 +0100 Subject: [PATCH 30/42] revised `Instances` --- .../Fin/Relation/Unary/Top/Instances.agda | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top/Instances.agda b/src/Data/Fin/Relation/Unary/Top/Instances.agda index f25d87871b..a0d474d1da 100644 --- a/src/Data/Fin/Relation/Unary/Top/Instances.agda +++ b/src/Data/Fin/Relation/Unary/Top/Instances.agda @@ -45,7 +45,7 @@ private -- terms of the functions `view-fromℕ` and `view-inject₁` defined in -- `Data.Fin.Relation.Unary.Top` -data IsFromℕ : View {suc n} i → Set where +data IsFromℕ : View i → Set where ‵fromℕ : IsFromℕ (‵fromℕ {n}) instance @@ -53,28 +53,28 @@ instance fromℕ⁺ : IsFromℕ (view (fromℕ n)) fromℕ⁺ {n = n} rewrite view-fromℕ n = ‵fromℕ -data IsInject₁ : View {suc n} i → Set where - ‵inj₁ : ∀ {j} (v : View {n} j) → IsInject₁ (‵inj₁ v) +data IsInject₁ : View i → Set where + ‵inj₁ : (v : View j) → IsInject₁ (‵inj₁ v) instance inject₁⁺ : IsInject₁ (view (inject₁ j)) inject₁⁺ {j = j} rewrite view-inject₁ j = ‵inj₁ _ - inject₁≡⁺ : {eq : inject₁ j ≡ i} → IsInject₁ (view i) - inject₁≡⁺ {eq = refl} = inject₁⁺ +inject₁≡⁺ : (eq : inject₁ j ≡ i) → IsInject₁ (view i) +inject₁≡⁺ refl = inject₁⁺ - inject₁≢n⁺ : {n≢i : n ≢ toℕ (inject₁ i)} → IsInject₁ (view {suc n} i) - inject₁≢n⁺ {n} {i} {n≢i} with view i - ... | ‵fromℕ = contradiction (sym i≡n) n≢i - where - open ≡-Reasoning - i≡n : toℕ (inject₁ (fromℕ n)) ≡ n - i≡n = begin - toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ - toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎ - ... | ‵inj₁ v = ‵inj₁ v +inject₁≢n⁺ : (n≢i : n ≢ toℕ (inject₁ i)) → IsInject₁ (view {suc n} i) +inject₁≢n⁺ {n} {i} n≢i with view i +... | ‵fromℕ = contradiction (sym i≡n) n≢i + where + open ≡-Reasoning + i≡n : toℕ (inject₁ (fromℕ n)) ≡ n + i≡n = begin + toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ + toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ + n ∎ +... | ‵inj₁ v = ‵inj₁ v ------------------------------------------------------------------------ @@ -83,7 +83,7 @@ instance -- the corresponding properties in `Data.Fin.Properties` view-fromℕ-toℕ : ∀ i → .{{IsFromℕ (view i)}} → toℕ i ≡ n -view-fromℕ-toℕ {n = n} i with ‵fromℕ ← view i = toℕ-fromℕ n +view-fromℕ-toℕ i with ‵fromℕ ← view i = toℕ-fromℕ _ view-inject₁-toℕ< : ∀ i → .{{IsInject₁ (view i)}} → toℕ i < n view-inject₁-toℕ< i with ‵inject₁ j ← view i = inject₁ℕ< j From 1f1f9f334440e04eb449c3e259822290cc554c72 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 23:00:45 +0100 Subject: [PATCH 31/42] fresh round of `variable` review comments --- src/Data/Fin/Relation/Unary/Top.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 8c59c0e996..a5f51da596 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -33,11 +33,11 @@ private -- target *disjoint* instances of the family; and hence the interpretations -- of the View constructors will also be disjoint -data View : ∀ {n} (j : Fin n) → Set where +data View : (j : Fin n) → Set where ‵fromℕ : View (fromℕ n) - ‵inj₁ : {j : Fin n} → View j → View (inject₁ j) + ‵inj₁ : View j → View (inject₁ j) -pattern ‵inject₁ {n} j = ‵inj₁ {n = n} {j = j} _ +pattern ‵inject₁ j = ‵inj₁ {j = j} _ -- The view covering function, witnessing soundness of the view @@ -48,34 +48,34 @@ view-zero (suc n) = ‵inj₁ (view-zero n) view : (j : Fin n) → View j view zero = view-zero _ view (suc i) with view i -... | ‵fromℕ = ‵fromℕ +... | ‵fromℕ = ‵fromℕ ... | ‵inject₁ j = ‵inj₁ (view (suc j)) -- Interpretation of the view constructors -⟦_⟧ : View {n} j → Fin n +⟦_⟧ : {j : Fin n} → View j → Fin n ⟦ ‵fromℕ ⟧ = fromℕ _ ⟦ ‵inject₁ j ⟧ = inject₁ j -- Completeness of the view -view-complete : (v : View {n} j) → ⟦ v ⟧ ≡ j +view-complete : (v : View j) → ⟦ v ⟧ ≡ j view-complete ‵fromℕ = refl view-complete (‵inj₁ _) = refl -- 'Computational' behaviour of the covering function -view-fromℕ : ∀ n → view {suc n} (fromℕ n) ≡ ‵fromℕ +view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ view-fromℕ zero = refl view-fromℕ (suc n) rewrite view-fromℕ n = refl -view-inject₁ : ∀ j → view {suc n} (inject₁ j) ≡ ‵inj₁ (view {n} j) +view-inject₁ : ∀ j → view (inject₁ j) ≡ ‵inj₁ (view {n = n} j) view-inject₁ zero = refl view-inject₁ (suc j) rewrite view-inject₁ j = refl -- Uniqueness of the view -view-unique : (v : View {n} j) → view j ≡ v +view-unique : (v : View j) → view j ≡ v view-unique ‵fromℕ = view-fromℕ _ view-unique (‵inj₁ {j = j} v) = begin view (inject₁ j) ≡⟨ view-inject₁ j ⟩ From a88d39cb1805c542e33c10eb8b6645e467e9ff29 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 23:12:53 +0100 Subject: [PATCH 32/42] sharpened use of `instance`s in response to review comments --- README/Data/Fin/Relation/Unary/Top.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 88d0f137b3..d1e97e924f 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -61,17 +61,17 @@ inject₁⁻¹ i with ‵inject₁ j ← view i = j inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view i)}} → inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} -inject₁⁻¹-irrelevant i with ‵inj₁_ ← view i = refl +inject₁⁻¹-irrelevant i with ‵inj₁ _ ← view i = refl -inject₁-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInject₁ (view i)}} → +inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{_ : IsInject₁ (view i)}} → inject₁ (inject₁⁻¹ i) ≡ i inject₁-inject₁⁻¹ i with ‵inj₁ _ ← view i = refl -inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) {{inj⁺}} ≡ j +inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) ≡ j inject₁⁻¹-inject₁ j rewrite view-inject₁ j = refl inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → - inject₁⁻¹ i {{inject₁≡⁺ {eq = eq}}} ≡ j + let instance _ = inject₁≡⁺ eq in inject₁⁻¹ i ≡ j inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → @@ -112,7 +112,7 @@ opposite-suc≡inject₁-opposite {suc n} i with view i opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j opposite-involutive {suc n} zero rewrite opposite-zero≡fromℕ n - | view-fromℕ n = refl + | 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) From c962e147dad5b7087e2f48a71e3a7f74ed358f76 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 23:16:37 +0100 Subject: [PATCH 33/42] reordering --- README/Data/Fin/Relation/Unary/Top.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index d1e97e924f..1066bc3eb6 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -59,10 +59,6 @@ inject₁⁻¹ i with ‵inject₁ j ← view i = j -- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties` -inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view i)}} → - inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} -inject₁⁻¹-irrelevant i with ‵inj₁ _ ← view i = refl - inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{_ : IsInject₁ (view i)}} → inject₁ (inject₁⁻¹ i) ≡ i inject₁-inject₁⁻¹ i with ‵inj₁ _ ← view i = refl @@ -80,6 +76,10 @@ inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → inject₁⁻¹ i₁ ≡ inject₁⁻¹ i₂ → i₁ ≡ i₂ inject₁⁻¹-injective i₁ i₂ with ‵inj₁ _ ← view i₁ | ‵inj₁ _ ← view i₂ = cong inject₁ +inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view i)}} → + inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} +inject₁⁻¹-irrelevant i with ‵inj₁ _ ← view i = refl + toℕ-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInject₁ (view i)}} → toℕ (inject₁⁻¹ i) ≡ toℕ i toℕ-inject₁⁻¹ i with ‵inject₁ j ← view i = sym (toℕ-inject₁ j) From 6ba18be3c26cd9f104aa0813efa8f19c496a44c0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 23:34:49 +0100 Subject: [PATCH 34/42] =?UTF-8?q?`from=E2=84=95=E2=89=A2inject=E2=82=81`?= =?UTF-8?q?=20now=20takes=20implicit=20argument?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Top.agda | 6 +++--- src/Data/Fin/Properties.agda | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index 1066bc3eb6..b29ebe276e 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -70,8 +70,8 @@ inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → let instance _ = inject₁≡⁺ eq in inject₁⁻¹ i ≡ j inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ -inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) → - .{{_ : IsInject₁ (view i₁)}} → +inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) + .{{_ : IsInject₁ (view i₁)}} .{{_ : IsInject₁ (view i₂)}} → inject₁⁻¹ i₁ ≡ inject₁⁻¹ i₂ → i₁ ≡ i₂ inject₁⁻¹-injective i₁ i₂ with ‵inj₁ _ ← view i₁ | ‵inj₁ _ ← view i₂ = cong inject₁ @@ -80,7 +80,7 @@ inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} inject₁⁻¹-irrelevant i with ‵inj₁ _ ← view i = refl -toℕ-inject₁⁻¹ : (i : Fin (suc n)) → .{{_ : IsInject₁ (view i)}} → +toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{_ : IsInject₁ (view i)}} → toℕ (inject₁⁻¹ i) ≡ toℕ i toℕ-inject₁⁻¹ i with ‵inject₁ j ← view i = sym (toℕ-inject₁ j) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 356b78df61..f5a96d351a 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -443,8 +443,8 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j) -- inject₁ ------------------------------------------------------------------------ -fromℕ≢inject₁ : (j : Fin n) → fromℕ n ≢ inject₁ j -fromℕ≢inject₁ (suc j) eq = fromℕ≢inject₁ j (suc-injective eq) +fromℕ≢inject₁ : fromℕ n ≢ inject₁ j +fromℕ≢inject₁ {j = suc j} eq = fromℕ≢inject₁ {j = j} (suc-injective eq) inject₁-injective : inject₁ i ≡ inject₁ j → i ≡ j inject₁-injective {i = zero} {zero} i≡j = refl From c7b3acfae0e0f26b31c8bde6350f57d41c38acf6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 12 Sep 2023 23:39:46 +0100 Subject: [PATCH 35/42] `CHANGELOG`! --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 44bd20501e..9321117464 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1920,7 +1920,7 @@ Other minor changes subst-is-cast : subst Fin eq k ≡ cast eq k cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k - fromℕ≢inject₁ : (j : Fin n) → fromℕ n ≢ inject₁ j + fromℕ≢inject₁ : {j : Fin n} → fromℕ n ≢ inject₁ j ``` * Added new functions in `Data.Integer.Base`: From eae3f83b0ab4b615640fe51306eb4e1c3a61151d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 14 Sep 2023 06:50:46 +0100 Subject: [PATCH 36/42] tidy up comments and binders --- src/Data/Fin/Relation/Unary/Top.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index a5f51da596..89ff3f48da 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -26,12 +26,12 @@ private j : Fin n ------------------------------------------------------------------------ --- The View, considered as a unary relation on Fin (suc 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 (suc n)` has constructors which --- target *disjoint* instances of the family; and hence the interpretations --- of the View constructors will also be disjoint +-- 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 : (j : Fin n) → Set where ‵fromℕ : View (fromℕ n) @@ -69,7 +69,7 @@ view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ view-fromℕ zero = refl view-fromℕ (suc n) rewrite view-fromℕ n = refl -view-inject₁ : ∀ j → view (inject₁ j) ≡ ‵inj₁ (view {n = n} j) +view-inject₁ : (j : Fin n) → view (inject₁ j) ≡ ‵inj₁ (view j) view-inject₁ zero = refl view-inject₁ (suc j) rewrite view-inject₁ j = refl From 4a4a4e2e735da565245acc4fbb50431404214115 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Fri, 15 Sep 2023 09:50:49 +0900 Subject: [PATCH 37/42] Change to use i rather than j in Top --- src/Data/Fin/Relation/Unary/Top.agda | 33 ++++++++++++++-------------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index 89ff3f48da..f0b514ba88 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- The 'top' view of Fin +-- 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 @@ -22,8 +22,7 @@ open import Relation.Nullary.Negation using (contradiction) private variable n : ℕ - i : Fin (suc n) - j : Fin n + i : Fin n ------------------------------------------------------------------------ -- The View, considered as a unary relation on Fin n @@ -33,11 +32,11 @@ private -- *disjoint* instances of the family (moreover at indices `n = suc _`); -- hence the interpretations of the View constructors will also be disjoint. -data View : (j : Fin n) → Set where +data View : (i : Fin n) → Set where ‵fromℕ : View (fromℕ n) - ‵inj₁ : View j → View (inject₁ j) + ‵inj₁ : View i → View (inject₁ i) -pattern ‵inject₁ j = ‵inj₁ {j = j} _ +pattern ‵inject₁ i = ‵inj₁ {i = i} _ -- The view covering function, witnessing soundness of the view @@ -45,21 +44,21 @@ view-zero : ∀ n → View {suc n} zero view-zero zero = ‵fromℕ view-zero (suc n) = ‵inj₁ (view-zero n) -view : (j : Fin n) → View j +view : (i : Fin n) → View i view zero = view-zero _ view (suc i) with view i ... | ‵fromℕ = ‵fromℕ -... | ‵inject₁ j = ‵inj₁ (view (suc j)) +... | ‵inject₁ i = ‵inj₁ (view (suc i)) -- Interpretation of the view constructors -⟦_⟧ : {j : Fin n} → View j → Fin n +⟦_⟧ : {i : Fin n} → View i → Fin n ⟦ ‵fromℕ ⟧ = fromℕ _ -⟦ ‵inject₁ j ⟧ = inject₁ j +⟦ ‵inject₁ i ⟧ = inject₁ i -- Completeness of the view -view-complete : (v : View j) → ⟦ v ⟧ ≡ j +view-complete : (v : View i) → ⟦ v ⟧ ≡ i view-complete ‵fromℕ = refl view-complete (‵inj₁ _) = refl @@ -69,16 +68,16 @@ view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ view-fromℕ zero = refl view-fromℕ (suc n) rewrite view-fromℕ n = refl -view-inject₁ : (j : Fin n) → view (inject₁ j) ≡ ‵inj₁ (view j) +view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) view-inject₁ zero = refl -view-inject₁ (suc j) rewrite view-inject₁ j = refl +view-inject₁ (suc i) rewrite view-inject₁ i = refl -- Uniqueness of the view -view-unique : (v : View j) → view j ≡ v +view-unique : (v : View i) → view i ≡ v view-unique ‵fromℕ = view-fromℕ _ -view-unique (‵inj₁ {j = j} v) = begin - view (inject₁ j) ≡⟨ view-inject₁ j ⟩ - ‵inj₁ (view j) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ +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 c8451d77899b6691f7cfdd12f929abdd08f58072 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 04:37:56 +0100 Subject: [PATCH 38/42] uniform naming scheme --- CHANGELOG.md | 2 +- src/Data/Fin/Properties.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9321117464..26a1ac9e11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1920,7 +1920,7 @@ Other minor changes subst-is-cast : subst Fin eq k ≡ cast eq k cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k - fromℕ≢inject₁ : {j : Fin n} → fromℕ n ≢ inject₁ j + fromℕ≢inject₁ : {i : Fin n} → fromℕ n ≢ inject₁ i ``` * Added new functions in `Data.Integer.Base`: diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index f5a96d351a..424a863043 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -443,8 +443,8 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j) -- inject₁ ------------------------------------------------------------------------ -fromℕ≢inject₁ : fromℕ n ≢ inject₁ j -fromℕ≢inject₁ {j = suc j} eq = fromℕ≢inject₁ {j = j} (suc-injective eq) +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 From 21500e926161ab5d8f9ccc6132db1c47cf38c537 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 09:17:49 +0100 Subject: [PATCH 39/42] removed `Instances` --- .../Fin/Relation/Unary/Top/Instances.agda | 89 ------------------- 1 file changed, 89 deletions(-) delete mode 100644 src/Data/Fin/Relation/Unary/Top/Instances.agda diff --git a/src/Data/Fin/Relation/Unary/Top/Instances.agda b/src/Data/Fin/Relation/Unary/Top/Instances.agda deleted file mode 100644 index a0d474d1da..0000000000 --- a/src/Data/Fin/Relation/Unary/Top/Instances.agda +++ /dev/null @@ -1,89 +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.Top.Instances 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₁; inject₁ℕ<) -open import Data.Fin.Relation.Unary.Top -open import Relation.Binary.PropositionalEquality.Core -open import Relation.Nullary.Negation using (contradiction) - -private - variable - n : ℕ - i : Fin (suc n) - j : Fin n - ------------------------------------------------------------------------- --- Experimental --- --- Because we work --without-K, Agda's unifier will complain about --- attempts to match `refl` against hypotheses of the form --- `view {n} i ≡ v` --- or gets stuck trying to solve unification problems of the form --- (inferred index ≟ expected index) --- even when these problems are *provably* solvable. --- --- So the two predicates on values of the view defined below --- are extensionally equivalent to the assertions --- `view {n} i ≡ ‵fromℕ` and `view {n} i ≡ ‵inject₁ j` --- --- But such assertions can only ever have a unique (irrelevant) proof --- so we introduce instances to witness them, themselves given in --- terms of the functions `view-fromℕ` and `view-inject₁` defined in --- `Data.Fin.Relation.Unary.Top` - -data IsFromℕ : View i → Set where - ‵fromℕ : IsFromℕ (‵fromℕ {n}) - -instance - - fromℕ⁺ : IsFromℕ (view (fromℕ n)) - fromℕ⁺ {n = n} rewrite view-fromℕ n = ‵fromℕ - -data IsInject₁ : View i → Set where - ‵inj₁ : (v : View j) → IsInject₁ (‵inj₁ v) - -instance - - inject₁⁺ : IsInject₁ (view (inject₁ j)) - inject₁⁺ {j = j} rewrite view-inject₁ j = ‵inj₁ _ - -inject₁≡⁺ : (eq : inject₁ j ≡ i) → IsInject₁ (view i) -inject₁≡⁺ refl = inject₁⁺ - -inject₁≢n⁺ : (n≢i : n ≢ toℕ (inject₁ i)) → IsInject₁ (view {suc n} i) -inject₁≢n⁺ {n} {i} n≢i with view i -... | ‵fromℕ = contradiction (sym i≡n) n≢i - where - open ≡-Reasoning - i≡n : toℕ (inject₁ (fromℕ n)) ≡ n - i≡n = begin - toℕ (inject₁ (fromℕ n)) ≡⟨ toℕ-inject₁ (fromℕ n) ⟩ - toℕ (fromℕ n) ≡⟨ toℕ-fromℕ n ⟩ - n ∎ -... | ‵inj₁ v = ‵inj₁ v - - ------------------------------------------------------------------------- --- As corollaries, we obtain two useful properties, which are --- witnessed by, but can also serve as proxy replacements for, --- the corresponding properties in `Data.Fin.Properties` - -view-fromℕ-toℕ : ∀ i → .{{IsFromℕ (view i)}} → toℕ i ≡ n -view-fromℕ-toℕ i with ‵fromℕ ← view i = toℕ-fromℕ _ - -view-inject₁-toℕ< : ∀ i → .{{IsInject₁ (view i)}} → toℕ i < n -view-inject₁-toℕ< i with ‵inject₁ j ← view i = inject₁ℕ< j From c5ed38f470fe38888642c595cec825bf4b1de0c6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 09:55:30 +0100 Subject: [PATCH 40/42] =?UTF-8?q?removed=20`inject=E2=82=81=E2=81=BB=C2=B9?= =?UTF-8?q?`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README/Data/Fin/Relation/Unary/Top.agda | 64 +++---------------------- 1 file changed, 6 insertions(+), 58 deletions(-) diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index b29ebe276e..e602932827 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -9,7 +9,7 @@ -- * 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`: +-- together with their corresponding properties in `Data.Fin.Properties`. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -22,8 +22,7 @@ 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 -open import Data.Fin.Relation.Unary.Top.Instances -open import Induction.WellFounded as WF +import Induction.WellFounded as WF open import Level using (Level) open import Relation.Binary.PropositionalEquality open import Relation.Unary using (Pred) @@ -32,57 +31,6 @@ private variable ℓ : Level n : ℕ - i : Fin (suc n) - j : Fin n - ------------------------------------------------------------------------- --- Inverting inject₁ - --- The principal purpose of this View of Fin (suc n) is that it provides --- a *partial inverse* to the function inject₁, as follows: --- --- * pattern matching of the form `... inj j ← view {n} i` ensures that --- `i ≟ inject₁ j`, and hence that `j` is, *definitionally*, an image --- under a hypothetical inverse to `inject₁`; --- --- * such patterns are irrefutable *precisely* when `i` is in the codomain --- of `inject₁`, which by property `fromℕ≢inject₁`, is equivalent to the --- condition `i ≢ fromℕ n`, or again equivalently, `toℕ i ≢ n`, each --- equivalent to `IsInject₁ {n} (view i)`, hence amenable to instance resolution --- --- Definition --- --- Rather than redefine `lower₁` of `Data.Fin.Base`, we instead define - -inject₁⁻¹ : (i : Fin (suc n)) → .{{IsInject₁ (view i)}} → Fin n -inject₁⁻¹ i with ‵inject₁ j ← view i = j - --- Properties, by analogy with those for `lower₁` in `Data.Fin.Properties` - -inject₁-inject₁⁻¹ : (i : Fin (suc n)) .{{_ : IsInject₁ (view i)}} → - inject₁ (inject₁⁻¹ i) ≡ i -inject₁-inject₁⁻¹ i with ‵inj₁ _ ← view i = refl - -inject₁⁻¹-inject₁ : (j : Fin n) → inject₁⁻¹ (inject₁ j) ≡ j -inject₁⁻¹-inject₁ j rewrite view-inject₁ j = refl - -inject₁≡⇒inject₁⁻¹≡ : (eq : inject₁ {n} j ≡ i) → - let instance _ = inject₁≡⁺ eq in inject₁⁻¹ i ≡ j -inject₁≡⇒inject₁⁻¹≡ refl = inject₁⁻¹-inject₁ _ - -inject₁⁻¹-injective : (i₁ i₂ : Fin (suc n)) - .{{_ : IsInject₁ (view i₁)}} - .{{_ : IsInject₁ (view i₂)}} → - inject₁⁻¹ i₁ ≡ inject₁⁻¹ i₂ → i₁ ≡ i₂ -inject₁⁻¹-injective i₁ i₂ with ‵inj₁ _ ← view i₁ | ‵inj₁ _ ← view i₂ = cong inject₁ - -inject₁⁻¹-irrelevant : (i : Fin (suc n)) .{{ii₁ ii₂ : IsInject₁ (view i)}} → - inject₁⁻¹ i {{ii₁}} ≡ inject₁⁻¹ i {{ii₂}} -inject₁⁻¹-irrelevant i with ‵inj₁ _ ← view i = refl - -toℕ-inject₁⁻¹ : (i : Fin (suc n)) .{{_ : IsInject₁ (view i)}} → - toℕ (inject₁⁻¹ i) ≡ toℕ i -toℕ-inject₁⁻¹ i with ‵inject₁ j ← view i = sym (toℕ-inject₁ j) ------------------------------------------------------------------------ -- Reimplementation of `Data.Fin.Base.opposite`, and its properties @@ -112,10 +60,10 @@ opposite-suc≡inject₁-opposite {suc n} i with view i opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j opposite-involutive {suc n} zero rewrite opposite-zero≡fromℕ n - | view-fromℕ n = refl + | 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) + | 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 @@ -128,7 +76,7 @@ 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 {n} {suc (toℕ j)} (toℕ-weakInduction {n = n} P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded 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 cb3eb95d0a6e8bcd3336817c328dd208c85347d2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 09:56:13 +0100 Subject: [PATCH 41/42] removed `Top.Instances` --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 26a1ac9e11..e5e2075c7c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1405,7 +1405,6 @@ New modules * A small library defining a structurally recursive view of `Fin n`: ``` Data.Fin.Relation.Unary.Top - Data.Fin.Relation.Unary.Top.Instances ``` * A small library for a non-empty fresh list: From 7207c6ef2c7dffed9e0893037334f5226bf97211 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Sep 2023 13:02:57 +0100 Subject: [PATCH 42/42] drastic `import` simplification --- src/Data/Fin/Relation/Unary/Top.agda | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index f0b514ba88..b6a567a9a8 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -13,11 +13,9 @@ module Data.Fin.Relation.Unary.Top 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₁; inject₁ℕ<) +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 -open import Relation.Nullary.Negation using (contradiction) private variable @@ -40,12 +38,11 @@ pattern ‵inject₁ i = ‵inj₁ {i = i} _ -- The view covering function, witnessing soundness of the view -view-zero : ∀ n → View {suc n} zero -view-zero zero = ‵fromℕ -view-zero (suc n) = ‵inj₁ (view-zero n) - view : (i : Fin n) → View i -view zero = view-zero _ +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)) @@ -80,4 +77,3 @@ 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 -