From 3c9a5f41010b1946b3c46901378feee57993cd60 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 27 Jul 2025 09:59:32 +0100 Subject: [PATCH 1/7] refactor: make `truncate` and `padRight` take irrelevant argument --- CHANGELOG.md | 6 ++++++ src/Data/Vec/Base.agda | 12 ++++++------ 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3cf9a9ac90..f99445b649 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,12 @@ Non-backwards compatible changes Minor improvements ------------------ +* The types of `Data.Vec.Base.{truncate|padRight}` have been weakened so + that the argument of type `m ≤ n` is marked as irrelevant. This should be + backwards compatible, but does change the equational behaviour of these + functions to be more eager, because no longer blocking on pattern matching + on that argument. + Deprecated modules ------------------ diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 8c03fb8a83..38f7bbfcd7 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -289,14 +289,14 @@ uncons (x ∷ xs) = x , xs -- Operations involving ≤ -- Take the first 'm' elements of a vector. -truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m -truncate {m = zero} _ _ = [] -truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs) +truncate : .(m ≤ n) → Vec A n → Vec A m +truncate {m = zero} _ _ = [] +truncate {m = suc _} le (x ∷ xs) = x ∷ (truncate (s≤s⁻¹ le) xs) -- Pad out a vector with extra elements. -padRight : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n -padRight z≤n a xs = replicate _ a -padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs +padRight : .(m ≤ n) → A → Vec A m → Vec A n +padRight {n = _} _ a [] = replicate _ a +padRight {n = suc _} le a (x ∷ xs) = x ∷ padRight (s≤s⁻¹ le) a xs ------------------------------------------------------------------------ -- Operations for converting between lists From ab03dc0b0527fb197a2e32767562a34d4d297e86 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 3 Aug 2025 13:52:17 +0100 Subject: [PATCH 2/7] fix: proofs of properties following #2769 and #2795; deprecate `truncate-irrelevant` --- CHANGELOG.md | 4 +- src/Data/Vec/Base.agda | 2 +- src/Data/Vec/Properties.agda | 131 +++++++++++++++++++++++++---------- 3 files changed, 99 insertions(+), 38 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 262fcea432..620bd62cff 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,8 +21,8 @@ Minor improvements that the argument of type `m ≤ n` is marked as irrelevant. This should be backwards compatible, but does change the equational behaviour of these functions to be more eager, because no longer blocking on pattern matching - on that argument. - ``` + on that argument. Corresponding changes have been made to the types of their + properties (and their proofs). * Refactored usages of `+-∸-assoc 1` to `∸-suc` in: ```agda diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 38f7bbfcd7..b4153db297 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -295,7 +295,7 @@ truncate {m = suc _} le (x ∷ xs) = x ∷ (truncate (s≤s⁻¹ le) xs) -- Pad out a vector with extra elements. padRight : .(m ≤ n) → A → Vec A m → Vec A n -padRight {n = _} _ a [] = replicate _ a +padRight {n = n} _ a [] = replicate n a padRight {n = suc _} le a (x ∷ xs) = x ∷ padRight (s≤s⁻¹ le) a xs ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 73459b360f..c7f2d0f547 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -11,14 +11,16 @@ 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ℕ<; _↑ˡ_; _↑ʳ_) + using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_; inject≤) open import Data.List.Base as List using (List) import Data.List.Properties as List open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s; uncurry) open import Data.Sum.Base using ([_,_]′) @@ -136,47 +138,31 @@ truncate-refl : (xs : Vec A n) → truncate ≤-refl xs ≡ xs truncate-refl [] = refl truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs) -truncate-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) → - truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs) -truncate-trans z≤n n≤p xs = refl -truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs) +truncate-trans : ∀ .(m≤n : m ≤ n) .(n≤o : n ≤ o) (xs : Vec A o) → + truncate (≤-trans m≤n n≤o) xs ≡ truncate m≤n (truncate n≤o xs) +truncate-trans {m = zero} _ _ _ = refl +truncate-trans {m = suc _} {n = suc _} m≤n n≤o (x ∷ xs) = + cong (x ∷_) (truncate-trans (s≤s⁻¹ m≤n) (s≤s⁻¹ n≤o) xs) -truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ -truncate-irrelevant m≤n₁ m≤n₂ xs = cong (λ m≤n → truncate m≤n xs) (≤-irrelevant m≤n₁ m≤n₂) - -truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → +truncate≡take : .(m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs) -truncate≡take z≤n _ eq = refl -truncate≡take (s≤s m≤n) (x ∷ xs) eq = cong (x ∷_) (truncate≡take m≤n xs (suc-injective eq)) +truncate≡take {m = zero} _ _ _ = refl +truncate≡take {m = suc _} m≤n (x ∷ xs) eq = + cong (x ∷_) (truncate≡take (s≤s⁻¹ m≤n) xs (suc-injective eq)) take≡truncate : ∀ m (xs : Vec A (m + n)) → take m xs ≡ truncate (m≤m+n m n) xs take≡truncate zero _ = refl take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs) ------------------------------------------------------------------------- --- pad - -padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs -padRight-refl a [] = refl -padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) - -padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m≤n a (replicate m a) -padRight-replicate z≤n a = refl -padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a) - -padRight-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (a : A) (xs : Vec A m) → - padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs) -padRight-trans z≤n n≤p a [] = padRight-replicate n≤p a -padRight-trans (s≤s m≤n) (s≤s n≤p) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤p a xs) - ------------------------------------------------------------------------ -- truncate and padRight together -truncate-padRight : (m≤n : m ≤ n) (a : A) (xs : Vec A m) → +truncate-padRight : .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → truncate m≤n (padRight m≤n a xs) ≡ xs -truncate-padRight z≤n a [] = refl -truncate-padRight (s≤s m≤n) a (x ∷ xs) = cong (x ∷_) (truncate-padRight m≤n a xs) +truncate-padRight _ a [] = refl +truncate-padRight {n = suc _} m≤n a (x ∷ xs) = + cong (x ∷_) (truncate-padRight (s≤s⁻¹ m≤n) a xs) ------------------------------------------------------------------------ -- lookup @@ -203,10 +189,10 @@ lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero refl = refl []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p = []=⇒lookup∘lookup⇒[]= xs i p -lookup-truncate : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → +lookup-truncate : .(m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) → lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n) -lookup-truncate (s≤s m≤m+n) (_ ∷ _) zero = refl -lookup-truncate (s≤s m≤m+n) (_ ∷ xs) (suc i) = lookup-truncate m≤m+n xs i +lookup-truncate _ (_ ∷ _) zero = refl +lookup-truncate m≤n (_ ∷ xs) (suc i) = lookup-truncate (suc[m]≤n⇒m≤pred[n] m≤n) xs i lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) → lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n)) @@ -1143,6 +1129,10 @@ sum-++ {ys = ys} (x ∷ xs) = begin ------------------------------------------------------------------------ -- replicate +cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x +cast-replicate {m = zero} {n = zero} _ _ = refl +cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x) + lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate n x) i ≡ x lookup-replicate zero x = refl lookup-replicate (suc i) x = lookup-replicate i x @@ -1184,6 +1174,67 @@ toList-replicate : ∀ (n : ℕ) (x : A) → toList-replicate zero x = refl toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x) +------------------------------------------------------------------------ +-- pad + +padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs +padRight-refl a [] = refl +padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) + +padRight-replicate : ∀ .(m≤n : m ≤ n) (a : A) → + replicate n a ≡ padRight m≤n a (replicate m a) +padRight-replicate {m = zero} _ a = refl +padRight-replicate {m = suc _} {n = suc _} m≤n a = + cong (a ∷_) (padRight-replicate (s≤s⁻¹ m≤n) a) + +padRight-trans : ∀ .(m≤n : m ≤ n) .(n≤o : n ≤ o) (a : A) (xs : Vec A m) → + padRight (≤-trans m≤n n≤o) a xs ≡ padRight n≤o a (padRight m≤n a xs) +padRight-trans _ n≤o a [] = padRight-replicate n≤o a +padRight-trans {n = suc _} {o = suc _} m≤n n≤o a (x ∷ xs) = + cong (x ∷_) (padRight-trans (s≤s⁻¹ m≤n) (s≤s⁻¹ n≤o) a xs) + +padRight-lookup : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → + lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i +padRight-lookup {n = suc _} _ a (x ∷ xs) zero = refl +padRight-lookup {n = suc _} m≤n a (x ∷ xs) (suc i) = padRight-lookup (s≤s⁻¹ m≤n) a xs i + +padRight-map : ∀ (f : A → B) .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) +padRight-map f _ a [] = map-replicate f a _ +padRight-map {n = suc _} f m≤n a (x ∷ xs) = cong (f x ∷_) (padRight-map f (s≤s⁻¹ m≤n) a xs) + +padRight-zipWith : ∀ (f : A → B → C) .(m≤n : m ≤ n) (a : A) (b : B) + (xs : Vec A m) (ys : Vec B m) → + zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys) +padRight-zipWith f _ a b [] [] = zipWith-replicate f a b +padRight-zipWith {n = suc _} f m≤n a b (x ∷ xs) (y ∷ ys) = + cong (f x y ∷_) (padRight-zipWith f (s≤s⁻¹ m≤n) a b xs ys) + +padRight-zipWith₁ : ∀ (f : A → B → C) .(m≤n : m ≤ n) .(n≤o : n ≤ o) + (a : A) (b : B) (xs : Vec A n) (ys : Vec B m) → + zipWith f (padRight n≤o a xs) (padRight (≤-trans m≤n n≤o) b ys) ≡ + padRight n≤o (f a b) (zipWith f xs (padRight m≤n b ys)) +padRight-zipWith₁ f m≤n n≤o a b xs ys = + trans (cong (zipWith f (padRight n≤o a xs)) (padRight-trans m≤n n≤o b ys)) + (padRight-zipWith f n≤o a b xs (padRight m≤n b ys)) + +padRight-drop : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → + drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a +padRight-drop {m = zero} _ a [] eq = cast-replicate eq a +padRight-drop {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = padRight-drop (s≤s⁻¹ m≤n) a xs (suc-injective eq) + +padRight-take : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → + take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs +padRight-take {m = zero} _ a [] _ = refl +padRight-take {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = cong (x ∷_) (padRight-take (s≤s⁻¹ m≤n) a xs (suc-injective eq)) + +padRight-updateAt : ∀ .(m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) → + updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ + padRight m≤n x (updateAt xs i f) +padRight-updateAt {n = suc _} m≤n (y ∷ xs) f zero x = refl +padRight-updateAt {n = suc _} m≤n (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt (s≤s⁻¹ m≤n) xs f i x) + + ------------------------------------------------------------------------ -- iterate @@ -1576,3 +1627,13 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin "Warning: lookup-inject≤-take was deprecated in v2.0. Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead." #-} + +-- Version 2.4 + +truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂ +truncate-irrelevant _ _ xs = refl +{-# WARNING_ON_USAGE truncate-irrelevant +"Warning: truncate-irrelevant was deprecated in v2.4. +Definition of truncate has been made definitionally proof-irrelevant." +#-} + From 81457f77cf7b6c108def4cc412183e0aa67173cc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 3 Aug 2025 17:41:13 +0100 Subject: [PATCH 3/7] fix: deprecation in `CHANGELOG` --- CHANGELOG.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 68d813b590..489b6dbc99 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,7 +22,8 @@ Minor improvements backwards compatible, but does change the equational behaviour of these functions to be more eager, because no longer blocking on pattern matching on that argument. Corresponding changes have been made to the types of their - properties (and their proofs). + properties (and their proofs). In particular, `truncate-irrelevant` is now + deprecated, because definitionally trivial. * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is @@ -48,6 +49,11 @@ Deprecated names interchange ↦ medial ``` +* In `Data.Vec.Properties`: + ```agda + truncate-irrelevant ↦ + ``` + New modules ----------- From a460f9cea7f0af1869222d7a219b1161b89904a3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 5 Aug 2025 07:25:35 +0100 Subject: [PATCH 4/7] fix: duplication after resolving merge conflict --- src/Data/Vec/Properties.agda | 59 ------------------------------------ 1 file changed, 59 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index cf4d54f3c5..f8a946ccda 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1174,65 +1174,6 @@ toList-replicate : ∀ (n : ℕ) (x : A) → toList-replicate zero x = refl toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x) -cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x -cast-replicate {m = zero} {n = zero} _ _ = refl -cast-replicate {m = suc _} {n = suc _} m≡n x = cong (x ∷_) (cast-replicate (suc-injective m≡n) x) - ------------------------------------------------------------------------- --- pad - -padRight-refl : (a : A) (xs : Vec A n) → padRight ≤-refl a xs ≡ xs -padRight-refl a [] = refl -padRight-refl a (x ∷ xs) = cong (x ∷_) (padRight-refl a xs) - -padRight-replicate : (m≤n : m ≤ n) (a : A) → replicate n a ≡ padRight m≤n a (replicate m a) -padRight-replicate z≤n a = refl -padRight-replicate (s≤s m≤n) a = cong (a ∷_) (padRight-replicate m≤n a) - -padRight-trans : ∀ (m≤n : m ≤ n) (n≤o : n ≤ o) (a : A) (xs : Vec A m) → - padRight (≤-trans m≤n n≤o) a xs ≡ padRight n≤o a (padRight m≤n a xs) -padRight-trans z≤n n≤o a [] = padRight-replicate n≤o a -padRight-trans (s≤s m≤n) (s≤s n≤o) a (x ∷ xs) = cong (x ∷_) (padRight-trans m≤n n≤o a xs) - -padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → - lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i -padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl -padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i - -padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → - map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) -padRight-map f z≤n a [] = map-replicate f a _ -padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs) - -padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) - (xs : Vec A m) (ys : Vec B m) → - zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys) -padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b -padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys) - -padRight-zipWith₁ : ∀ (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) - (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) → - zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡ - padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys)) -padRight-zipWith₁ f o≤m m≤n a b xs ys = trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans o≤m m≤n b ys)) - (padRight-zipWith f m≤n a b xs (padRight o≤m b ys)) - -padRight-take : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → - take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs -padRight-take m≤n a [] n≡m+o = refl -padRight-take (s≤s m≤n) a (x ∷ xs) n≡m+o = cong (x ∷_) (padRight-take m≤n a xs (suc-injective n≡m+o)) - -padRight-drop : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → - drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a -padRight-drop {m = zero} z≤n a [] n≡m+o = cast-replicate n≡m+o a -padRight-drop {m = suc _} {n = suc _} (s≤s m≤n) a (x ∷ xs) n≡m+o = padRight-drop m≤n a xs (suc-injective n≡m+o) - -padRight-updateAt : ∀ (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) → - updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ - padRight m≤n x (updateAt xs i f) -padRight-updateAt {n = suc _} (s≤s m≤n) x (y ∷ xs) f zero = refl -padRight-updateAt {n = suc _} (s≤s m≤n) x (y ∷ xs) f (suc i) = cong (y ∷_) (padRight-updateAt m≤n x xs f i) - ------------------------------------------------------------------------ -- pad From 42efbfe956744bbb39eb24acb2329beda69d5116 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 5 Aug 2025 07:30:01 +0100 Subject: [PATCH 5/7] fix: alignment --- src/Data/Vec/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index f8a946ccda..2ef6f465f5 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1130,7 +1130,7 @@ sum-++ {ys = ys} (x ∷ xs) = begin -- replicate cast-replicate : ∀ .(m≡n : m ≡ n) (x : A) → cast m≡n (replicate m x) ≡ replicate n x -cast-replicate {m = zero} {n = zero} _ _ = refl +cast-replicate {m = zero} {n = zero} _ _ = refl cast-replicate {m = suc _} {n = suc _} eq x = cong (x ∷_) (cast-replicate (suc-injective eq) x) lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate n x) i ≡ x From 49e31f5285487a5dc3377f941e2a47fd13b84ca8 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 5 Aug 2025 08:10:24 +0100 Subject: [PATCH 6/7] add: specialised versions of `padRight-drop` and `padRight-take` --- CHANGELOG.md | 8 ++++++++ src/Data/Vec/Properties.agda | 16 ++++++++++++++-- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8b843939e5..6ab28e935c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -106,8 +106,16 @@ Additions to existing modules padRight-take : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs + padRight-take′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in take m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ xs + padRight-drop : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a + padRight-drop′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in drop m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ replicate o a + padRight-updateAt : (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) → updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f) ``` diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 2ef6f465f5..3f03235c76 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -19,7 +19,7 @@ open import Data.Nat.Base open import Data.Nat.Properties using (suc-injective; +-assoc; +-comm; +-suc; +-identityʳ ; m≤n⇒m≤1+n; m≤m+n; suc[m]≤n⇒m≤pred[n] - ; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″ + ; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; m≤n⇒∃[o]m+o≡n ) open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry) @@ -1223,18 +1223,30 @@ padRight-drop : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ padRight-drop {m = zero} _ a [] eq = cast-replicate eq a padRight-drop {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = padRight-drop (s≤s⁻¹ m≤n) a xs (suc-injective eq) +padRight-drop′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in drop m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ replicate o a +padRight-drop′ m≤n a xs = let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in padRight-drop m≤n a xs (sym n≡m+o) + padRight-take : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs padRight-take {m = zero} _ a [] _ = refl padRight-take {m = suc _} {n = suc _} m≤n a (x ∷ xs) eq = cong (x ∷_) (padRight-take (s≤s⁻¹ m≤n) a xs (suc-injective eq)) +padRight-take′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → + let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in take m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ xs +padRight-take′ m≤n a xs = let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n + in padRight-take m≤n a xs (sym n≡m+o) + padRight-updateAt : ∀ .(m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) → updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f) padRight-updateAt {n = suc _} m≤n (y ∷ xs) f zero x = refl padRight-updateAt {n = suc _} m≤n (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt (s≤s⁻¹ m≤n) xs f i x) - +-- ------------------------------------------------------------------------ -- iterate From 42ac317156351fdff84bb824fd1c5fb5e10f8381 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 5 Aug 2025 08:11:23 +0100 Subject: [PATCH 7/7] fix: whitespace --- src/Data/Vec/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 3f03235c76..101c54169c 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1227,7 +1227,7 @@ padRight-drop′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n in drop m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ replicate o a padRight-drop′ m≤n a xs = let o , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n - in padRight-drop m≤n a xs (sym n≡m+o) + in padRight-drop m≤n a xs (sym n≡m+o) padRight-take : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs @@ -1238,7 +1238,7 @@ padRight-take′ : ∀ .(m≤n : m ≤ n) (a : A) (xs : Vec A m) → let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n in take m (cast (sym n≡m+o) (padRight m≤n a xs)) ≡ xs padRight-take′ m≤n a xs = let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n - in padRight-take m≤n a xs (sym n≡m+o) + in padRight-take m≤n a xs (sym n≡m+o) padRight-updateAt : ∀ .(m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) → updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