Reorganize matrix code

3 files changed, 72 insertions, 20 deletions

diff --git a/Data/Vector/Bisemimodule.agda b/Data/Vector/Bisemimodule.agda
index d895459..e38536a 100644
--- a/Data/Vector/Bisemimodule.agda
+++ b/Data/Vector/Bisemimodule.agda
@@ -136,19 +136,19 @@ opaque
 
   unfolding _∙_ ⟨ε⟩
 
-  ∙-identityˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0#
-  ∙-identityˡ [] = refl
-  ∙-identityˡ (x ∷ V) = begin
+  ∙-zeroˡ : (V : Vector n) → ⟨ε⟩ ∙ V ≈ 0#
+  ∙-zeroˡ [] = refl
+  ∙-zeroˡ (x ∷ V) = begin
       0# * x + ⟨ε⟩ ∙ V  ≈⟨ +-congʳ (zeroˡ x) ⟩
-      0# + ⟨ε⟩ ∙ V      ≈⟨ +-congˡ (∙-identityˡ V) ⟩
+      0# + ⟨ε⟩ ∙ V      ≈⟨ +-congˡ (∙-zeroˡ V) ⟩
       0# + 0#           ≈⟨ +-identityˡ 0# ⟩
       0#                ∎
 
-  ∙-identityʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0#
-  ∙-identityʳ [] = refl
-  ∙-identityʳ (x ∷ V) = begin
+  ∙-zeroʳ : (V : Vector n) → V ∙ ⟨ε⟩ ≈ 0#
+  ∙-zeroʳ [] = refl
+  ∙-zeroʳ (x ∷ V) = begin
       x * 0# + V ∙ ⟨ε⟩  ≈⟨ +-congʳ (zeroʳ x) ⟩
-      0# + V ∙ ⟨ε⟩      ≈⟨ +-congˡ (∙-identityʳ V) ⟩
+      0# + V ∙ ⟨ε⟩      ≈⟨ +-congˡ (∙-zeroʳ V) ⟩
       0# + 0#           ≈⟨ +-identityˡ 0# ⟩
       0#                ∎
 
diff --git a/Data/Vector/Core.agda b/Data/Vector/Core.agda
index 974f672..a430f12 100644
--- a/Data/Vector/Core.agda
+++ b/Data/Vector/Core.agda
@@ -13,18 +13,18 @@ open import Categories.Category.Instance.Nat using (Natop)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; _+_)
 open import Data.Setoid using (∣_∣)
-open import Data.Vec using (Vec; lookup; tabulate)
+open import Data.Vec as Vec using (Vec; lookup; tabulate)
 open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate; tabulate-cong)
 open import Data.Vec.Relation.Binary.Equality.Setoid S using (_≋_; ≋-isEquivalence)
 open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_; _∘_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open Func
 open Setoid S
-open Vec
 open Fin
+open Vec.Vec
 
 private
   variable
@@ -44,6 +44,18 @@ opaque
   ≊-isEquiv : IsEquivalence (_≊_ {n})
   ≊-isEquiv {n} = ≋-isEquivalence n
 
+  _++_ : Vector A → Vector B → Vector (A + B)
+  _++_ = Vec._++_
+
+  ⟨⟩ : Vector 0
+  ⟨⟩ = []
+
+  ⟨⟩-! : (V : Vector 0) → V ≡ ⟨⟩
+  ⟨⟩-! [] = ≡.refl
+
+  ⟨⟩-++ : (V : Vector A) → ⟨⟩ ++ V ≡ V
+  ⟨⟩-++ V = ≡.refl
+
 -- A setoid of vectors for every natural number
 Vectorₛ : ℕ → Setoid c (c ⊔ ℓ)
 Vectorₛ n = record
diff --git a/Data/Vector/Vec.agda b/Data/Vector/Vec.agda
index ae87737..868571a 100644
--- a/Data/Vector/Vec.agda
+++ b/Data/Vector/Vec.agda
@@ -3,8 +3,8 @@
 module Data.Vector.Vec where
 
 open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec; tabulate; zipWith; replicate)
+open import Data.Nat using (ℕ; _+_)
+open import Data.Vec using (Vec; tabulate; zipWith; replicate; map; _++_)
 open import Function using (_∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
@@ -13,10 +13,18 @@ open Vec
 open ℕ
 open Fin
 
+private
+  variable
+    a b c d e : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+    n : ℕ
+
 zipWith-tabulate
-    : {a : Level}
-      {A : Set a}
-      {n : ℕ}
+    : {n : ℕ}
       (_⊕_ : A → A → A)
       (f g : Fin n → A)
     → zipWith _⊕_ (tabulate f) (tabulate g) ≡ tabulate (λ i → f i ⊕ g i)
@@ -24,10 +32,42 @@ zipWith-tabulate {n = zero} _⊕_ f g = ≡.refl
 zipWith-tabulate {n = suc n} _⊕_ f g = ≡.cong (f zero ⊕ g zero ∷_) (zipWith-tabulate _⊕_ (f ∘ suc) (g ∘ suc))
 
 replicate-tabulate
-    : {a : Level}
-      {A : Set a}
-      {n : ℕ}
+    : {n : ℕ}
       (x : A)
     → replicate n x ≡ tabulate (λ _ → x)
 replicate-tabulate {n = zero} x = ≡.refl
 replicate-tabulate {n = suc n} x = ≡.cong (x ∷_) (replicate-tabulate x)
+
+zipWith-map
+    : {n : ℕ}
+      (f : A → B)
+      (g : A → C)
+      (_⊕_ : B → C → D)
+      (v : Vec A n)
+    → zipWith _⊕_ (map f v) (map g v) ≡ map (λ x → f x ⊕ g x) v
+zipWith-map f g _⊕_ [] = ≡.refl
+zipWith-map f g _⊕_ (x ∷ v) = ≡.cong (f x ⊕ g x ∷_) (zipWith-map f g _⊕_ v)
+
+replicate-++ : (n m : ℕ) (x : A) → replicate n x ++ replicate m x ≡ replicate (n + m) x
+replicate-++ zero _ x = ≡.refl
+replicate-++ (suc n) m x = ≡.cong (x ∷_) (replicate-++ n m x)
+
+map-zipWith
+    : (f : C → D)
+      (_⊕_ : A → B → C)
+      {n : ℕ}
+      (v : Vec A n)
+      (w : Vec B n)
+    → map f (zipWith _⊕_ v w) ≡ zipWith (λ x y → f (x ⊕ y)) v w
+map-zipWith f _⊕_ [] [] = ≡.refl
+map-zipWith f _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f (x ⊕ y) ∷_) (map-zipWith f _⊕_ v w)
+
+zipWith-map-map
+    : (f : A → C)
+      (g : B → D)
+      (_⊕_ : C → D → E)
+      (v : Vec A n)
+      (w : Vec B n)
+    → zipWith (λ x y → f x ⊕ g y) v w ≡ zipWith _⊕_ (map f v) (map g w)
+zipWith-map-map f g _⊕_ [] [] = ≡.refl
+zipWith-map-map f g _⊕_ (x ∷ v) (y ∷ w) = ≡.cong (f x ⊕ g y ∷_) (zipWith-map-map f g _⊕_ v w)