Additional lemmas about lists and vectors (#2020)

Author: amblafont

CHANGELOG.md

@@ -2203,6 +2203,7 @@ Other minor changes
   ```agda
   mapWith∈-id  : mapWith∈ xs (λ {x} _ → x) ≡ xs
   map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f)
+  index-injective : index x₁∈xs ≡ index x₂∈xs → x₁ ≈ x₂
   ```
 
 * Add new proofs in `Data.List.Properties`:
@@ -2231,6 +2232,8 @@ Other minor changes
 
   take-[] : ∀ m → take  m [] ≡ []
   drop-[] : ∀ m → drop  m [] ≡ []
+
+  map-replicate : map f (replicate n x) ≡ replicate n (f x)
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2599,6 +2602,8 @@ Other minor changes
   map-∷ʳ       : map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x)
   map-reverse  : map f (reverse xs) ≡ reverse (map f xs)
   map-ʳ++      : map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
+  map-insert   : map f (insert xs i x) ≡ insert (map f xs) i (f x)
+  toList-map   : toList (map f xs) ≡ List.map f (toList xs)
 
   lookup-concat : lookup (concat xss) (combine i j) ≡ lookup (lookup xss i) j
 
@@ -2633,6 +2638,9 @@ Other minor changes
   reverse-injective  : reverse xs ≡ reverse ys → xs ≡ ys
 
   transpose-replicate : transpose (replicate xs) ≡ map replicate xs
+  toList-replicate    : toList (replicate {n = n} a) ≡ List.replicate n a
+
+  toList-++ : toList (xs ++ ys) ≡ toList xs List.++ toList ys
 
   toList-cast   : toList (cast eq xs) ≡ toList xs
   cast-is-id    : cast eq xs ≡ xs
@@ -2642,6 +2650,13 @@ Other minor changes
   lookup-cast   : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
+
+  zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
+  ```
+
+* Added new proofs in `Data.Vec.Membership.Propositional.Properties`:
+  ```agda
+  index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs
   ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:

src/Data/List/Membership/Setoid/Properties.agda

@@ -11,6 +11,7 @@ module Data.List.Membership.Setoid.Properties where
 open import Algebra using (Op₂; Selective)
 open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List.Base
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Relation.Unary.All as All using (All)
@@ -62,6 +63,13 @@ module _ (S : Setoid c ℓ) where
   ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
   ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)
 
+  -- index is injective in its first argument.
+
+  index-injective : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
+                    Any.index x₁∈xs ≡ Any.index x₂∈xs → x₁ ≈ x₂
+  index-injective (here x₁≈x)   (here x₂≈x)   _  = trans x₁≈x (sym x₂≈x)
+  index-injective (there x₁∈xs) (there x₂∈xs) eq = index-injective x₁∈xs x₂∈xs (suc-injective eq)
+
 ------------------------------------------------------------------------
 -- Irrelevance
 

src/Data/List/Properties.agda

@@ -118,6 +118,10 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
   let fx≡fy , fxs≡fys = ∷-injective eq in
   cong₂ _∷_ (finj fx≡fy) (map-injective finj fxs≡fys)
 
+map-replicate : ∀ (f : A → B) n x → map f (replicate n x) ≡ replicate n (f x)
+map-replicate f zero    x = refl
+map-replicate f (suc n) x = cong (_ ∷_) (map-replicate f n x)
+
 ------------------------------------------------------------------------
 -- mapMaybe
 

src/Data/Vec/Membership/Propositional/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Product.Base using (_,_; ∃; _×_; -,_; map₁; map₂)
 open import Data.Vec.Base
 open import Data.Vec.Relation.Unary.Any using (here; there)
 open import Data.List.Base using ([]; _∷_)
-open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.List.Relation.Unary.Any as ListAny using (here; there)
 open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Vec.Membership.Propositional
 open import Data.List.Membership.Propositional
