Port reverse lemmas to Data.Vec (fixes #942)

CHANGELOG.md

@@ -432,6 +432,31 @@ Deprecated names
   zipWith-identityʳ  ↦  zipWith-zeroʳ
   ```
 
+* In `Data.Fin.Base`:
+two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the position of the Fin m argument.
+  ```
+  inject+   ↦   flip _↑ˡ_
+  raise     ↦   _↑ʳ_
+  ```
+
+* In `Data.Fin.Properties`:
+  ```
+  toℕ-raise       ↦ toℕ-↑ʳ
+  toℕ-inject+ n i ↦ sym (toℕ-↑ˡ i n)
+  splitAt-inject+ m n i ↦ splitAt-↑ˡ m i n
+  splitAt-raise ↦ splitAt-↑ʳ
+  Fin0↔⊥        ↦ 0↔⊥
+  ```
+
+* In `Data.Vec.Properties`:
+
+  ```
+  []≔-++-inject+       ↦ []≔-++-↑ˡ
+  idIsFold  ↦  id-is-foldr
+  sum-++-commute ↦ sum-++
+  ```
+  Additionally, `[]≔-++-↑ʳ`, by analogy.
+
 * In `Function.Construct.Composition`:
   ```
   _∘-⟶_   ↦   _⟶-∘_
@@ -465,28 +490,6 @@ Deprecated names
   sym-↔   ↦   ↔-sym
   ```
 
-* In `Data.Fin.Base`:
-two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the position of the Fin m argument.
-  ```
-  inject+   ↦   flip _↑ˡ_
-  raise     ↦   _↑ʳ_
-  ```
-
-* In `Data.Fin.Properties`:
-  ```
-  toℕ-raise       ↦ toℕ-↑ʳ
-  toℕ-inject+ n i ↦ sym (toℕ-↑ˡ i n)
-  splitAt-inject+ m n i ↦ splitAt-↑ˡ m i n
-  splitAt-raise ↦ splitAt-↑ʳ
-  Fin0↔⊥        ↦ 0↔⊥
-  ```
-
-* In `Data.Vec.Properties`:
-  ```
-  []≔-++-inject+       ↦ []≔-++-↑ˡ
-  ```
-  Additionally, `[]≔-++-↑ʳ`, by analogy.
-
 * In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`:
   ```
   toForeign   ↦ Foreign.Haskell.Coerce.coerce
@@ -527,6 +530,11 @@ New modules
   Data.Vec.Reflection
   ```
 
+* A small library for heterogenous equational reasoning on vectors:
+  ```
+  Data.Vec.Properties.Heterogeneous
+  ```
+
 * Show module for unnormalised rationals:
   ```
   Data.Rational.Unnormalised.Show
@@ -827,8 +835,15 @@ Other minor changes
 
 * Added new definitions in `Data.Vec.Base`:
   ```agda
+  FoldrOp A B = ∀ {n} → A → B n → B (suc n)
+  FoldlOp A B = ∀ {n} → B n → A → B (suc n)
+
+  foldr′ : ∀ {n} → (A → B → B) → B → Vec A n → B
+  foldl′ : ∀ {n} → (B → A → B) → B → Vec A n → B
+
   diagonal : ∀ {n} → Vec (Vec A n) n → Vec A n
   DiagonalBind._>>=_ : ∀ {n} → Vec A n → (A → Vec B n) → Vec B n
+  _ʳ++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
   ```
 
 * Added new instance in `Data.Vec.Categorical`:
@@ -843,6 +858,56 @@ Other minor changes
   ⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) → (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs)
   transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs
   []≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i → (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y)
+  map-++ : ∀ (f : A → B) {m} {n} (xs : Vec A m) (ys : Vec A n) →
+           map f (xs ++ ys) ≡ map f xs ++ map f ys
+  foldl-universal : ∀ {A : Set a} (B : ℕ → Set b)
+                    (f : FoldlOp A B) {e}
+                    (h : ∀ {c} (C : ℕ → Set c) (g : FoldlOp A C) (e : C zero) →
+                         ∀ {n} → Vec A n → C n) →
+                    (∀ {c} {C} {g : FoldlOp A C} e → h {c} C g e [] ≡ e) →
+                    (∀ {c} {C} {g : FoldlOp A C} e → ∀ {n} x →
+                     (h {c} C g e {suc n}) ∘ (x ∷_) ≗ h (C ∘ suc) (λ {n} → g {suc n}) (g e x)) →
+                    ∀ {n} → h B f e ≗ foldl B {n} f e
+  foldl-fusion : ∀ {A : Set a} {B : ℕ → Set b} {C : ℕ → Set c}
+                 (h : ∀ {n} → B n → C n) →
+                 {f : FoldlOp A B} {d : B zero} →
+                 {g : FoldlOp A C} {e : C zero} →
+                 (h d ≡ e) →
+                 (∀ {n} b x → h (f {n} b x) ≡ g (h b) x) →
+                 ∀ {n} → h ∘ foldl B {n} f d ≗ foldl C g e
+  reverse-∷  : ∀ {n} (x : A) xs → reverse (x ∷ xs) ≡ reverse {n = n} xs ∷ʳ x
+  unfold-ʳ++ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → xs ʳ++ ys ≡ reverse xs ++ ys
+  foldl-∷ʳ : ∀ {A : Set a} (B : ℕ → Set b) (f : FoldrOp A B) {e} →
+             ∀ {n} y (ys : Vec A n) → foldl B f e (ys ∷ʳ y) ≡ f (foldl B f e ys) y
+  foldl-[] : ∀ {A : Set a} (B : ℕ → Set b) (f : FoldlOp A B) {e} → foldl B f e [] ≡ e
+  foldl-reverse : ∀ {B : ℕ → Set b} {n} (f : FoldlOp A B) e →
+                foldl B {n} f e ∘ reverse ≗ foldr B (λ {n} → flip (f {n})) e
+  foldr-[] : ∀ {A : Set a} (B : ℕ → Set b) (f : FoldrOp A B) {e} → foldr B f e [] ≡ e
+  foldr-++ : ∀ {A : Set a} (B : ℕ → Set b) (f : FoldrOp A B) {e} →
+             ∀ {m n} (xs : Vec A m) {ys : Vec A n} →
+             foldr B f e (xs ++ ys) ≡ foldr (B ∘ (_+ n)) f (foldr B f e ys) xs
+  foldr-∷ʳ : ∀ {A : Set a} (B : ℕ → Set b) (f : FoldrOp A B) {e} →
+             ∀ {n} y (ys : Vec A n) → foldr B f e (ys ∷ʳ y) ≡ foldr (B ∘ suc) f (f y e) ys
+  foldr-ʳ++ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} →
+              ∀ {m} {n} b (xs : Vec A m) {ys : Vec A n} →
+              foldr B f e (xs ʳ++ ys)
+              ≡
+              foldl (B ∘ (_+ n)) ((λ {m} → flip (f {m + n}))) (foldr B f e ys) xs
+  foldr-reverse : ∀ {B : ℕ → Set b} (f : FoldrOp A B) {e} {n} →
+                foldr B {n} f e ∘ reverse ≗ foldl B (λ {n} → flip (f {n})) e
+  ++-is-foldr : ∀ {m n} (xs : Vec A m) {ys : Vec A n} →
+                xs ++ ys ≡ foldr ((Vec A) ∘ (_+ n)) _∷_ ys xs
+  ∷ʳ-injective : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
+  ∷ʳ-injectiveˡ : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
+  ∷ʳ-injectiveʳ : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
+  map-is-foldr : (f : A → B) → ∀ {n} → map {n = n} f ≗ foldr (Vec B) (λ x ys → f x ∷ ys) []
+  map-∷ʳ : (f : A → B) → ∀ {n} x (xs : Vec A n) → map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x)
+  map-reverse : (f : A → B) → ∀ {n} (xs : Vec A n) → map f (reverse xs) ≡ reverse (map f xs)
+  map-ʳ++ : ∀ (f : A → B) {m n} (xs : Vec A m) {ys : Vec A n} →
+            map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
+  reverse-involutive : ∀ {n} → Involutive {A = Vec A n} _≡_ reverse
+  reverse-reverse : ∀ {n} {xs ys : Vec A n} → reverse xs ≡ ys → reverse ys ≡ xs
+  reverse-injective : ∀ {n} {xs ys : Vec A n} → reverse xs ≡ reverse ys → xs ≡ ys
   ```
 
 * Added new proofs in `Function.Construct.Symmetry`:

README/Tactic/Rewrite.agda

@@ -13,7 +13,7 @@ open import Tactic.Rewrite using (cong!)
 -- Usage
 ----------------------------------------------------------------------
 
--- When performing large equational reasoning proofs, it's quite 
+-- When performing large equational reasoning proofs, it's quite
 -- common to have to construct sophisticated lambdas to pass
 -- into 'cong'. This can be extremely tedious, and can bog down
 -- large proofs in piles of boilerplate. The 'cong!' tactic
@@ -79,13 +79,13 @@ module LiteralTests
 
   test₁ : 40 + 2 ≡ 42
   test₁ = cong! refl
-  
+
   test₂ : 48 ≡ 42 → 42 ≡ 48
   test₂ eq = cong! (sym eq)
-  
-  test₃ : (f : ℕ → ℕ) → f 48 ≡ f 42 
+
+  test₃ : (f : ℕ → ℕ) → f 48 ≡ f 42
   test₃ f = cong! assumption
-  
+
   test₄ : (f : ℕ → ℕ → ℕ) → f 48 48 ≡ f 42 42
   test₄ f = cong! assumption
 
@@ -111,7 +111,7 @@ module HigherOrderTests
 
   test₂ : f ≡ g → ∀ n → f (f (f n)) ≡ g (g (g n))
   test₂ eq n = cong! eq
- 
+
 module EquationalReasoningTests where
 
   test₁ : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)

