From 6b378fb79186f165e44ecd5a8a9558687ca2ca40 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 13:23:53 +0100 Subject: [PATCH 01/16] adding primed functionality for NonZero instances --- src/Data/Fin/Base.agda | 43 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 06c4581337..85eef11fa7 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -7,6 +7,7 @@ -- Note that elements of Fin n can be seen as natural numbers in the -- set {m | m < n}. The notation "m" in comments below refers to this -- natural number view. + {-# OPTIONS --without-K --safe #-} module Data.Fin.Base where @@ -38,6 +39,27 @@ data Fin : ℕ → Set where zero : Fin (suc n) suc : (i : Fin n) → Fin (suc n) +------------------------------------------------------------------------ +-- Much of the power of dependently-typed programming comes from the +-- ability of pattern-matching over inhomogeneous telescopes of types +-- to discriminate aruments to functions in sharper ways. + +-- The Fin type exemplifies this behaviour, but at the cost of not always +-- being able to know in a function defintion which case one is in by virtue +-- of an explicit constructor (ℕ.suc) symbol occurring in the type. So +-- (issue #1686) we also consider constructors and functions defined over +-- homogeneous telescopes of the form {n} (i : Fin n) subject to n being +-- ℕ.NonZero, to be instantiated at any cal-site by instance inference. +-- This additional functionality will be systematically marked by use of a prime \'. + +-- homogeneous constructors + +zero′ : .{{ℕ.NonZero n}} → Fin n +zero′ {n = suc n} = zero + +suc′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +suc′ {n = suc n} = suc + -- A conversion: toℕ "i" = i. toℕ : Fin n → ℕ @@ -115,17 +137,24 @@ inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) +inject₁′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +inject₁′ {n = suc n} = inject₁ + inject≤ : Fin m → m ℕ.≤ n → Fin n inject≤ {_} {suc n} zero _ = zero inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n) -- lower₁ "i" _ = "i". -lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n +lower₁ : (i : Fin (suc n)) → n ≢ toℕ i → Fin n lower₁ {zero} zero ne = ⊥-elim (ne refl) lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) +lower₁′ : .{{ℕ.NonZero n}} → + (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) +lower₁′ {n = suc n} i ne = lower₁ i (ne ∘ cong suc) + -- A strengthening injection into the minimal Fin fibre. strengthen : ∀ (i : Fin n) → Fin′ (suc i) strengthen zero = zero @@ -258,6 +287,10 @@ punchOut {_} {zero} {suc j} _ = j punchOut {suc _} {suc i} {zero} _ = zero punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) +punchOut′ : .{{ℕ.NonZero n}} → + {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) +punchOut′ {n = suc n} = punchOut + -- The function f(i,j) = if j≥i then j+1 else j punchIn : Fin (suc n) → Fin n → Fin (suc n) @@ -265,6 +298,10 @@ punchIn zero j = suc j punchIn (suc i) zero = zero punchIn (suc i) (suc j) = suc (punchIn i j) +punchIn′ : .{{ℕ.NonZero n}} → + Fin n → Fin (ℕ.pred n) → Fin n +punchIn′ {n = suc n} = punchIn + -- The function f(i,j) such that f(i,j) = if j≤i then j else j-1 pinch : Fin n → Fin (suc n) → Fin n @@ -272,6 +309,10 @@ pinch {suc n} _ zero = zero pinch {suc n} zero (suc j) = j pinch {suc n} (suc i) (suc j) = suc (pinch i j) +pinch′ : .{{ℕ.NonZero n}} → + Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) +pinch′ {n = suc n} = pinch + ------------------------------------------------------------------------ -- Order relations From 3b6f952f13391199d80e86dd22b2d1fec11abd39 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 13:33:04 +0100 Subject: [PATCH 02/16] CHANGELOG updates --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 26b29feae3..8dcbb92aad 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1511,6 +1511,19 @@ Other minor changes quotient : Fin (m * n) → Fin m remainder : Fin (m * n) → Fin n ``` + + Additionally, as per issue #1686, primed functionality in cases + the Fin index n is NonZero: + ``` + zero′ : Fin n + suc' : Fin (ℕ.pred n) → Fin n + inject₁′ : Fin (ℕ.pred n) → Fin n + lower₁′ : (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) + punchOut′ : + {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) + punchIn′ : Fin n → Fin (ℕ.pred n) → Fin n + pinch′ : Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) + ``` * Added new proofs in `Data.Fin.Induction`: every (strict) partial order is well-founded and Noetherian. From 5291e3145f1aa02461cc659f444aa38f7f4e60ba Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 14:18:38 +0100 Subject: [PATCH 03/16] finished Data.Fin.Base, Data.Fin.Properties --- CHANGELOG.md | 25 ++++++++++++++++- src/Data/Fin/Permutation.agda | 4 +-- src/Data/Fin/Properties.agda | 53 +++++++++++++++++++++++++++++++++-- 3 files changed, 77 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8dcbb92aad..054ee01142 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1513,7 +1513,7 @@ Other minor changes ``` Additionally, as per issue #1686, primed functionality in cases - the Fin index n is NonZero: + where the `Fin` index `n` is `NonZero`: ``` zero′ : Fin n suc' : Fin (ℕ.pred n) → Fin n @@ -1588,6 +1588,29 @@ Other minor changes cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k ``` + Additionally primed functionality as in `Data.Fin.Base`: + ``` + inject₁-lower₁′ : (n≢i+1 : n ≢ suc (toℕ i)) → + inject₁′ (lower₁′ i n≢i+1) ≡ i + lower₁-irrelevant′ : (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) → + lower₁′ i n≢i₁+1 ≡ lower₁′ i n≢i₂+1 + inject₁≡⇒lower₁≡′ : (n≢j+1 : n ≢ suc (toℕ j)) → inject₁′ i ≡ j → lower₁′ j n≢j+1 ≡ i + pred<′ : (i : Fin n) → i ≢ zero′ → pred i < i + punchOut-cong′ : {i≢j : i ≢ j} {i≢k : i ≢ k} → + j ≡ k → punchOut′ i≢j ≡ punchOut′ i≢k + punchOut-injective′ : (i≢j : i ≢ j) (i≢k : i ≢ k) → + punchOut′ i≢j ≡ punchOut′ i≢k → j ≡ k + punchIn-punchOut′ : {i j : Fin n} (i≢j : i ≢ j) → + punchIn′ i (punchOut′ i≢j) ≡ j + + pinch-injective′ : {i : Fin (ℕ.pred n)} {j k : Fin n} → + suc′ i ≢ j → suc′ i ≢ k → pinch′ i j ≡ pinch′ i k → j ≡ k + ``` + + NB Adding `punchOut-cong′` for the sake of uniformity with the 'primed' naming scheme + for `NonZero` instances, entailed renaming the old `punchOut-cong′` to `punchOut-cong-eq`, + with knock-on effect in two places in `Data.Fin.Permutation` + * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 19292f102d..30885c1e5d 100644 --- a/src/Data/Fin/Permutation.agda +++ b/src/Data/Fin/Permutation.agda @@ -145,7 +145,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ inverseʳ′ : Inverseʳ _≡_ _≡_ to from inverseʳ′ j = begin from (to j) ≡⟨⟩ - punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩ + punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong-eq i (cong πˡ (punchIn-punchOut _)) ⟩ punchOut {i = i} {πˡ (πʳ (punchIn i j))} _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩ punchOut {i = i} {punchIn i j} _ ≡⟨ punchOut-punchIn i ⟩ j ∎ @@ -153,7 +153,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′ inverseˡ′ : Inverseˡ _≡_ _≡_ to from inverseˡ′ j = begin to (from j) ≡⟨⟩ - punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ + punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))} _ ≡⟨ punchOut-cong-eq (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩ punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))} _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩ punchOut {i = πʳ i} {punchIn (πʳ i) j} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩ j ∎ diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 46e146c8c9..8529dfcfe9 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -202,6 +202,10 @@ fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i) ≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n ≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i) +≤fromℕ′ : .{{ℕ.NonZero n}} → + (i : Fin n) → i ≤ fromℕ (ℕ.pred n) +≤fromℕ′ {n = suc n} i = ≤fromℕ i + ------------------------------------------------------------------------ -- fromℕ< ------------------------------------------------------------------------ @@ -500,6 +504,11 @@ inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) +inject₁-lower₁′ : .{{_ : ℕ.NonZero n}} → + (i : Fin n) (n≢i+1 : n ≢ suc (toℕ i)) → + inject₁′ (lower₁′ i n≢i+1) ≡ i +inject₁-lower₁′ {n = suc n} i n≢i+1 = inject₁-lower₁ i (n≢i+1 ∘ cong suc) + lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → lower₁ (inject₁ i) n≢i ≡ i lower₁-inject₁′ zero _ = refl @@ -517,10 +526,21 @@ lower₁-irrelevant {suc n} zero _ _ = refl lower₁-irrelevant {suc n} (suc i) _ _ = cong suc (lower₁-irrelevant i _ _) +lower₁-irrelevant′ : .{{_ : ℕ.NonZero n}} → + (i : Fin n) (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) → + lower₁′ i n≢i₁+1 ≡ lower₁′ i n≢i₂+1 +lower₁-irrelevant′ {n = suc n} i n≢i₁+1 n≢i₂+1 = + lower₁-irrelevant i (n≢i₁+1 ∘ cong suc) (n≢i₂+1 ∘ cong suc) + inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} → (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) +inject₁≡⇒lower₁≡′ : .{{_ : ℕ.NonZero n}} → + {i : Fin (ℕ.pred n)} {j : Fin n} → + (n≢j+1 : n ≢ suc (toℕ j)) → inject₁′ i ≡ j → lower₁′ j n≢j+1 ≡ i +inject₁≡⇒lower₁≡′ {n = suc n} n≢j+1 = inject₁≡⇒lower₁≡ (n≢j+1 ∘ cong suc) + ------------------------------------------------------------------------ -- inject≤ ------------------------------------------------------------------------ @@ -554,6 +574,10 @@ pred< : ∀ (i : Fin (suc n)) → i ≢ zero → pred i < i pred< zero i≢0 = contradiction refl i≢0 pred< (suc i) _ = ≤̄⇒inject₁< ℕₚ.≤-refl +pred<′ : .{{_ : ℕ.NonZero n}} → + (i : Fin n) → i ≢ zero′ → pred i < i +pred<′ {n = suc n} i = pred< i + ------------------------------------------------------------------------ -- splitAt ------------------------------------------------------------------------ @@ -831,13 +855,23 @@ punchOut-cong {_} zero {suc j} {suc k} = suc-injective punchOut-cong {suc n} (suc i) {zero} {zero} _ = refl punchOut-cong {suc n} (suc i) {suc j} {suc k} = cong suc ∘ punchOut-cong i ∘ suc-injective +punchOut-cong′ : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} → + j ≡ k → punchOut′ i≢j ≡ punchOut′ i≢k +punchOut-cong′ {n = suc n} = punchOut-cong + -- An alternative to 'punchOut-cong' in the which the new inequality argument is -- specific. Useful for enabling the omission of that argument during equational -- reasoning. -punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → +punchOut-cong-eq : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym) -punchOut-cong′ i q = punchOut-cong i q +punchOut-cong-eq i q = punchOut-cong i q + +punchOut-cong-eq′ : .{{_ : ℕ.NonZero n}} → + ∀ (i : Fin n) {j k} {p : i ≢ j} (q : j ≡ k) → + punchOut′ p ≡ punchOut′ (p ∘ sym ∘ trans q ∘ sym) +punchOut-cong-eq′ {n = suc n} = punchOut-cong-eq punchOut-injective : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → @@ -849,6 +883,11 @@ punchOut-injective {suc n} {suc i} {zero} {zero} _ _ _ = refl punchOut-injective {suc n} {suc i} {suc j} {suc k} i≢j i≢k pⱼ≡pₖ = cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ)) +punchOut-injective′ : .{{_ : ℕ.NonZero n}} → + {i j k : Fin n} (i≢j : i ≢ j) (i≢k : i ≢ k) → + punchOut′ i≢j ≡ punchOut′ i≢k → j ≡ k +punchOut-injective′ {n = suc n} = punchOut-injective + punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) → punchIn i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 @@ -857,6 +896,11 @@ punchIn-punchOut {suc m} {suc i} {zero} i≢j = refl punchIn-punchOut {suc m} {suc i} {suc j} i≢j = cong suc (punchIn-punchOut (i≢j ∘ cong suc)) +punchIn-punchOut′ : .{{_ : ℕ.NonZero n}} → + {i j : Fin n} (i≢j : i ≢ j) → + punchIn′ i (punchOut′ i≢j) ≡ j +punchIn-punchOut′ {n = suc n} = punchIn-punchOut + punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j punchOut-punchIn zero {j} = refl punchOut-punchIn (suc i) {zero} = refl @@ -896,6 +940,11 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq = (pinch-injective (1+i≢j ∘ cong suc) (1+i≢k ∘ cong suc) (suc-injective eq)) +pinch-injective′ : .{{_ : ℕ.NonZero n}} → + {i : Fin (ℕ.pred n)} {j k : Fin n} → + suc′ i ≢ j → suc′ i ≢ k → pinch′ i j ≡ pinch′ i k → j ≡ k +pinch-injective′ {n = suc n} = pinch-injective + ------------------------------------------------------------------------ -- Quantification ------------------------------------------------------------------------ From 193de9b6bd3d31eac14b954fdcbf6b2345eac425 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 14:19:33 +0100 Subject: [PATCH 04/16] additional Data.vec functions and properties --- CHANGELOG.md | 1 + src/Data/Vec/Base.agda | 4 ++++ src/Data/Vec/Properties.agda | 5 +++++ 3 files changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 054ee01142..835971a555 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1929,6 +1929,7 @@ Other minor changes _ʳ++_ : Vec A m → Vec A n → Vec A (m + n) cast : .(eq : m ≡ n) → Vec A m → Vec A n + insert′ : Vec A (pred n) → Fin n → A → Vec A n ``` * Added new instance in `Data.Vec.Categorical`: diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index acc8f54b49..185a8395a4 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -68,6 +68,10 @@ insert : Vec A n → Fin (suc n) → A → Vec A (suc n) insert xs zero v = v ∷ xs insert (x ∷ xs) (suc i) v = x ∷ insert xs i v +insert′ : .{{_ : NonZero n}} → + Vec A (pred n) → Fin n → A → Vec A n +insert′ {n = suc n} = insert + remove : Vec A (suc n) → Fin (suc n) → Vec A n remove (_ ∷ xs) zero = xs remove (x ∷ y ∷ xs) (suc i) = x ∷ remove (y ∷ xs) i diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 805570c42e..0d5c9cadc4 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1071,6 +1071,11 @@ insert-punchIn xs zero v j = refl insert-punchIn (x ∷ xs) (suc i) v zero = refl insert-punchIn (x ∷ xs) (suc i) v (suc j) = insert-punchIn xs i v j +insert-punchIn′ : .{{_ : NonZero n}} → + (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) → + lookup (insert′ xs i v) (Fin.punchIn′ i j) ≡ lookup xs j +insert-punchIn′ {n = suc n} = insert-punchIn + remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) → lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j remove-punchOut (x ∷ xs) {zero} {zero} i≢j = contradiction refl i≢j From 3bfcb8308774732daa7715fbad68f9ff12231f04 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 14:26:01 +0100 Subject: [PATCH 05/16] Data.vec.Recursive --- CHANGELOG.md | 7 +++++++ src/Data/Vec/Recursive.agda | 9 +++++++++ 2 files changed, 16 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 835971a555..43756b558c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1999,6 +1999,13 @@ Other minor changes lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i ``` +* Added new functions in `Data.Vec.Recursive` for `{{NonZero n}}`: + ``` + uncons′ : A ^ n → A × A ^ (pred n) + head′ : A ^ n → A + tail′ : A ^ n → A ^ (pred n) + ``` + * Added new proofs in `Data.Vec.Functional.Properties`: ``` map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs) diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda index b30089d33c..60ed69b9ae 100644 --- a/src/Data/Vec/Recursive.agda +++ b/src/Data/Vec/Recursive.agda @@ -74,12 +74,21 @@ uncons : ∀ n → A ^ suc n → A × A ^ n uncons 0 a = a , lift tt uncons (suc n) (a , as) = a , as +uncons′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A × A ^ (pred n) +uncons′ (suc n) = uncons n + head : ∀ n → A ^ suc n → A head n as = proj₁ (uncons n as) +head′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A +head′ (suc n) = head n + tail : ∀ n → A ^ suc n → A ^ n tail n as = proj₂ (uncons n as) +tail′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A ^ (pred n) +tail′ (suc n) = tail n + fromVec : ∀[ Vec A ⇒ (A ^_) ] fromVec = Vec.foldr (_ ^_) (cons _) _ From 0eb3ad74c4b948e6a1ae58fb1e9ba38aa66c95bb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 15:00:39 +0100 Subject: [PATCH 06/16] additional Data.Fin and Data.Vec functions and properties --- CHANGELOG.md | 22 +++++++++++++++++++--- src/Data/Fin/Base.agda | 3 +++ src/Data/Vec/Base.agda | 19 +++++++++++++++++++ src/Data/Vec/Properties.agda | 23 ++++++++++++++++++++++- 4 files changed, 63 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 43756b558c..053dcc6e31 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1517,10 +1517,10 @@ Other minor changes ``` zero′ : Fin n suc' : Fin (ℕ.pred n) → Fin n + inject!′ : {i : Fin n} → Fin′ i → Fin (ℕ.pred n) inject₁′ : Fin (ℕ.pred n) → Fin n lower₁′ : (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) - punchOut′ : - {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) + punchOut′ : {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) punchIn′ : Fin n → Fin (ℕ.pred n) → Fin n pinch′ : Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) ``` @@ -1588,7 +1588,7 @@ Other minor changes cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k ``` - Additionally primed functionality as in `Data.Fin.Base`: + Additionally properties of the primed functionality as in `Data.Fin.Base`: ``` inject₁-lower₁′ : (n≢i+1 : n ≢ suc (toℕ i)) → inject₁′ (lower₁′ i n≢i+1) ≡ i @@ -1929,7 +1929,16 @@ Other minor changes _ʳ++_ : Vec A m → Vec A n → Vec A (m + n) cast : .(eq : m ≡ n) → Vec A m → Vec A n + ``` + And for `{{NonZero n}}` as per issue 1686 + ``` + head′ : Vec A n → A + tail′ : Vec A n → A ^ (pred n) insert′ : Vec A (pred n) → Fin n → A → Vec A n + remove′ : Vec A n → Fin n → Vec A (pred n) + uncons′ : Vec A n → A × Vec A (pred n) + init′ : (xs : Vec A n) → Vec A (pred n) + last′ : (xs : Vec A n) → A ``` * Added new instance in `Data.Vec.Categorical`: @@ -1998,7 +2007,14 @@ Other minor changes lookup-cast₁ : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i) lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i ``` + And for `{{NonZero n}}`: + ``` + insert-lookup′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) → + lookup (insert′ xs i v) i ≡ v + insert-punchIn′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) → + lookup (insert′ xs i v) (Fin.punchIn′ i j) ≡ lookup xs j + ``` * Added new functions in `Data.Vec.Recursive` for `{{NonZero n}}`: ``` uncons′ : A ^ n → A × A ^ (pred n) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 85eef11fa7..edf6278576 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -133,6 +133,9 @@ inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n inject! {n = suc _} {i = suc _} zero = zero inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j) +inject!′ : .{{ℕ.NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n) +inject!′ {n = suc n} = inject! + inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 185a8395a4..5c113ecd6d 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -53,9 +53,15 @@ length {n = n} _ = n head : Vec A (1 + n) → A head (x ∷ xs) = x +head′ : .{{_ : NonZero n}} → Vec A n → A +head′ {n = suc n} = head + tail : Vec A (1 + n) → Vec A n tail (x ∷ xs) = xs +tail′ : .{{_ : NonZero n}} → Vec A n → Vec A (pred n) +tail′ {n = suc n} = tail + lookup : Vec A n → Fin n → A lookup (x ∷ xs) zero = x lookup (x ∷ xs) (suc i) = lookup xs i @@ -76,6 +82,10 @@ remove : Vec A (suc n) → Fin (suc n) → Vec A n remove (_ ∷ xs) zero = xs remove (x ∷ y ∷ xs) (suc i) = x ∷ remove (y ∷ xs) i +remove′ : .{{_ : NonZero n}} → + Vec A n → Fin n → Vec A (pred n) +remove′ {n = suc n} = remove + updateAt : Fin n → (A → A) → Vec A n → Vec A n updateAt zero f (x ∷ xs) = f x ∷ xs updateAt (suc i) f (x ∷ xs) = x ∷ updateAt i f xs @@ -291,6 +301,9 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs) uncons : Vec A (suc n) → A × Vec A n uncons (x ∷ xs) = x , xs +uncons′ : .{{NonZero n}} → Vec A n → A × Vec A (pred n) +uncons′ {n = suc n} = uncons + ------------------------------------------------------------------------ -- Operations involving ≤ @@ -349,10 +362,16 @@ init : Vec A (1 + n) → Vec A n init xs with initLast xs ... | (ys , y , refl) = ys +init′ : .{{NonZero n}} → (xs : Vec A n) → Vec A (pred n) +init′ {n = suc n} = init + last : Vec A (1 + n) → A last xs with initLast xs ... | (ys , y , refl) = y +last′ : .{{NonZero n}} → (xs : Vec A n) → A +last′ {n = suc n} = last + ------------------------------------------------------------------------ -- Other operations diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 0d5c9cadc4..ea513ec082 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -10,7 +10,8 @@ module Data.Vec.Properties where open import Algebra.Definitions open import Data.Bool.Base using (true; false) -open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_) +open import Data.Fin.Base as Fin + using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_; punchIn; punchIn′; punchOut; punchOut′) open import Data.List.Base as List using (List) open import Data.Nat.Base open import Data.Nat.Properties @@ -1065,6 +1066,11 @@ insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) → insert-lookup xs zero v = refl insert-lookup (x ∷ xs) (suc i) v = insert-lookup xs i v +insert-lookup′ : .{{_ : NonZero n}} → + (xs : Vec A (pred n)) (i : Fin n) (v : A) → + lookup (insert′ xs i v) i ≡ v +insert-lookup′ {n = suc n} = insert-lookup + insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) → lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j insert-punchIn xs zero v j = refl @@ -1084,6 +1090,11 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j = remove-punchOut (y ∷ xs) (i≢j ∘ cong suc) +remove-punchOut′ : .{{_ : NonZero n}} → + ∀ (xs : Vec A n) {i} {j} (i≢j : i ≢ j) → + lookup (remove′ xs i) (Fin.punchOut′ i≢j) ≡ lookup xs j +remove-punchOut′ {n = suc n} = remove-punchOut + ------------------------------------------------------------------------ -- remove @@ -1094,12 +1105,22 @@ remove-insert (x ∷ xs) (suc zero) v = refl remove-insert (x ∷ y ∷ xs) (suc (suc i)) v = cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v) +remove-insert′ : .{{_ : NonZero n}} → + (xs : Vec A (pred n)) (i : Fin n) (v : A) → + remove′ (insert′ xs i v) i ≡ xs +remove-insert′ {n = suc n} = remove-insert + insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) → insert (remove xs i) i (lookup xs i) ≡ xs insert-remove (x ∷ xs) zero = refl insert-remove (x ∷ y ∷ xs) (suc i) = cong (x ∷_) (insert-remove (y ∷ xs) i) +insert-remove′ : .{{_ : NonZero n}} → + (xs : Vec A n) (i : Fin n) → + insert′ (remove′ xs i) i (lookup xs i) ≡ xs +insert-remove′ {n = suc n} = insert-remove + ------------------------------------------------------------------------ -- Conversion function From 3add2070b18b00444718f6dec2f899a55b256f84 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 15:16:55 +0100 Subject: [PATCH 07/16] additional Data.Vec.Functional functions and properties --- CHANGELOG.md | 11 +++++++++++ src/Algebra/Properties/CommutativeMonoid/Sum.agda | 3 +++ src/Data/Vec/Functional.agda | 4 ++++ 3 files changed, 18 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 053dcc6e31..e1c5539552 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1436,6 +1436,11 @@ Other minor changes _^ᵗ_ : A → ℕ → A ``` +* Added new proofs to `Algebra.Properties.CommutativeSemigroup`: + ``` + sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t) + ``` + * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: ``` interchange : Interchangable _∙_ _∙_ @@ -1444,6 +1449,7 @@ Other minor changes rightSemimedial : RightSemimedial _∙_ middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x) ``` + * Added new proofs to `Algebra.Properties.Semigroup`: ``` leftAlternative : LeftAlternative _∙_ @@ -1946,6 +1952,11 @@ Other minor changes monad : RawMonad (λ (A : Set a) → Vec A n) ``` +* Added new functions in `Data.Vec.Functional` for `{{NonZero n}}`: + ``` + remove′ : Vec A n → Fin n → Vec A (pred n) + ``` + * Added new proofs in `Data.Vec.Properties`: ```agda padRight-refl : padRight ≤-refl a xs ≡ xs diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda index 54731cfb5b..c4bf6e45c0 100644 --- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda +++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda @@ -59,6 +59,9 @@ sum-remove {suc n} {suc i} xs = begin ∑t = sum t ∑t′ = sum (remove i t) +sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t) +sum-remove′ {n = suc n} = sum-remove + -- The '∑' operator distributes over addition. ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i ∑-distrib-+ {zero} f g = sym (+-identityˡ _) diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 1696e6b482..90cef63843 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -90,6 +90,10 @@ insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n remove i t = t ∘ punchIn i +remove′ : ∀ {n} .{{_ : NonZero n}} → + Fin n → Vector A n → Vector A (ℕ.pred n) +remove′ {n = suc n} i t = t ∘ punchIn′ i + updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n updateAt {n = suc n} zero f xs zero = f (head xs) updateAt {n = suc n} zero f xs (suc j) = xs (suc j) From 5cf546a6ca0cacf44c8fc4f68249402880f5ad44 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 15:23:23 +0100 Subject: [PATCH 08/16] additional Data.Vec.Functional functions and properties --- CHANGELOG.md | 10 ++++++++-- src/Data/Vec/Functional.agda | 19 +++++++++++++++++-- 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e1c5539552..8e1493695a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1940,9 +1940,9 @@ Other minor changes ``` head′ : Vec A n → A tail′ : Vec A n → A ^ (pred n) + uncons′ : Vec A n → A × Vec A (pred n) insert′ : Vec A (pred n) → Fin n → A → Vec A n remove′ : Vec A n → Fin n → Vec A (pred n) - uncons′ : Vec A n → A × Vec A (pred n) init′ : (xs : Vec A n) → Vec A (pred n) last′ : (xs : Vec A n) → A ``` @@ -1954,7 +1954,13 @@ Other minor changes * Added new functions in `Data.Vec.Functional` for `{{NonZero n}}`: ``` - remove′ : Vec A n → Fin n → Vec A (pred n) + head′ : Vector A n → A + tail′ : Vector A n → A ^ (pred n) + uncons′ : Vector A n → A × Vector A (pred n) + insert′ : Vector A (pred n) → Fin n → A → Vector A n + remove′ : Vector A n → Fin n → Vector A (pred n) + init′ : (xs : Vector A n) → Vector A (pred n) + last′ : (xs : Vector A n) → A ``` * Added new proofs in `Data.Vec.Properties`: diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda index 90cef63843..fd4e683797 100644 --- a/src/Data/Vec/Functional.agda +++ b/src/Data/Vec/Functional.agda @@ -15,7 +15,7 @@ module Data.Vec.Functional where -open import Data.Fin.Base +open import Data.Fin.Base hiding (pred) open import Data.List.Base as L using (List) open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred) open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry) @@ -72,12 +72,21 @@ length {n = n} _ = n head : ∀ {n} → Vector A (suc n) → A head xs = xs zero +head′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A +head′ {n = suc n} = head + tail : ∀ {n} → Vector A (suc n) → Vector A n tail xs = xs ∘ suc +tail′ : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) +tail′ {n = suc n} = tail + uncons : ∀ {n} → Vector A (suc n) → A × Vector A n uncons xs = head xs , tail xs +uncons′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A × Vector A (pred n) +uncons′ {n = suc n} = uncons + replicate : ∀ {n} → A → Vector A n replicate = const @@ -91,7 +100,7 @@ remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n remove i t = t ∘ punchIn i remove′ : ∀ {n} .{{_ : NonZero n}} → - Fin n → Vector A n → Vector A (ℕ.pred n) + Fin n → Vector A n → Vector A (pred n) remove′ {n = suc n} i t = t ∘ punchIn′ i updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n @@ -153,8 +162,14 @@ reverse xs = xs ∘ opposite init : ∀ {n} → Vector A (suc n) → Vector A n init xs = xs ∘ inject₁ +init′ : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n) +init′ {n = suc n} = init + last : ∀ {n} → Vector A (suc n) → A last {n = n} xs = xs (fromℕ n) +last′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A +last′ {n = suc n} = last + transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n transpose = flip From f9b8076492e7f7f10ec01b3807ffc84824c5172d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 9 Oct 2022 17:09:12 +0100 Subject: [PATCH 09/16] more selctive imports from Data.fin.base in Data.Vec.Properties --- src/Data/Vec/Properties.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index ea513ec082..ceb3ccba6e 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -11,7 +11,7 @@ module Data.Vec.Properties where open import Algebra.Definitions open import Data.Bool.Base using (true; false) open import Data.Fin.Base as Fin - using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_; punchIn; punchIn′; punchOut; punchOut′) + using (Fin; zero; suc; toℕ; _↑ˡ_; _↑ʳ_; combine) open import Data.List.Base as List using (List) open import Data.Nat.Base open import Data.Nat.Properties @@ -534,12 +534,12 @@ lookup-cast₂ eq (_ ∷ xs) (suc i) = lookup-cast₂ (suc-injective eq) xs i lookup-concat : ∀ (xss : Vec (Vec A m) n) i j → - lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j + lookup (concat xss) (combine i j) ≡ lookup (lookup xss i) j lookup-concat (xs ∷ xss) zero j = lookup-++ˡ xs (concat xss) j lookup-concat (xs ∷ xss) (suc i) j = begin - lookup (concat (xs ∷ xss)) (Fin.combine (suc i) j) - ≡⟨ lookup-++ʳ xs (concat xss) (Fin.combine i j) ⟩ - lookup (concat xss) (Fin.combine i j) + lookup (concat (xs ∷ xss)) (combine (suc i) j) + ≡⟨ lookup-++ʳ xs (concat xss) (combine i j) ⟩ + lookup (concat xss) (combine i j) ≡⟨ lookup-concat xss i j ⟩ lookup (lookup (xs ∷ xss) (suc i)) j ∎ where open ≡-Reasoning @@ -747,9 +747,9 @@ zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (zipWith-is-⊛ f xs ys) -- _⊛*_ lookup-⊛* : ∀ (fs : Vec (A → B) m) (xs : Vec A n) i j → - lookup (fs ⊛* xs) (Fin.combine i j) ≡ (lookup fs i $ lookup xs j) + lookup (fs ⊛* xs) (combine i j) ≡ (lookup fs i $ lookup xs j) lookup-⊛* (f ∷ fs) xs zero j = trans (lookup-++ˡ (map f xs) _ j) (lookup-map j f xs) -lookup-⊛* (f ∷ fs) xs (suc i) j = trans (lookup-++ʳ (map f xs) _ (Fin.combine i j)) (lookup-⊛* fs xs i j) +lookup-⊛* (f ∷ fs) xs (suc i) j = trans (lookup-++ʳ (map f xs) _ (combine i j)) (lookup-⊛* fs xs i j) ------------------------------------------------------------------------ -- foldl From 5450199c1e0ecc8ef038da7ef0b9e5b110190109 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Oct 2022 11:11:57 +0100 Subject: [PATCH 10/16] tidy up List.Properties --- src/Data/List/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index d9fef297c5..f741c074ca 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -22,7 +22,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Base -open import Data.Nat.Divisibility +open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n) open import Data.Nat.Properties open import Data.Product as Prod hiding (map; zip) import Data.Product.Relation.Unary.All as Prod using (All) @@ -622,10 +622,10 @@ tabulate-lookup : ∀ (xs : List A) → tabulate (lookup xs) ≡ xs tabulate-lookup [] = refl tabulate-lookup (x ∷ xs) = cong (_ ∷_) (tabulate-lookup xs) -length-tabulate : ∀ {n} → (f : Fin n → A) → +length-tabulate : ∀ {n} (f : Fin n → A) → length (tabulate f) ≡ n length-tabulate {n = zero} f = refl -length-tabulate {n = suc n} f = cong suc (length-tabulate (λ z → f (suc z))) +length-tabulate {n = suc n} f = cong suc (length-tabulate (f ∘ suc)) lookup-tabulate : ∀ {n} → (f : Fin n → A) → ∀ i → let i′ = cast (sym (length-tabulate f)) i From cb7d853e7560b5398482a482fcbf30e672a3667e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Oct 2022 11:53:15 +0100 Subject: [PATCH 11/16] additional properties of Vec.Unary predicates --- CHANGELOG.md | 25 +++++++++++++++++++ src/Data/Vec/Relation/Unary/All.agda | 10 ++++++++ src/Data/Vec/Relation/Unary/Any.agda | 8 ++++++ .../Vec/Relation/Unary/Linked/Properties.agda | 5 ++++ 4 files changed, 48 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2f4ced2dc1..163ffebfb4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1044,6 +1044,31 @@ Deprecated names map-++-commute ↦ map-++ ``` +* In `Data.Vec.Relation.Unary.All`: + for `{{NonZero n}}`, as per issue #1686 + + ```agda + head′ : All P xs → P (Vec.head′ {n = n} xs) + tail′ : All P xs → All P (Vec.tail′ {n = n} xs) + uncons′ : All P xs → P (Vec.head′ {n = n} xs) × All P (Vec.tail′ {n = n} xs) + ``` + +* In `Data.Vec.Relation.Unary.Any`: + for `{{NonZero n}}`, as per issue #1686 + + ```agda + head′ : ¬ Any P (Vec.tail′ {n = n} xs) → Any P xs → P (Vec.head′ {n = n} xs) + tail′ : ¬ P (Vec.head′ {n = n} xs) → Any P xs → Any P (Vec.tail′ {n = n} xs) + ``` + +* In `Data.Vec.Relation.Unary.Linked.Properties`: + for `{{NonZero n}}`, as per issue #1686 + + ```agda + Linked⇒All′ : ∀ {v} {xs : Vec _ n} → R v (head′ xs) → + Linked R xs → All (R v) xs + ``` + * In `Function.Construct.Composition`: ``` _∘-⟶_ ↦ _⟶-∘_ diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index b16340ef6b..9184f4e273 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -52,9 +52,15 @@ data All {A : Set a} (P : Pred A p) : Vec A n → Set (p ⊔ a) where head : All P (x ∷ xs) → P x head (px ∷ pxs) = px +head′ : .{{_ : NonZero n}} → All P xs → P (Vec.head′ {n = n} xs) +head′ {n = suc _} pxs@(_ ∷ _) = head pxs + tail : All P (x ∷ xs) → All P xs tail (px ∷ pxs) = pxs +tail′ : .{{_ : NonZero n}} → All P xs → All P (Vec.tail′ {n = n} xs) +tail′ {n = suc _} pxs@(_ ∷ _) = tail pxs + reduce : (f : ∀ {x} → P x → B) → ∀ {n} {xs : Vec A n} → All P xs → Vec B n reduce f [] = [] reduce f (px ∷ pxs) = f px ∷ reduce f pxs @@ -62,6 +68,10 @@ reduce f (px ∷ pxs) = f px ∷ reduce f pxs uncons : All P (x ∷ xs) → P x × All P xs uncons = < head , tail > +uncons′ : .{{_ : NonZero n}} → + All P xs → P (Vec.head′ {n = n} xs) × All P (Vec.tail′ {n = n} xs) +uncons′ = < head′ , tail′ > + map : P ⊆ Q → All P ⊆ All Q {n} map g [] = [] map g (px ∷ pxs) = g px ∷ map g pxs diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index a54991976f..831df9f08d 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -44,11 +44,19 @@ head : ∀ {x} → ¬ Any P xs → Any P (x ∷ xs) → P x head ¬pxs (here px) = px head ¬pxs (there pxs) = contradiction pxs ¬pxs +head′ : .{{_ : NonZero n}} → + ¬ Any P (Vec.tail′ {n = n} xs) → Any P xs → P (Vec.head′ {n = n} xs) +head′ {n = suc _} {xs = _ ∷ _} ¬pxs = head ¬pxs + -- If the head does not satisfy the predicate, then the tail will. tail : ∀ {x} → ¬ P x → Any P (x ∷ xs) → Any P xs tail ¬px (here px) = ⊥-elim (¬px px) tail ¬px (there pxs) = pxs +tail′ : .{{_ : NonZero n}} → + ¬ P (Vec.head′ {n = n} xs) → Any P xs → Any P (Vec.tail′ {n = n} xs) +tail′ {n = suc _} {xs = _ ∷ _} ¬px = tail ¬px + -- Convert back and forth with sum toSum : ∀ {x} → Any P (x ∷ xs) → P x ⊎ Any P xs toSum (here px) = inj₁ px diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda index 3935a263c4..3ebe0eb19f 100644 --- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda @@ -43,6 +43,11 @@ module _ (trans : Transitive R) where Linked⇒All Rvx [-] = Rvx ∷ [] Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs + Linked⇒All′ : .{{_ : NonZero n}} → + ∀ {v} {xs : Vec _ n} → R v (head′ xs) → + Linked R xs → All (R v) xs + Linked⇒All′ {n = suc n} = Linked⇒All {n = n} + lookup⁺ : ∀ {i j} {xs : Vec _ n} → Linked R xs → i < j → R (lookup xs i) (lookup xs j) From 727112f6178e028738a30e7626397eb7278cccf2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 11 Oct 2022 11:59:47 +0100 Subject: [PATCH 12/16] tighten constraints --- src/Data/Fin/Base.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index edf6278576..e65052f7a7 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -55,10 +55,10 @@ data Fin : ℕ → Set where -- homogeneous constructors zero′ : .{{ℕ.NonZero n}} → Fin n -zero′ {n = suc n} = zero +zero′ {n = suc _} = zero suc′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n -suc′ {n = suc n} = suc +suc′ {n = suc _} = suc -- A conversion: toℕ "i" = i. @@ -134,14 +134,14 @@ inject! {n = suc _} {i = suc _} zero = zero inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j) inject!′ : .{{ℕ.NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n) -inject!′ {n = suc n} = inject! +inject!′ {n = suc _} = inject! inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) inject₁′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n -inject₁′ {n = suc n} = inject₁ +inject₁′ {n = suc _} = inject₁ inject≤ : Fin m → m ℕ.≤ n → Fin n inject≤ {_} {suc n} zero _ = zero @@ -156,7 +156,7 @@ lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) lower₁′ : .{{ℕ.NonZero n}} → (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) -lower₁′ {n = suc n} i ne = lower₁ i (ne ∘ cong suc) +lower₁′ {n = suc _} i ne = lower₁ i (ne ∘ cong suc) -- A strengthening injection into the minimal Fin fibre. strengthen : ∀ (i : Fin n) → Fin′ (suc i) @@ -292,7 +292,7 @@ punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) punchOut′ : .{{ℕ.NonZero n}} → {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) -punchOut′ {n = suc n} = punchOut +punchOut′ {n = suc _} = punchOut -- The function f(i,j) = if j≥i then j+1 else j @@ -303,7 +303,7 @@ punchIn (suc i) (suc j) = suc (punchIn i j) punchIn′ : .{{ℕ.NonZero n}} → Fin n → Fin (ℕ.pred n) → Fin n -punchIn′ {n = suc n} = punchIn +punchIn′ {n = suc _} = punchIn -- The function f(i,j) such that f(i,j) = if j≤i then j else j-1 @@ -314,7 +314,7 @@ pinch {suc n} (suc i) (suc j) = suc (pinch i j) pinch′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) -pinch′ {n = suc n} = pinch +pinch′ {n = suc _} = pinch ------------------------------------------------------------------------ -- Order relations From f7548b9003138fa4d4412f30210e0bd1d958f901 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 27 Oct 2022 14:53:56 +0100 Subject: [PATCH 13/16] added two additional functions; no additional properties to `Data.Fin` --- CHANGELOG.md | 4 +++- src/Data/Fin/Base.agda | 12 +++++++++--- src/Data/Fin/Properties.agda | 36 ++++++++++++++++++------------------ 3 files changed, 30 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4e46ac8349..43031ac590 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1659,10 +1659,12 @@ Other minor changes where the `Fin` index `n` is `NonZero`: ``` zero′ : Fin n - suc' : Fin (ℕ.pred n) → Fin n + suc' : Fin (ℕ.pred n) → Fin n inject!′ : {i : Fin n} → Fin′ i → Fin (ℕ.pred n) inject₁′ : Fin (ℕ.pred n) → Fin n lower₁′ : (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) + _ℕ-′_ : (j : Fin n) → Fin (n ℕ.∸ toℕ j) + _ℕ-ℕ′_ : Fin n → ℕ punchOut′ : {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) punchIn′ : Fin n → Fin (ℕ.pred n) → Fin n pinch′ : Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index e65052f7a7..2650c09504 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -14,7 +14,7 @@ module Data.Fin.Base where open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Empty using (⊥-elim) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z Date: Thu, 27 Oct 2022 15:09:19 +0100 Subject: [PATCH 14/16] remove qualified use of `NonZero` --- src/Data/Fin/Base.agda | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index 2650c09504..d5918912e6 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -49,15 +49,15 @@ data Fin : ℕ → Set where -- of an explicit constructor (ℕ.suc) symbol occurring in the type. So -- (issue #1686) we also consider constructors and functions defined over -- homogeneous telescopes of the form {n} (i : Fin n) subject to n being --- ℕ.NonZero, to be instantiated at any cal-site by instance inference. +-- NonZero, to be instantiated at any cal-site by instance inference. -- This additional functionality will be systematically marked by use of a prime \'. -- homogeneous constructors -zero′ : .{{ℕ.NonZero n}} → Fin n +zero′ : .{{NonZero n}} → Fin n zero′ {n = suc _} = zero -suc′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +suc′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n suc′ {n = suc _} = suc -- A conversion: toℕ "i" = i. @@ -133,14 +133,14 @@ inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n inject! {n = suc _} {i = suc _} zero = zero inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j) -inject!′ : .{{ℕ.NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n) +inject!′ : .{{NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n) inject!′ {n = suc _} = inject! inject₁ : Fin n → Fin (suc n) inject₁ zero = zero inject₁ (suc i) = suc (inject₁ i) -inject₁′ : .{{ℕ.NonZero n}} → Fin (ℕ.pred n) → Fin n +inject₁′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n inject₁′ {n = suc _} = inject₁ inject≤ : Fin m → m ℕ.≤ n → Fin n @@ -154,7 +154,7 @@ lower₁ {zero} zero ne = ⊥-elim (ne refl) lower₁ {suc n} zero _ = zero lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc)) -lower₁′ : .{{ℕ.NonZero n}} → +lower₁′ : .{{NonZero n}} → (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n) lower₁′ {n = suc _} i ne = lower₁ i (ne ∘ cong suc) @@ -296,7 +296,7 @@ punchOut {_} {zero} {suc j} _ = j punchOut {suc _} {suc i} {zero} _ = zero punchOut {suc _} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc)) -punchOut′ : .{{ℕ.NonZero n}} → +punchOut′ : .{{NonZero n}} → {i j : Fin n} → i ≢ j → Fin (ℕ.pred n) punchOut′ {n = suc _} = punchOut @@ -307,7 +307,7 @@ punchIn zero j = suc j punchIn (suc i) zero = zero punchIn (suc i) (suc j) = suc (punchIn i j) -punchIn′ : .{{ℕ.NonZero n}} → +punchIn′ : .{{NonZero n}} → Fin n → Fin (ℕ.pred n) → Fin n punchIn′ {n = suc _} = punchIn @@ -318,7 +318,7 @@ pinch {suc n} _ zero = zero pinch {suc n} zero (suc j) = j pinch {suc n} (suc i) (suc j) = suc (pinch i j) -pinch′ : .{{ℕ.NonZero n}} → +pinch′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n) pinch′ {n = suc _} = pinch From 7f3dd41ed09b2a23f7183d4172ee9745d0f97ba7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 11 Nov 2022 14:36:08 +0000 Subject: [PATCH 15/16] finally added myself to the LICENCE --- LICENCE | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LICENCE b/LICENCE index 6786f01a32..893656f5ff 100644 --- a/LICENCE +++ b/LICENCE @@ -7,7 +7,7 @@ Eric Mertens, Joachim Breitner, Liyang Hu, Noam Zeilberger, Érdi Gergő, Stevan Andjelkovic, Helmut Grohne, Guilhem Moulin, Noriyuki Ohkawa, Evgeny Kotelnikov, James Chapman, Wen Kokke, Matthew Daggitt, Jason Hu, Sandro Stucki, Milo Turner, Zack Grannan, Lex van der Stoep, -Jacques Carette and some anonymous contributors. +Jacques Carette, James McKinna, and some anonymous contributors. Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the From 4e636f03f330b845b290ef6a2c40fba44f1953d6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 20 Dec 2022 12:14:04 +0000 Subject: [PATCH 16/16] Revert "finally added myself to the LICENCE" This reverts commit 7f3dd41ed09b2a23f7183d4172ee9745d0f97ba7. --- LICENCE | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LICENCE b/LICENCE index 893656f5ff..6786f01a32 100644 --- a/LICENCE +++ b/LICENCE @@ -7,7 +7,7 @@ Eric Mertens, Joachim Breitner, Liyang Hu, Noam Zeilberger, Érdi Gergő, Stevan Andjelkovic, Helmut Grohne, Guilhem Moulin, Noriyuki Ohkawa, Evgeny Kotelnikov, James Chapman, Wen Kokke, Matthew Daggitt, Jason Hu, Sandro Stucki, Milo Turner, Zack Grannan, Lex van der Stoep, -Jacques Carette, James McKinna, and some anonymous contributors. +Jacques Carette and some anonymous contributors. Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the