Add some _∷ʳ_ properties to Data.Vec.Properties (#2041)

CHANGELOG.md

@@ -864,6 +864,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⁺`
@@ -1253,6 +1256,8 @@ Deprecated names
  zipWith-identityˡ ↦ zipWith-zeroˡ
  zipWith-identityʳ ↦ zipWith-zeroʳ
 
+ ʳ++-++ ↦ ++-ʳ++
+
  take++drop ↦ take++drop≡id
  ```
 
@@ -2658,6 +2663,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

src/Data/List/Properties.agda

@@ -993,11 +993,11 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
 -- Reverse-append of append is reverse-append after reverse-append.
 
-ʳ++-++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
-ʳ++-++ [] = refl
-ʳ++-++ (x ∷ xs) {ys} {zs} = begin
+++-ʳ++ : ∀ (xs {ys zs} : List A) → (xs ++ ys) ʳ++ zs ≡ ys ʳ++ xs ʳ++ zs
+++-ʳ++ [] = refl
+++-ʳ++ (x ∷ xs) {ys} {zs} = begin
  (x ∷ xs ++ ys) ʳ++ zs ≡⟨⟩
- (xs ++ ys) ʳ++ x ∷ zs ≡⟨ ʳ++-++ xs ⟩
+ (xs ++ ys) ʳ++ x ∷ zs ≡⟨ ++-ʳ++ xs ⟩
  ys ʳ++ xs ʳ++ x ∷ zs ≡⟨⟩
  ys ʳ++ (x ∷ xs) ʳ++ zs ∎
 
@@ -1073,7 +1073,7 @@ reverse-++ : (xs ys : List A) →
  reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 reverse-++ xs ys = begin
  reverse (xs ++ ys) ≡⟨⟩
- (xs ++ ys) ʳ++ [] ≡⟨ ʳ++-++ xs ⟩
+ (xs ++ ys) ʳ++ [] ≡⟨ ++-ʳ++ xs ⟩
  ys ʳ++ xs ʳ++ [] ≡⟨⟩
  ys ʳ++ reverse xs ≡⟨ ʳ++-defn ys ⟩
  reverse ys ++ reverse xs ∎
@@ -1213,6 +1213,12 @@ zipWith-identityʳ = zipWith-zeroʳ
 Please use zipWith-zeroʳ instead."
 #-}
 
+ʳ++-++ = ++-ʳ++
+{-# WARNING_ON_USAGE ʳ++-++
+"Warning: ʳ++-++ was deprecated in v2.0.
+Please use ++-ʳ++ instead."
+#-}
+
 take++drop = take++drop≡id
 {-# WARNING_ON_USAGE take++drop
 "Warning: take++drop was deprecated in v2.0.

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

@@ -399,7 +399,7 @@ 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) =
@@ -864,6 +864,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 +891,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