[Add] truncate properties to Data.Vec.Properties

CHANGELOG.md

@@ -43,3 +43,27 @@ Additions to existing modules
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```
 
+* In `Data.Vec.Properties`:
+  ```agda
+  updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
+                  updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+
+  truncate-zipWith : (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) (f : A → B → C) →
+                    truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+
+  truncate-zipWith-truncate : (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o) (xs : Vec A o) (ys : Vec B n) →
+                              truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡
+                              zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys)
+
+  truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
+                      updateAt (truncate m≤n xs) i f ≡
+                      truncate m≤n (updateAt xs (inject≤ i m≤n) f)
+
+  updateAt-truncate : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
+                      updateAt (truncate (m≤m+n m n) xs) i f ≡
+                      truncate (m≤m+n m n) (updateAt xs (inject≤ i (m≤m+n m n)) f)
+
+  map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →
+                map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+
+  ```

src/Data/Vec/Properties.agda

@@ -11,14 +11,14 @@ 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<s⁻¹; _≥_; s≤s⁻¹; z≤n)
+  using (ℕ; zero; suc; _+_; _≤_; _<_; s≤s; pred; s<s⁻¹; _≥_; s≤s⁻¹; z≤n; _∸_)
 open import Data.Nat.Properties
   using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″
-        ; suc-injective; +-comm; +-suc; +-identityʳ)
+        ; suc-injective; +-comm; +-suc; +-identityʳ; m≤n⇒∃[o]m+o≡n)
 open import Data.Product.Base as Product
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -104,6 +104,11 @@ take-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) →
 take-map f zero    xs       = refl
 take-map f (suc m) (x ∷ xs) = cong (f x ∷_) (take-map f m xs)
 
+updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
+                updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
+updateAt-take (_ ∷ _ ) zero    f = refl
+updateAt-take (x ∷ xs) (suc i) f = cong (x ∷_) (updateAt-take xs i f)
+
 ------------------------------------------------------------------------
 -- drop
 
@@ -154,6 +159,37 @@ take≡truncate : ∀ m (xs : Vec A (m + n)) →
 take≡truncate zero    _        = refl
 take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs)
 
+truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
+  truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+truncate-zipWith f z≤n xs ys = refl
+truncate-zipWith f (s≤s m≤n) (x ∷ xs) (y ∷ ys) =
+  cong (f x y ∷_) (truncate-zipWith f m≤n xs ys)
+
+truncate-zipWith-truncate : ∀ (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o)
+  (xs : Vec A o) (ys : Vec B n) →
+  truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡
+  zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys)
+truncate-zipWith-truncate f m≤n n≤o xs ys =
+  trans (truncate-zipWith f m≤n (truncate n≤o xs) ys)
+  (cong (λ zs → zipWith f zs (truncate m≤n ys)) ((sym (truncate-trans m≤n n≤o xs))))
+
+truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
+                    updateAt (truncate m≤n xs) i f ≡ truncate m≤n (updateAt xs (inject≤ i m≤n) f)
+truncate-updateAt (s≤s _  ) (_ ∷ _ ) zero f = refl
+truncate-updateAt (s≤s m≤n) (x ∷ xs) (suc i) f = cong (x ∷_) (truncate-updateAt m≤n xs i f)
+
+module _ (xs : Vec A (m + n)) (i : Fin m) (f : A → A) where
+  private
+    i′ = inject≤ i (m≤m+n m n)
+
+  updateAt-truncate : updateAt (truncate (m≤m+n m n) xs) i f ≡ truncate (m≤m+n m n) (updateAt xs i′ f)
+  updateAt-truncate = begin
+    updateAt (truncate (m≤m+n m n) xs) i f ≡⟨ cong (λ l → updateAt l i f) (take≡truncate m xs) ⟨
+    updateAt (take m xs) i f         ≡⟨ updateAt-take xs i f ⟩
+    take m (updateAt xs i′ f)        ≡⟨ take≡truncate m (updateAt xs i′ f) ⟩
+    truncate (m≤m+n m n) (updateAt xs i′ f) ∎
+    where open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- pad
 
@@ -472,6 +508,19 @@ toList-map : ∀ (f : A → B) (xs : Vec A n) →
 toList-map f [] = refl
 toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 
+map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →
+  map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+map-truncate {m = m} {n = n} f m≤n xs =
+  let _ , n≡m+o = m≤n⇒∃[o]m+o≡n m≤n
+  in begin
+    map f (truncate m≤n xs)              ≡⟨ cong (map f) (truncate≡take m≤n xs (sym n≡m+o)) ⟩
+    map f (take m (cast (sym n≡m+o) xs)) ≡⟨ sym (take-map f m _) ⟩
+    take m (map f (cast (sym n≡m+o) xs)) ≡⟨ cong (take m) (map-cast f (sym n≡m+o) xs) ⟩
+    take m (cast (sym n≡m+o) (map f xs)) ≡⟨ sym (truncate≡take m≤n (map f xs) (sym n≡m+o)) ⟩
+    truncate m≤n (map f xs)              ∎
+  where
+    open ≡-Reasoning
+
 ------------------------------------------------------------------------
 -- _++_