Add more matrix operations

1 files changed, 75 insertions, 93 deletions

diff --git a/Data/Matrix/Transform.agda b/Data/Matrix/Transform.agda
index f536aaf..9f87cbb 100644
--- a/Data/Matrix/Transform.agda
+++ b/Data/Matrix/Transform.agda
@@ -13,15 +13,15 @@ import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 
 open import Data.Nat using (ℕ)
 open import Data.Vec using (Vec; map; replicate; zipWith; _++_)
-open import Data.Vec.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-cong)
+open import Data.Vec.Properties using (map-id; map-const; map-∘; zipWith-replicate; zipWith-replicate₁; map-replicate; map-++; map-cong)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_; module ≡-Reasoning)
 open import Function using (id; _∘_)
 
 open import Data.Matrix.Raw
   using
-    ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapRows
+    ( _ᵀ; _∷ₕ_; []ᵥ; []ₕ; []ᵥ-ᵀ; mapₕ; mapᵥ; ∷ₕⁿ; ∷ᵥⁿ; columns
     ; _ᵀᵀ; []ᵥ-!; ∷ₕ-ᵀ; _∥_; []ᵥ-∥; headₕ; tailₕ; head-∷-tailₕ; ∷ₕ-∥
-    ; _≑_; []ᵥ-≑; ∷ₕ-≑; []ₕ-≑; []ₕ-!; ∷ᵥ-∥
+    ; _≑_; []ᵥ-≑; ∷ₕ-≑; []ₕ-≑; []ₕ-!; ∷ᵥ-∥; columns-≑
     )
 open import Data.Matrix.Core R.setoid
   using
@@ -30,11 +30,12 @@ open import Data.Matrix.Core R.setoid
     )
 open import Data.Matrix.Monoid R.+-monoid using (𝟎; 𝟎ᵀ; _[+]_) renaming (⟨ε⟩∷ᵥ𝟎 to ⟨0⟩∷ᵥ𝟎; ⟨ε⟩∷ₕ𝟎 to ⟨0⟩∷ₕ𝟎)
 open import Data.Matrix.Cast R.setoid using (∥-≑)
-open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++)
+open import Data.Vector.Raw using (⟨⟩; ⟨⟩-++; ⟨⟩-!)
 open import Data.Vector.Core R.setoid using (Vector; Vectorₛ; module ≊; _≊_)
+open import Data.Vector.Endofunctor.Setoid using (zipWith-cong)
 open import Data.Vector.Vec using (zipWith-map; map-zipWith; zipWith-map-map)
 open import Data.Vector.Monoid R.+-monoid using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ) renaming (⟨ε⟩ to ⟨0⟩; ⟨ε⟩-++ to ⟨0⟩-++)
-open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; *-∙ʳ; ∙-distribˡ; ∙-distribʳ)
+open import Data.Vector.Bisemimodule R using (_∙_; ∙-cong; ∙-zeroˡ; ∙-zeroʳ; _⟨_⟩; *-∙ˡ; ∙-distribˡ; ∙-distribʳ)
 
 open Vec
 open ℕ
@@ -51,13 +52,11 @@ opaque
 
   opaque
 
-    -- unfolding Vector
-
     _[_] : Matrix n m → Vector n → Vector m
-    _[_] M V = map (_∙ V) M
+    _[_] M V = mapₕ (_∙ V) M
 
     [_]_ : Vector m → Matrix n m → Vector n
-    [_]_ V M = map (V ∙_) (M ᵀ)
+    [_]_ V = mapᵥ (V ∙_)
 
     -[-]-cong : {x y : Vector n} (A : Matrix n m) → x ≊ y → A [ x ] ≊ A [ y ]
     -[-]-cong {x = x} {y} A ≋V = PW.map⁺ (λ ≋w → ∙-cong ≋w ≋V) {xs = A} ≋.refl
@@ -68,17 +67,12 @@ opaque
     [-]--cong : {x y : Vector m} {A B : Matrix n m} → x ≊ y → A ≋ B → [ x ] A ≊ [ y ] B
     [-]--cong ≋V A≋B = PW.map⁺ (∙-cong ≋V) (ᵀ-cong A≋B)
 
-    opaque
-
-      unfolding _ᵀ []ᵥ
-
-      [-]-[]ᵥ : (V : Vector A) → [ V ] []ᵥ ≡ ⟨⟩
-      [-]-[]ᵥ [] = ≡.refl
-      [-]-[]ᵥ (x ∷ V) = ≡.cong (map ((x ∷ V) ∙_)) []ᵥ-ᵀ
+    [-]-[]ᵥ : (V : Vector A) → [ V ] []ᵥ ≡ ⟨⟩
+    [-]-[]ᵥ V = ⟨⟩-! ([ V ] []ᵥ)
 
     opaque
 
