Add proofs take-step and lookup-inject≤-take (#1250)

Author: umazalakain

CHANGELOG.md

@@ -452,6 +452,13 @@ Other minor additions
   inject≤-injective : (n≤m : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m → x ≡ y
   ```
 
+* Added new proofs to `Data.Vec.Properties`:
+  ```agda
+  unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
+  lookup-inject≤-take : ∀ m {n} (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
+                        lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
+  ```
+
 * Added new functions to `Data.Vec.Functional`:
   ```agda
   length : ∀ {n} → Vector A n → ℕ

src/Data/Vec/Properties.agda

@@ -69,6 +69,13 @@ module _ {n} {x y : A} {xs ys : Vec A n} where
 
 -- See also Data.Vec.Properties.WithK.[]=-irrelevant.
 
+------------------------------------------------------------------------
+-- take
+
+unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
+unfold-take n x xs with splitAt n xs
+unfold-take n x .(xs ++ ys) | xs , ys , refl = refl
+
 ------------------------------------------------------------------------
 -- lookup
 
@@ -102,6 +109,15 @@ lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
   []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p    =
     []=⇒lookup∘lookup⇒[]= xs i p
 
+lookup-inject≤-take : ∀ m {n} (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
+                      lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
+lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs)
+  rewrite unfold-take m x xs = refl
+lookup-inject≤-take (suc (suc m)) m≤m+n (suc zero) (x ∷ x' ∷ xs)
+  rewrite unfold-take (suc m) x (x' ∷ xs) | unfold-take m x' xs = refl
+lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ x' ∷ xs)
+  rewrite unfold-take (suc m) x (x' ∷ xs) | unfold-take m x' xs = lookup-inject≤-take m m≤m+n i xs
+
 ------------------------------------------------------------------------
 -- updateAt (_[_]%=_)