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

CHANGELOG.md

@@ -432,6 +432,30 @@ 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  ↦  idIsFoldr
+  ```
+  Additionally, `[]≔-++-↑ʳ`, by analogy.
+
 * In `Function.Construct.Composition`:
   ```
   _∘-⟶_   ↦   _⟶-∘_
@@ -465,28 +489,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 +529,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
@@ -829,6 +836,7 @@ Other minor changes
   ```agda
   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 +851,63 @@ 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-++-commute : ∀ {A : Set a} {B : Set b} {m} {n} (f : A → B) xs ys →
+                 map f (xs ++ ys) ≡ map {n = m} f xs ++ map {n = n} f ys
+  foldr-[] : ∀ {A : Set a} (B : ℕ → Set b)
+           (f : ∀ {n} → A → B n → B (suc n)) {e} → foldr B f e [] ≡ e
+  foldr-++ : ∀ {A : Set a} (B : ℕ → Set b)
+           (f : ∀ {n} → A → B n → B (suc n)) {e} →
+           ∀ {m n} {xs} {ys} →
+           foldr B {m + n} f e (xs ++ ys) ≡ foldr (B ∘ (_+ n)) f (foldr B {n} f e ys) xs
+  foldl-universal : ∀ {A : Set a} (B : ℕ → Set b)
+                  (f : ∀ {n} → B n → A → B (suc n)) {e}
+                  (h : ∀ {c} (C : ℕ → Set c) →
+                       (g : ∀ {n} → C n → A → C (suc n)) → C zero →
+                       ∀ {n} → Vec A n → C n) →
+                  (∀ {c} {C} {g : ∀ {n} → C n → A → C (suc n)} e →
+                   h {c} C g e [] ≡ e) →
+                  (∀ {c} {C} {g : ∀ {n} → C n → A → C (suc n)} 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-[] : ∀ {A : Set a} (B : ℕ → Set b)
+           (f : ∀ {n} → B n → A → B (suc n)) {e} → foldl B f e [] ≡ e
+  foldl-fusion : ∀ {A : Set a}
+               {B : ℕ → Set b} {C : ℕ → Set c}
+               (h : ∀ {n} → B n → C n) →
+               {f : ∀ {n} → B n → A → B (suc n)} (d : B zero) →
+               {g : ∀ {n} → C n → A → C (suc n)} (e : C zero) →
+               (h {zero} 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
+  foldr-∷ʳ : ∀ {A : Set a} (B : ℕ → Set b)
+           (f : ∀ {n} → A → B n → B (suc n)) {n} e y ys →
+           foldr B {suc n} f e (ys ∷ʳ y) ≡ foldr (B ∘ suc) {n} f (f y e) ys
+  foldl-∷ʳ : ∀ {A : Set a} (B : ℕ → Set b)
+           (f : ∀ {n} → B n → A → B (suc n)) {n} e y ys →
+           foldl B {suc n} f e (ys ∷ʳ y) ≡ f (foldl B {n} f e ys) y
+  foldr-ʳ++ : ∀ (B : ℕ → Set b) (f : ∀ {n} → A → B n → B (suc n))
+           {m} {n} b (xs : Vec A m) {ys : Vec A n} →
+           foldr B f b (xs ʳ++ ys)
+           ≡
+           foldl (B ∘ (_+ n)) ((λ {m} → flip (f {m + n}))) (foldr B f b 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
+  ∷ʳ-map-commute : (f : A → B) → ∀ {n} x (xs : Vec A n) →
+                 map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x)
+  unfold-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
+  reverse-map-commute : (f : A → B) →
+                      ∀ {n} (xs : Vec A n) → map f (reverse xs) ≡ reverse (map f xs)
+  map-ʳ++ : ∀ {A : Set a} {B : Set b} {m n} (f : A → B) (xs : Vec A m) {ys : Vec A n} →
+          map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
+  reverse-foldr : ∀ {B : ℕ → Set b} {n} (f : ∀ {n} → A → B n → B (suc n)) b →
+                foldr B f b ∘ reverse ≗ foldl B {n} (λ {n} → flip (f {n})) b
+  reverse-foldl : ∀ {B : ℕ → Set b} {n} (f : ∀ {n} → B n → A → B (suc n)) b →
+                foldl B {n} f b ∘ reverse ≗ foldr B (λ {n} → flip (f {n})) b
+  reverse-involutive : ∀ {n} → Involutive {A = Vec A n} _≡_ reverse
+  reverse-reverse : ∀ {n} {xs ys : Vec A n} →
+                  reverse xs ≡ ys → reverse ys ≡ xs
   ```
 
 * 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

@@ -10,6 +10,7 @@ module Data.Vec.Base where
 
 open import Data.Bool.Base
 open import Data.Nat.Base
+open import Data.Nat.Properties
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
 open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
@@ -183,24 +184,29 @@ module DiagonalBind where
 ------------------------------------------------------------------------
 -- Operations for reducing vectors
 
-foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
-        (∀ {n} → A → B n → B (suc n)) →
+module _ {a b} {A : Set a} (B : ℕ → Set b) where
+
+  Opʳ = ∀ {n} → A → B n → B (suc n)
+  Opˡ = ∀ {n} → B n → A → B (suc n)
+
+  foldr : ∀ {m} →
+        Opʳ →
+        B zero →
+        Vec A m → B m
+  foldr _⊕_ n []       = n
+  foldr _⊕_ n (x ∷ xs) = x ⊕ foldr _⊕_ n xs
+
+foldl : ∀ {b} (B : ℕ → Set b) {m} →
+        Opˡ {A = 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
 
 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,14 +286,30 @@ 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)
+{- better ?
+_∷ʳ_ {A = A} xs y = foldr ((Vec A) ∘ suc) (λ x r → x ∷ r) [ y ] xs
+-}
+
+-- 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