Add properties of Vector operations reverse, _++_ and fromList (#…

…2045)

CHANGELOG.md

@@ -2684,16 +2684,27 @@ Other minor changes
 
  toList-++ : toList (xs ++ ys) ≡ toList xs List.++ toList ys
 
- toList-cast : toList (cast eq xs) ≡ toList xs
  cast-is-id : cast eq xs ≡ xs
  subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs
  cast-trans : cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
  map-cast : map f (cast eq xs) ≡ cast eq (map f xs)
  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
+ cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
 
  zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
+
+ ++-assoc : cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+ ++-identityʳ : cast eq (xs ++ []) ≡ xs
+ init-reverse : init ∘ reverse ≗ reverse ∘ tail
+ last-reverse : last ∘ reverse ≗ head
+ reverse-++ : cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+
+ toList-cast : toList (cast eq xs) ≡ toList xs
+ cast-fromList : cast _ (fromList xs) ≡ fromList ys
+ fromList-map : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
+ fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
  ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:

src/Data/Fin/Properties.agda

@@ -267,7 +267,7 @@ cast-is-id eq (suc k) = cong suc (cast-is-id (ℕₚ.suc-injective eq) k)
 subst-is-cast : (eq : m ≡ n) (k : Fin m) → subst Fin eq k ≡ cast eq k
 subst-is-cast refl k = sym (cast-is-id refl k)
 
-cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (k : Fin m) →
+cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (k : Fin m) →
  cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ zero = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (suc k) =

src/Data/Vec/Properties.agda

@@ -12,9 +12,10 @@ 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ℕ<; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
+import Data.List.Properties as Listₚ
 open import Data.Nat.Base
 open import Data.Nat.Properties
- using (+-assoc; m≤n⇒m≤1+n; ≤-refl; ≤-trans; suc-injective)
+ using (+-assoc; m≤n⇒m≤1+n; ≤-refl; ≤-trans; suc-injective; +-comm; +-suc)
 open import Data.Product.Base as Prod
  using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -387,11 +388,6 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 ------------------------------------------------------------------------
 -- cast
 
-toList-cast : ∀ .(eq : m ≡ n) (xs : Vec A m) → toList (cast eq xs) ≡ toList xs
-toList-cast {n = zero} eq [] = refl
-toList-cast {n = suc _} eq (x ∷ xs) =
- cong (x List.∷_) (toList-cast (cong pred eq) xs)
-
 cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
 cast-is-id eq [] = refl
 cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
