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

CHANGELOG.md

@@ -457,7 +457,7 @@ Major improvements
 * Previously the division and modulus operators were defined in `Data.Nat.DivMod`
   which in turn meant that using them required importing `Data.Nat.Properties`
   which is a very heavy dependency.
-  
+
 * To fix this, these operators have been moved to `Data.Nat.Base`. The properties
   for them still live in `Data.Nat.DivMod` (which also publicly re-exports them
   to provide backwards compatability).
@@ -823,7 +823,7 @@ New modules
   -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
   -‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
   ```
-  
+
 
 Other minor changes
 -------------------
@@ -875,14 +875,14 @@ Other minor changes
   ring : Ring a ℓ₁ → Ring b ℓ₂ → Ring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   commutativeRing : CommutativeRing a ℓ₁ → CommutativeRing b ℓ₂ →
                     CommutativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-  rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ → 
+  rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ →
                   RawQuasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-  unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → 
+  unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ →
                 UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-  invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → 
+  invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ →
                     InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
-  invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ → 
+  invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ →
                           InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
   loop : Loop a ℓ₁ → Loop b ℓ₂ → Loop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
@@ -977,7 +977,7 @@ Other minor changes
   combine-injectiveʳ : combine x y ≡ combine x z → y ≡ z
   combine-injective  : combine x y ≡ combine w z → x ≡ w × y ≡ z
   combine-surjective : ∀ x → ∃₂ λ y z → combine y z ≡ x
-  
+
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
   ```
 
@@ -1044,11 +1044,11 @@ Other minor changes
   m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
-  
+
   1≤n!    : 1 ≤ n !
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)
-  
+
   anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
   allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
   ```
@@ -1173,6 +1173,9 @@ Other minor changes
 
 * Added new definitions in `Data.Vec.Base`:
   ```agda
+  truncate : m ≤ n → Vec A n → Vec A m
+  pad      : m ≤ n → A → Vec A m → Vec A n
+
   FoldrOp A B = ∀ {n} → A → B n → B (suc n)
   FoldlOp A B = ∀ {n} → B n → A → B (suc n)
 
@@ -1191,6 +1194,14 @@ Other minor changes
 
 * Added new proofs in `Data.Vec.Properties`:
   ```agda
+  padRight-refl      : padRight ≤-refl a xs ≡ xs
+  padRight-replicate : replicate a ≡ padRight le a (replicate a)
+  padRight-trans     : padRight (≤-trans m≤n n≤p) a xs ≡ padRight n≤p a (padRight m≤n a xs)
+
+  truncate-refl     : truncate ≤-refl xs ≡ xs
+  truncate-trans    : truncate (≤-trans m≤n n≤p) xs ≡ truncate m≤n (truncate n≤p xs)
+  truncate-padRight : truncate m≤n (padRight m≤n a xs) ≡ xs
+
   map-const    : map (const x) xs ≡ replicate x
   map-⊛        : map f xs ⊛ map g xs ≡ map (f ˢ g) xs
   map-++       : map f (xs ++ ys) ≡ map f xs ++ map f ys

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)
@@ -278,6 +278,19 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
 uncons : 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

@@ -13,7 +13,8 @@ open import Data.Bool.Base using (true; false)
 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 ([_,_]′)
@@ -152,6 +153,42 @@ take-drop-id (suc m) (x ∷ xs) = begin
     x ∷ xs
   ∎
 
+--------------------------------------------------------------------------------
+-- truncate
+
+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)
+
+--------------------------------------------------------------------------------
+-- 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 a ≡ padRight m≤n a (replicate 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 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)
+
 ------------------------------------------------------------------------
 -- lookup
 
@@ -1039,4 +1076,3 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ instead."
 #-}
-