-      unfolding []ᵥ _ᵀ ⟨0⟩ _∙_
+      unfolding []ᵥ ⟨0⟩ _∙_
 
       [-]-[]ₕ : (V : Vector 0) → [ V ] []ₕ ≡ ⟨0⟩ {n}
       [-]-[]ₕ {zero} [] = ≡.refl
@@ -101,7 +95,7 @@ opaque
 
   opaque
 
-    unfolding _ᵀ _∷ₕ_
+    unfolding _∷ₕ_
 
     Iᵀ : I ᵀ ≡ I {n}
     Iᵀ {zero} = ≡.sym ([]ᵥ-! [])
@@ -141,18 +135,18 @@ opaque
       open ≡-Reasoning
 
 opaque
-  unfolding mapRows _ᵀ _[_] [_]_ []ᵥ
-  -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → mapRows (A [_]) (B ᵀ) ≡ (mapRows ([_] B) A) ᵀ
-  -[-]ᵀ [] B = map-const (B ᵀ) []
+  unfolding _[_] [_]_ []ᵥ
+  -[-]ᵀ : (A : Matrix m p) (B : Matrix n m) → ∷ᵥⁿ (mapᵥ (A [_]) B) ≡ ∷ₕⁿ (mapₕ ([_] B) A)
+  -[-]ᵀ [] B = map-const (columns B) []
   -[-]ᵀ (A₀ ∷ A) B = begin
-      map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (B ᵀ) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (B ᵀ) ⟨
-      [ A₀ ] B ∷ₕ (map (A [_]) (B ᵀ))         ≡⟨ ≡.cong ([ A₀ ] B ∷ₕ_) (-[-]ᵀ A B) ⟩
-      [ A₀ ] B ∷ₕ ((map ([_] B) A) ᵀ) ∎
+      map (λ V → A₀ ∙ V ∷ map (_∙ V) A) (columns B) ≡⟨ zipWith-map (A₀ ∙_) (A [_]) _∷_ (columns B) ⟨
+      [ A₀ ] B ∷ₕ (map (A [_]) (columns B))         ≡⟨ ≡.cong ([ A₀ ] B ∷ₕ_) (-[-]ᵀ A B) ⟩
+      [ A₀ ] B ∷ₕ ∷ₕⁿ ((map ([_] B) A))             ∎
     where
       open ≡-Reasoning
 
 opaque
-  unfolding [_]_ _[_] _ᵀ []ₕ _∙_ _∷ₕ_ _⟨_⟩
+  unfolding [_]_ _[_] []ₕ _∙_ _∷ₕ_ _⟨_⟩
 
   []-∙ : (V : Vector m) (M : Matrix n m) (W : Vector n) → [ V ] M ∙ W ≈ V ∙ M [ W ]
   []-∙ {n = n} [] M@[] W = begin
@@ -172,7 +166,7 @@ opaque
       open ≈-Reasoning setoid
 
 opaque
-  unfolding [_]_ I _∙_ ⟨0⟩ mapRows _ᵀ []ᵥ
+  unfolding [_]_ I _∙_ ⟨0⟩ []ᵥ
   [-]I : {n : ℕ} (V : Vector n) → [ V ] I ≊ V
   [-]I {zero} [] = ≊.refl
   [-]I {suc n} (x ∷ V) = begin
@@ -215,8 +209,8 @@ opaque
           open ≈-Reasoning (Vectorₛ n)
 
 opaque
-  unfolding mapRows _[_] _ᵀ _∷ₕ_ I
-  map--[-]-I : (M : Matrix n m) → mapRows (M [_]) I ≋ M ᵀ
+  unfolding _[_] _∷ₕ_ I
+  map--[-]-I : (M : Matrix n m) → ∷ᵥⁿ (mapₕ (M [_]) I) ≋ M ᵀ
   map--[-]-I {n} {m} [] = ≋.reflexive (map-const I [])
   map--[-]-I {n} {suc m} (M₀ ∷ M) = begin
       map ((M₀ ∷ M) [_]) I              ≡⟨⟩
@@ -257,14 +251,13 @@ opaque
       open ≡-Reasoning
 
 opaque
-  unfolding Matrix _[_]
+  unfolding _[_]
   ≑--[-]
       : (V : Vector A)
         (M : Matrix A B)
         (N : Matrix A C)
       → (M ≑ N) [ V ] ≡ M [ V ] ++ N [ V ]
-  ≑--[-] {A} {zero} {C} V [] N = ≡.refl
-  ≑--[-] {A} {suc B} {C} V (M₀ ∷ M) N = ≡.cong (M₀ ∙ V ∷_) (≑--[-] V M N)
+  ≑--[-] V M N = map-++ (_∙ V) M N
 
 opaque
 
@@ -281,54 +274,41 @@ opaque
 
 opaque
 
