diff --git a/CHANGELOG.md b/CHANGELOG.md index f28e0f0e05..bc558ac5ba 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -444,6 +444,24 @@ Additions to existing modules fromList-reverse : (xs : List A) → (fromList (List.reverse xs)) ≈[ List.length-reverse xs ] reverse (fromList xs) fromList∘toList : ∀ (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] 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-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-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 → 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-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-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-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) ``` * In `Data.Product.Nary.NonDependent`: diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 73459b360f..73d8d94f26 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ℕ<; _↑ˡ_; _↑ʳ_) + 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 @@ -154,22 +154,6 @@ take≡truncate : ∀ m (xs : Vec A (m + n)) → 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 @@ -1184,13 +1168,71 @@ 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) + ------------------------------------------------------------------------ -- iterate iterate-id : ∀ (x : A) n → iterate id x n ≡ replicate n x iterate-id x zero = refl iterate-id x (suc n) = cong (_ ∷_) (iterate-id (id x) n) - take-iterate : ∀ n f (x : A) → take n (iterate f x (n + m)) ≡ iterate f x n take-iterate zero f x = refl take-iterate (suc n) f x = cong (_ ∷_) (take-iterate n f (f x))