src/Data/Vec/Base.agda

@@ -183,24 +183,41 @@ module DiagonalBind where
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
 
-foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
-        (∀ {n} → A → B n → B (suc n)) →
+-- Dependent folds
+
+module _ (A : Set a) (B : ℕ → Set b) where
+
+  FoldrOp = ∀ {n} → A → B n → B (suc n)
+  FoldlOp = ∀ {n} → B n → A → B (suc n)
+
+foldr : ∀ (B : ℕ → Set b) {m} →
+        FoldrOp A B →
+        B zero →
+        Vec A m → B m
+foldr B _⊕_ n []       = n
+foldr B _⊕_ n (x ∷ xs) = x ⊕ foldr B _⊕_ n xs
+
+foldl : ∀ (B : ℕ → Set b) {m} →
+        FoldlOp A B →
         B zero →
         Vec A m → B m
-foldr b _⊕_ n []       = n
-foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs
+foldl B _⊕_ n []       = n
+foldl B _⊕_ n (x ∷ xs) = foldl (B ∘ suc) _⊕_ (n ⊕ x) xs
+
+-- Non-dependent folds
+
+foldr′ : ∀ {n} → (A → B → B) → B → Vec A n → B
+foldr′ _⊕_ = foldr _ λ {n} → _⊕_
+
+foldl′ : ∀ {n} → (B → A → B) → B → Vec A n → B
+foldl′ _⊕_ = foldl _ λ {n} → _⊕_
+
+-- Non-empty folds
 
 foldr₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
 foldr₁ _⊕_ (x ∷ [])     = x
 foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)
 
-foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
-        (∀ {n} → B n → A → B (suc n)) →
-        B zero →
-        Vec A m → B m
-foldl b _⊕_ n []       = n
-foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs
-
 foldl₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
 foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
 
@@ -280,15 +297,28 @@ fromList (List._∷_ x xs) = x ∷ fromList xs
 ------------------------------------------------------------------------
 -- Operations for reversing vectors
 
-reverse : ∀ {n} → Vec A n → Vec A n
-reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
+-- snoc
 
 infixl 5 _∷ʳ_
 
-_∷ʳ_ : ∀ {n} → Vec A n → A → Vec A (1 + n)
+_∷ʳ_ : ∀ {n} → Vec A n → A → Vec A (suc n)
 []       ∷ʳ y = [ y ]
 (x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)
 
+-- vanilla reverse
+
+reverse : ∀ {n} → Vec A n → Vec A n
+reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
+
+-- reverse-append
+
+infix 5 _ʳ++_
+
+_ʳ++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
+_ʳ++_ {A = A} {n = n} xs ys = foldl ((Vec A) ∘ (_+ n)) (λ rev x → x ∷ rev) ys xs
+
+-- init and last
+
 initLast : ∀ {n} (xs : Vec A (1 + n)) →
            ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
 initLast {n = zero}  (x ∷ [])         = ([] , x , refl)