@@ -102,6 +102,11 @@ index-∈-lookup (suc i) (x ∷ xs) = cong suc (index-∈-lookup i xs)
 ∈-fromList⁻ {xs = _ ∷ _} (here refl)  = here refl
 ∈-fromList⁻ {xs = _ ∷ _} (there v∈xs) = there (∈-fromList⁻ v∈xs)
 
+index-∈-fromList⁺ : ∀ {v : A} {xs} → (v∈xs : v ∈ₗ xs) →
+                    Any.index (∈-fromList⁺ v∈xs) ≡ ListAny.index v∈xs
+index-∈-fromList⁺ (here refl) = refl
+index-∈-fromList⁺ (there v∈xs) = cong suc (index-∈-fromList⁺ v∈xs)
+
 ------------------------------------------------------------------------
 -- Relationship to Any
 

src/Data/Vec/Properties.agda

@@ -448,6 +448,12 @@ map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B}
 map-updateAt (x ∷ xs) zero    eq = cong (_∷ _) eq
 map-updateAt (x ∷ xs) (suc i) eq = cong (_ ∷_) (map-updateAt xs i eq)
 
+map-insert : ∀ (f : A → B) (x : A) (xs : Vec A n) (i : Fin (suc n)) →
+             map f (insert xs i x) ≡ insert (map f xs) i (f x)
+map-insert f _ []        Fin.zero = refl
+map-insert f _ (x' ∷ xs) Fin.zero = refl
+map-insert f x (x' ∷ xs) (Fin.suc i) = cong (_ ∷_) (map-insert f x xs i)
+
 map-[]≔ : ∀ (f : A → B) (xs : Vec A n) (i : Fin n) →
           map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
 map-[]≔ f xs i = map-updateAt xs i refl
@@ -457,6 +463,11 @@ map-⊛ : ∀ (f : A → B → C) (g : A → B) (xs : Vec A n) →
 map-⊛ f g []       = refl
 map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs)
 
+toList-map : ∀ (f : A → B) (xs : Vec A n) →
+             toList (map f xs) ≡ List.map f (toList xs)
+toList-map f [] = refl
+toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
+
 ------------------------------------------------------------------------
 -- _++_
 
@@ -509,6 +520,11 @@ lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans
   (lookup-splitAt m xs ys i)
   (sym ([,]-map (Fin.splitAt m i)))
 
+toList-++ : (xs : Vec A n) (ys : Vec A m) →
+            toList (xs ++ ys) ≡ toList xs List.++ toList ys
+toList-++ []       ys = refl
+toList-++ (x ∷ xs) ys = cong (x List.∷_) (toList-++ xs ys)
+
 ------------------------------------------------------------------------
 -- concat
 
@@ -645,6 +661,15 @@ lookup-zipWith : ∀ (f : A → B → C) (i : Fin n) xs ys →
 lookup-zipWith _ zero    (x ∷ _)  (y ∷ _)   = refl
 lookup-zipWith _ (suc i) (_ ∷ xs) (_ ∷ ys)  = lookup-zipWith _ i xs ys
 
+zipWith-++ : ∀ (f : A → B → C)
+             (xs : Vec A n) (ys : Vec A m)
+             (xs' : Vec B n) (ys' : Vec B m) →
+             zipWith f (xs ++ ys) (xs' ++ ys') ≡
+             zipWith f xs xs' ++ zipWith f ys ys'
+zipWith-++ f []       ys []         ys' = refl
+zipWith-++ f (x ∷ xs) ys (x' ∷ xs') ys' =
+  cong (_ ∷_) (zipWith-++ f xs ys xs' ys')
+
 ------------------------------------------------------------------------
 -- zip
 
@@ -1002,6 +1027,11 @@ zipWith-replicate₂ _⊕_ []       y = refl
 zipWith-replicate₂ _⊕_ (x ∷ xs) y =
   cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
 
+toList-replicate : ∀ (n : ℕ) (x : A) →
+                   toList (replicate {n = n} a) ≡ List.replicate n a
+toList-replicate zero    x = refl
+toList-replicate (suc n) x = cong (_ List.∷_) (toList-replicate n x)
+
 ------------------------------------------------------------------------
 -- tabulate