-  unfolding _⊕_ [_]_
+  unfolding _⊕_
 
-  [++]-≑
-      : (V : Vector B)
-        (W : Vector C)
-        (M : Matrix A B)
-        (N : Matrix A C)
-      → [ V ++ W ] (M ≑ N)
-      ≊ [ V ] M ⊕ [ W ] N
-  [++]-≑ {B} {C} {zero} V W M N
-    rewrite []ᵥ-! M
-    rewrite []ᵥ-! N = begin
-      [ V ++ W ] ([]ᵥ {m = B} ≑ []ᵥ)  ≡⟨ ≡.cong ([ V ++ W ]_) ([]ᵥ-≑ {B}) ⟩
-      [ V ++ W ] []ᵥ                  ≡⟨ [-]-[]ᵥ (V ++ W) ⟩
-      ⟨⟩ ⊕ ⟨⟩                         ≡⟨ ≡.cong₂ _⊕_ ([-]-[]ᵥ V) ([-]-[]ᵥ W) ⟨
-      [ V ] []ᵥ ⊕ [ W ] []ᵥ           ∎
-    where
-      open ≈-Reasoning (Vectorₛ 0)
-  [++]-≑ {B} {C} {suc A} V W M N
-    rewrite ≡.sym (head-∷-tailₕ M)
-    rewrite ≡.sym (head-∷-tailₕ N)
-    using M₀ ← headₕ M
-    using M ← tailₕ M
-    using N₀ ← headₕ N
-    using N ← tailₕ N = begin
-      [ V ++ W ] ((M₀ ∷ₕ M) ≑ (N₀ ∷ₕ N))            ≡⟨ ≡.cong ([ V ++ W ]_) (∷ₕ-≑ M₀ N₀ M N) ⟨
-      [ V ++ W ] ((M₀ ++ N₀) ∷ₕ (M ≑ N))            ≡⟨ ≡.cong (map ((V ++ W) ∙_)) (∷ₕ-ᵀ (M₀ ++ N₀) (M ≑ N)) ⟩
-      (V ++ W) ∙ (M₀ ++ N₀) ∷ ([ V ++ W ] (M ≑ N))  ≈⟨ ∙-++ V M₀ W N₀ PW.∷ [++]-≑ V W M N ⟩
-      (V ∙ M₀ ∷ [ V ] M) ⊕ (W ∙ N₀ ∷ [ W ] N)       ≡⟨ ≡.cong₂ (λ h₁ h₂ → map (V ∙_) h₁ ⊕ map (W ∙_) h₂) (∷ₕ-ᵀ M₀ M) (∷ₕ-ᵀ N₀ N) ⟨
-      ([ V ] (M₀ ∷ₕ M)) ⊕ ([ W ] (N₀ ∷ₕ N))         ∎
-    where
-      open ≈-Reasoning (Vectorₛ (suc A))
+  opaque
+    unfolding [_]_
+    [++]-≑
+        : (V : Vector B)
+          (W : Vector C)
+          (M : Matrix A B)
+          (N : Matrix A C)
+        → [ V ++ W ] (M ≑ N)
+        ≊ [ V ] M ⊕ [ W ] N
+    [++]-≑ {A = A} V W M N = begin
+        map ((V ++ W) ∙_) (columns (M ++ N))                          ≡⟨ ≡.cong (map ((V ++ W) ∙_)) (columns-≑ M N) ⟩
+        map ((V ++ W) ∙_) (zipWith _++_ (columns M) (columns N))      ≡⟨ map-zipWith ((V ++ W) ∙_) _++_ (columns M) (columns N) ⟩
+        zipWith (λ x y → (V ++ W) ∙ (x ++ y)) (columns M) (columns N) ≈⟨ zipWith-cong A R.setoid (λ x y → ∙-++ V x W y) (columns M) (columns N) ⟩
+        zipWith (λ x y → V ∙ x + W ∙ y) (columns M) (columns N)       ≡⟨ zipWith-map-map (V ∙_) (W ∙_) _+_ (columns M) (columns N) ⟩
+        zipWith _+_ (map (V ∙_) (columns M)) (map (W ∙_) (columns N)) ∎
+      where
+        open ≈-Reasoning (Vectorₛ A)
 
-opaque
-  unfolding Matrix _[_] _⊕_
-  ∥-[++]
-      : (V : Vector A)
-        (W : Vector B)
-        (M : Matrix A C)
-        (N : Matrix B C)
-      → (M ∥ N) [ V ++ W ]
-      ≊ M [ V ] ⊕ N [ W ]
-  ∥-[++] {A} {B} {zero} V W [] [] = PW.[]
-  ∥-[++] {A} {B} {suc C} V W (M₀ ∷ M) (N₀ ∷ N) = ∙-++ M₀ V N₀ W PW.∷ ∥-[++] V W M N
+  opaque
+    unfolding _[_]
+    ∥-[++]
+        : (V : Vector A)
+          (W : Vector B)
+          (M : Matrix A C)
+          (N : Matrix B C)
+        → (M ∥ N) [ V ++ W ]
+        ≊ M [ V ] ⊕ N [ W ]
+    ∥-[++] {A} {B} {zero} V W [] [] = PW.[]
+    ∥-[++] {A} {B} {suc C} V W (M₀ ∷ M) (N₀ ∷ N) = ∙-++ M₀ V N₀ W PW.∷ ∥-[++] V W M N
 
 opaque
 
-  unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_ _ᵀ
+  unfolding []ₕ []ᵥ [_]_ ⟨0⟩ _∙_
 
   [⟨⟩]-[]ₕ : [ ⟨⟩ ] ([]ₕ {n = A}) ≡ ⟨0⟩ {A}
   [⟨⟩]-[]ₕ {zero} = ≡.refl
@@ -336,7 +316,7 @@ opaque
 
 opaque
 
-  unfolding ⟨0⟩ []ᵥ [_]_ _ᵀ _∷ₕ_ 𝟎
+  unfolding ⟨0⟩ []ᵥ [_]_ _∷ₕ_ 𝟎
 
   [-]-𝟎 : (V : Vector A) →  [ V ] (𝟎 {B}) ≊ ⟨0⟩
   [-]-𝟎 {A} {zero} V = ≊.reflexive (≡.cong (map (V ∙_)) 𝟎ᵀ)
@@ -349,29 +329,31 @@ opaque
       open ≈-Reasoning (Vectorₛ (suc B))
 
 opaque
-  unfolding Matrix _[_] ⟨0⟩ 𝟎
+  unfolding _[_] ⟨0⟩ 𝟎
   𝟎-[-] : (V : Vector A) → (𝟎 {A} {B}) [ V ] ≊ ⟨0⟩
   𝟎-[-] {A} {zero} V = PW.[]
   𝟎-[-] {A} {suc B} V = ∙-zeroˡ V PW.∷ 𝟎-[-] V
 
 opaque
 
-  unfolding ⟨0⟩ [_]_
+  unfolding ⟨0⟩
 
-  [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩
-  [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩)
-  [⟨0⟩]- {suc A} M
-    rewrite ≡.sym (head-∷-tailₕ M)
-    using M₀ ← headₕ M
-    using M ← tailₕ M = begin
-      [ ⟨0⟩ ] (M₀ ∷ₕ M)     ≡⟨ ≡.cong (map (⟨0⟩ ∙_)) (∷ₕ-ᵀ M₀ M) ⟩
-      ⟨0⟩ ∙ M₀ ∷ [ ⟨0⟩ ] M  ≈⟨ ∙-zeroˡ M₀ PW.∷ [⟨0⟩]- M ⟩
-      0# ∷ ⟨0⟩              ∎
-    where
-      open ≈-Reasoning (Vectorₛ _)
+  opaque
+    unfolding [_]_
+    [⟨0⟩]- : (M : Matrix A B) → [ ⟨0⟩ ] M ≊ ⟨0⟩
+    [⟨0⟩]- {zero} M rewrite []ᵥ-! M = ≊.reflexive ([-]-[]ᵥ ⟨0⟩)
+    [⟨0⟩]- {suc A} M
+      rewrite ≡.sym (head-∷-tailₕ M)
+      using M₀ ← headₕ M
+      using M ← tailₕ M = begin
+        [ ⟨0⟩ ] (M₀ ∷ₕ M)     ≡⟨ ≡.cong (map (⟨0⟩ ∙_)) (∷ₕ-ᵀ M₀ M) ⟩
+        ⟨0⟩ ∙ M₀ ∷ [ ⟨0⟩ ] M  ≈⟨ ∙-zeroˡ M₀ PW.∷ [⟨0⟩]- M ⟩
+        0# ∷ ⟨0⟩              ∎
+      where
+        open ≈-Reasoning (Vectorₛ _)
 
-opaque
-  unfolding _[_] ⟨0⟩
-  -[⟨0⟩] : (M : Matrix A B) → M [ ⟨0⟩ ] ≊ ⟨0⟩
-  -[⟨0⟩] {A} {B} [] = PW.[]
-  -[⟨0⟩] {A} {B} (M₀ ∷ M) = ∙-zeroʳ M₀ PW.∷ -[⟨0⟩] M
+  opaque
+    unfolding _[_]
+    -[⟨0⟩] : (M : Matrix A B) → M [ ⟨0⟩ ] ≊ ⟨0⟩
+    -[⟨0⟩] {A} {B} [] = PW.[]
+    -[⟨0⟩] {A} {B} (M₀ ∷ M) = ∙-zeroʳ M₀ PW.∷ -[⟨0⟩] M