Previous PRs content -- will be gone after rebase

Author: shhyou

CHANGELOG.md

@@ -858,6 +858,9 @@ Non-backwards compatible changes
 
 * In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`.
 
+* In `Data.Vec.Base`: the definitions `init` and `last` have been changed from the `initLast`
+  view-derived implementation to direct recursive definitions.
+
 * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions:
   * `cycle`
   * `interleave⁺`
@@ -2632,6 +2635,12 @@ Other minor changes
   ∷ʳ-injectiveˡ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
   ∷ʳ-injectiveʳ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
 
+  unfold-∷ʳ : cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
+  init-∷ʳ   : init (xs ∷ʳ x) ≡ xs
+  last-∷ʳ   : last (xs ∷ʳ x) ≡ x
+  cast-∷ʳ   : cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
+  ++-∷ʳ     : cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+
   reverse-∷          : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
   reverse-involutive : Involutive _≡_ reverse
   reverse-reverse    : reverse xs ≡ ys → reverse ys ≡ xs
@@ -2642,16 +2651,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

@@ -262,7 +262,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/Base.agda

@@ -345,12 +345,12 @@ initLast {n = suc n} (x ∷ xs) with initLast xs
 ... | (ys , y , refl) = (x ∷ ys , y , refl)
 
 init : Vec A (1 + n) → Vec A n
-init xs with initLast xs
-... | (ys , y , refl) = ys
+init {n = zero}  (x ∷ _)  = []
+init {n = suc n} (x ∷ xs) = x ∷ init xs
 
 last : Vec A (1 + n) → A
-last xs with initLast xs
-... | (ys , y , refl) = y
+last {n = zero}  (x ∷ _)  = x
+last {n = suc n} (_ ∷ xs) = last xs
 
 ------------------------------------------------------------------------
 -- Other operations

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,19 +388,14 @@ 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)
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
 
-cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
+cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
 cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ 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)
@@ -864,6 +869,12 @@ map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
+-- snoc is snoc
+
+unfold-∷ʳ : ∀ .(eq : suc n ≡ n + 1) x (xs : Vec A n) → cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
+unfold-∷ʳ eq x []       = refl
+unfold-∷ʳ eq x (y ∷ xs) = cong (y ∷_) (unfold-∷ʳ (cong pred eq) x xs)
+
 ∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 ∷ʳ-injective []       []        refl = (refl , refl)
 ∷ʳ-injective (x ∷ xs) (y  ∷ ys) eq   with ∷-injective eq
@@ -885,12 +896,37 @@ foldr-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} y (ys : Vec A n) →
 foldr-∷ʳ B f y []       = refl
 foldr-∷ʳ B f y (x ∷ xs) = cong (f x) (foldr-∷ʳ B f y xs)
 
+-- init, last and _∷ʳ_
+
+init-∷ʳ : ∀ x (xs : Vec A n) → init (xs ∷ʳ x) ≡ xs
+init-∷ʳ x []       = refl
+init-∷ʳ x (y ∷ xs) = cong (y ∷_) (init-∷ʳ x xs)
+
+last-∷ʳ : ∀ x (xs : Vec A n) → last (xs ∷ʳ x) ≡ x
+last-∷ʳ x []       = refl
+last-∷ʳ x (y ∷ xs) = last-∷ʳ x xs
+
 -- map and _∷ʳ_
 
 map-∷ʳ : ∀ (f : A → B) x (xs : Vec A n) → map f (xs ∷ʳ x) ≡ map f xs ∷ʳ f x
 map-∷ʳ f x []       = refl
 map-∷ʳ f x (y ∷ xs) = cong (f y ∷_) (map-∷ʳ f x xs)
 
+-- cast and _∷ʳ_
+
+cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) →
+          cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
+cast-∷ʳ {m = zero}  eq x []       = refl
+cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq) x xs)
+
+-- _++_ and _∷ʳ_
+
+++-∷ʳ : ∀ .(eq : suc (m + n) ≡ m + suc n) z (xs : Vec A m) (ys : Vec A n) →
+        cast eq ((xs ++ ys) ∷ʳ z) ≡ xs ++ (ys ∷ʳ z)
+++-∷ʳ {m = zero}  eq z []       []       = refl
+++-∷ʳ {m = zero}  eq z []       (y ∷ ys) = cong (y ∷_) (++-∷ʳ refl z [] ys)
+++-∷ʳ {m = suc m} eq z (x ∷ xs) ys       = cong (x ∷_) (++-∷ʳ (cong pred eq) z xs ys)
+
 ------------------------------------------------------------------------
 -- reverse
 
@@ -939,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) →
@@ -952,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))              ∎
+
 ------------------------------------------------------------------------
 -- _ʳ++_
 
@@ -1130,6 +1213,31 @@ 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 = begin
+  x ∷ cast (cong (pred ∘ List.length) eq) (fromList xs) ≡⟨ cong (_ ∷_) (cast-fromList xs-equals-ys) ⟩
+  x ∷ fromList ys                                       ≡⟨ cong (_∷ _) x-equals-y ⟩
+  y ∷ fromList ys                                       ∎
+  where
+  x-equals-y = proj₁ (Listₚ.∷-injective eq)
+  xs-equals-ys = proj₂ (Listₚ.∷-injective eq)
+
+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