@@ -488,6 +484,15 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs)
 ++-injective ws xs eq =
  (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
 
+++-assoc : ∀ .(eq : (m + n) + o ≡ m + (n + o)) (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
+ cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
+++-assoc eq [] ys zs = cast-is-id eq (ys ++ zs)
+++-assoc eq (x ∷ xs) ys zs = cong (x ∷_) (++-assoc (cong pred eq) xs ys zs)
+
+++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
+++-identityʳ eq [] = refl
+++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)
+
 lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
  ∀ i (i<m : toℕ i < m) →
  lookup (xs ++ ys) i ≡ lookup xs (Fin.fromℕ< i<m)
@@ -970,6 +975,20 @@ reverse-injective {xs = xs} {ys} eq = begin
  reverse (reverse ys) ≡⟨ reverse-involutive ys ⟩
  ys ∎
 
+-- init and last of reverse
+
+init-reverse : init ∘ reverse ≗ reverse ∘ tail {A = A} {n = n}
+init-reverse (x ∷ xs) = begin
+ init (reverse (x ∷ xs)) ≡⟨ cong init (reverse-∷ x xs) ⟩
+ init (reverse xs ∷ʳ x) ≡⟨ init-∷ʳ x (reverse xs) ⟩
+ reverse xs ∎
+
+last-reverse : last ∘ reverse ≗ head {A = A} {n = n}
+last-reverse (x ∷ xs) = begin
+ last (reverse (x ∷ xs)) ≡⟨ cong last (reverse-∷ x xs) ⟩
+ last (reverse xs ∷ʳ x) ≡⟨ last-∷ʳ x (reverse xs) ⟩
+ x ∎
+
 -- map and reverse
 
 map-reverse : ∀ (f : A → B) (xs : Vec A n) →
@@ -983,6 +1002,39 @@ map-reverse f (x ∷ xs) = begin
  reverse (f x ∷ map f xs) ≡⟨⟩
  reverse (map f (x ∷ xs)) ∎
 
+-- append and reverse
+
+reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
+ cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
+reverse-++ {m = zero} {n = n} eq [] ys = begin
+ cast _ (reverse ys) ≡˘⟨ cong (cast eq) (++-identityʳ (sym eq) (reverse ys)) ⟩
+ cast _ (cast _ (reverse ys ++ [])) ≡⟨ cast-trans (sym eq) eq (reverse ys ++ []) ⟩
+ cast _ (reverse ys ++ []) ≡⟨ cast-is-id (trans (sym eq) eq) (reverse ys ++ []) ⟩
+ reverse ys ++ [] ≡⟨⟩
+ reverse ys ++ reverse [] ∎
+reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
+ cast eq (reverse (x ∷ xs ++ ys)) ≡⟨ cong (cast eq) (reverse-∷ x (xs ++ ys)) ⟩
+ cast eq (reverse (xs ++ ys) ∷ʳ x) ≡˘⟨ cast-trans eq₂ eq₁ (reverse (xs ++ ys) ∷ʳ x) ⟩
+ (cast eq₁ ∘ cast eq₂) (reverse (xs ++ ys) ∷ʳ x) ≡⟨ cong (cast eq₁) (cast-∷ʳ _ x (reverse (xs ++ ys))) ⟩
+ cast eq₁ ((cast eq₃ (reverse (xs ++ ys))) ∷ʳ x) ≡⟨ cong (cast eq₁) (cong (_∷ʳ x) (reverse-++ _ xs ys)) ⟩
+ cast eq₁ ((reverse ys ++ reverse xs) ∷ʳ x) ≡⟨ ++-∷ʳ _ x (reverse ys) (reverse xs) ⟩
+ reverse ys ++ (reverse xs ∷ʳ x) ≡˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
+ reverse ys ++ (reverse (x ∷ xs)) ∎
+ where
+ eq₁ = sym (+-suc n m)
+ eq₂ = cong suc (+-comm m n)
+ eq₃ = cong pred eq₂
+
+cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
+cast-reverse {n = zero} eq [] = refl
+cast-reverse {n = suc n} eq (x ∷ xs) = begin
+ cast eq (reverse (x ∷ xs)) ≡⟨ cong (cast eq) (reverse-∷ x xs) ⟩
+ cast eq (reverse xs ∷ʳ x) ≡⟨ cast-∷ʳ eq x (reverse xs) ⟩
+ (cast (cong pred eq) (reverse xs)) ∷ʳ x ≡⟨ cong (_∷ʳ x) (cast-reverse (cong pred eq) xs) ⟩
+ (reverse (cast (cong pred eq) xs)) ∷ʳ x ≡˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
+ reverse (x ∷ cast (cong pred eq) xs) ≡⟨⟩
+ reverse (cast eq (x ∷ xs)) ∎
+
 ------------------------------------------------------------------------
 -- _ʳ++_
 
@@ -1161,6 +1213,29 @@ toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
 toList∘fromList List.[] = refl
 toList∘fromList (x List.∷ xs) = cong (x List.∷_) (toList∘fromList xs)
 
+toList-cast : ∀ .(eq : m ≡ n) (xs : Vec A m) → toList (cast eq xs) ≡ toList xs
+toList-cast {n = zero} eq [] = refl
+toList-cast {n = suc _} eq (x ∷ xs) =
+ cong (x List.∷_) (toList-cast (cong pred eq) xs)
+
+cast-fromList : ∀ {xs ys : List A} (eq : xs ≡ ys) →
+ cast (cong List.length eq) (fromList xs) ≡ fromList ys
+cast-fromList {xs = List.[]} {ys = List.[]} eq = refl
+cast-fromList {xs = x List.∷ xs} {ys = y List.∷ ys} eq =
+ let x≡y , xs≡ys = Listₚ.∷-injective eq in begin
+ x ∷ cast (cong (pred ∘ List.length) eq) (fromList xs) ≡⟨ cong (_ ∷_) (cast-fromList xs≡ys) ⟩
+ x ∷ fromList ys ≡⟨ cong (_∷ _) x≡y ⟩
+ y ∷ fromList ys ∎
+
+fromList-map : ∀ (f : A → B) (xs : List A) →
+ cast (Listₚ.length-map f xs) (fromList (List.map f xs)) ≡ map f (fromList xs)
+fromList-map f List.[] = refl
+fromList-map f (x List.∷ xs) = cong (f x ∷_) (fromList-map f xs)
+
+fromList-++ : ∀ (xs : List A) {ys : List A} →
+ cast (Listₚ.length-++ xs) (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
+fromList-++ List.[] {ys} = cast-is-id refl (fromList ys)
+fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES