Add padRight and truncate to Data.Vec, and prove some properties

CHANGELOG.md

@@ -696,6 +696,8 @@ Other minor changes
   ```agda
   diagonal : ∀ {n} → Vec (Vec A n) n → Vec A n
   DiagonalBind._>>=_ : ∀ {n} → Vec A n → (A → Vec B n) → Vec B n
+  truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m
+  pad : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n
   ```
 
 * Added new instance in `Data.Vec.Categorical`:
@@ -708,8 +710,17 @@ Other minor changes
   map-const : ∀ {n} (xs : Vec A n) (x : B) → map {n = n} (const x) xs ≡ replicate x
   map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) → (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs
   ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs)
+  padRight-refl : ∀ {n} → (a : A) → (xs : Vec A n) → padRight ≤-refl a xs ≡ xs
+  padRight-replicate : ∀ {m n} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a)
+  padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) →
+              padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs)
   transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs
   []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y)
+
+  truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs
+  truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) →
+                   truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs)
+  truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs
   ```
 
 * Added new proofs in `Function.Construct.Symmetry`:

src/Data/Vec/Base.agda

@@ -8,7 +8,7 @@
 
 module Data.Vec.Base where
 
-open import Data.Bool.Base
+open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
@@ -266,6 +266,19 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
 uncons : ∀ {n} → Vec A (suc n) → A × Vec A n
 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 z≤n      _        = []
+truncate (s≤s le) (x ∷ xs) = x ∷ (truncate 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
+
 ------------------------------------------------------------------------
 -- Operations for converting between lists
 

src/Data/Vec/Properties.agda

@@ -14,7 +14,8 @@ open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
-open import Data.Nat.Properties using (+-assoc; ≤-step)
+open import Data.Nat.Properties
+  using (+-assoc; ≤-step; ≤-refl; ≤-trans)
 open import Data.Product as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -25,7 +26,7 @@ open import Function.Inverse using (_↔_; inverse)
 open import Level using (Level)
 open import Relation.Binary as B hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as P
-  using (_≡_; _≢_; refl; _≗_; cong₂)
+  using (_≡_; _≢_; refl; _≗_; cong; cong₂)
 open P.≡-Reasoning
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary using (Dec; does; yes; no)
@@ -155,6 +156,41 @@ take-drop-id (suc m) (x ∷ xs) = begin
     x ∷ xs
   ∎
 
+--------------------------------------------------------------------------------
+-- truncate
+
+truncate-refl : ∀ {n} → (xs : Vec A n) → truncate ≤-refl xs ≡ xs
+truncate-refl []       = refl
+truncate-refl (x ∷ xs) = cong (x ∷_) (truncate-refl xs)
+
+truncate-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (xs : Vec A p) →
+                 truncate (≤-trans le₁ le₂) xs ≡ truncate le₁ (truncate le₂ xs)
+truncate-trans z≤n       le₂       xs = refl
+truncate-trans (s≤s le₁) (s≤s le₂) (x ∷ xs) = cong (x ∷_) (truncate-trans le₁ le₂ xs)
+
+--------------------------------------------------------------------------------
+-- pad
+
+padRight-refl : ∀ {n} → (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} → (le : m ≤ n) → (a : A) → replicate a ≡ padRight le a (replicate a)
+padRight-replicate z≤n      a = refl
+padRight-replicate (s≤s le) a = cong (a ∷_) (padRight-replicate le a)
+
+padRight-trans : ∀ {m n p} → (le₁ : m ≤ n) → (le₂ : n ≤ p) → (a : A) → (xs : Vec A m) →
+            padRight (≤-trans le₁ le₂) a xs ≡ padRight le₂ a (padRight le₁ a xs)
+padRight-trans z≤n       le₂       a []       = padRight-replicate le₂ a
+padRight-trans (s≤s le₁) (s≤s le₂) a (x ∷ xs) = cong (x ∷_) (padRight-trans le₁ le₂ a xs)
+
+--------------------------------------------------------------------------------
+-- truncate and padRight together
+
+truncate-padRight-id : ∀ {m n} → (le : m ≤ n) → (a : A) → (xs : Vec A m) → truncate le (padRight le a xs) ≡ xs
+truncate-padRight-id z≤n      a []       = refl
+truncate-padRight-id (s≤s le) a (x ∷ xs) = cong (x ∷_) (truncate-padRight-id le a xs)
+
 ------------------------------------------------------------------------
 -- lookup