Add more matrix operations

1 files changed, 204 insertions, 65 deletions

diff --git a/Data/Matrix/Raw.agda b/Data/Matrix/Raw.agda
index ecd5e9f..73a4b8c 100644
--- a/Data/Matrix/Raw.agda
+++ b/Data/Matrix/Raw.agda
@@ -5,14 +5,14 @@ open import Relation.Binary using (Rel; REL)
 
 module Data.Matrix.Raw where
 
-open import Data.Nat using (ℕ; _+_)
-open import Data.Vec as Vec using (Vec; zipWith; head; tail; replicate)
+open import Data.Nat using (ℕ; _+_; _*_)
+open import Data.Vec as Vec using (Vec; zipWith; head; tail; replicate; concat; foldr)
 open import Data.Vec using (_++_)
-open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-replicate)
+open import Data.Vec.Properties using (map-cong; map-id; map-++; map-∘; map-const; map-replicate; zipWith-map₂; zipWith-++; zipWith-replicate)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW-Vec using (Pointwise; map⁺)
 open import Data.Vector.Raw as Vector using (R-zipWith)
 open import Data.Vector.Vec using (zipWith-map; replicate-++; map-zipWith; zipWith-map-map; zipWith-cong)
-open import Function using (id; _∘_)
+open import Function using (id; _∘_; const)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
 
 open ℕ
@@ -20,61 +20,138 @@ open Vec.Vec
 
 private
   variable
-    n m p : ℕ
+    n m p q : ℕ
     a ℓ ℓ₁ ℓ₂ : Level
     A B C D E F : Set a
 
 open ≡-Reasoning
 
-module FixedBase (A : Set a) where
-
-  opaque
-
-    -- Matrices
-    Matrix : Rel ℕ a
-    Matrix n m = Vec (Vec A n) m
-
-open FixedBase public
-
 opaque
 
-  unfolding Matrix
+  -- Matrices
+  Matrix : Set a → Rel ℕ a
+  Matrix A n m = Vec (Vec A n) m
 
+  -- Pointwise relation on matrices
   PW : {a b : Level} {A : Set a} {B : Set b} (R : REL A B ℓ) → REL (Matrix A n m) (Matrix B n m) (a ⊔ b ⊔ ℓ)
   PW R = Pointwise (Pointwise R)
 
-  mapRows : (Vec A n → Vec A m) → Matrix A n p → Matrix A m p
-  mapRows = Vec.map
-
+  -- Apply a function to every element
   map : (A → B) → Matrix A n m → Matrix B n m
   map f = Vec.map (Vec.map f)
 
+  -- Lift a square in the double category of sets and relations to matrices
+  map₂
+      : {R : REL A B ℓ}
+        {S : REL C D ℓ}
+        {f : A → C}
+        {g : B → D}
+      → (∀ {x y} → R x y → S (f x) (g y))
+      → {M₁ : Matrix A m n}
+        {M₂ : Matrix B m n}
+      → PW R M₁ M₂
+      → PW S (map f M₁) (map g M₂)
+  map₂ R⇒S = map⁺ (map⁺ R⇒S)
+
+  -- Juxtapose matrices horizontally
   _∥_ : Matrix A n p → Matrix A m p → Matrix A (n + m) p
   _∥_ M N = zipWith _++_ M N
 
   infixr 7 _∥_
 
+  -- Juxtapose matrices verically
   _≑_ : Matrix A n m → Matrix A n p → Matrix A n (m + p)
-  _≑_ M N = M ++ N
+  _≑_ = _++_
 
   infixr 6 _≑_
 
+  -- Append a column on the left
+  _∷ₕ_ : Vec A m → Matrix A n m → Matrix A (suc n) m
+  _∷ₕ_ = zipWith _∷_
+
+  infixr 5 _∷ₕ_
+
+  -- Append a row to the top
   _∷ᵥ_ : Vec A n → Matrix A n m → Matrix A n (suc m)
   _∷ᵥ_ V M = V Vec.∷ M
 
   infixr 5 _∷ᵥ_
 
-  _∷ₕ_ : Vec A m → Matrix A n m → Matrix A (suc n) m
-  _∷ₕ_ V M = zipWith _∷_ V M
+  -- A matrix of width 0
+  []ᵥ : Matrix A 0 m
+  []ᵥ = replicate _ []
 
-  infixr 5 _∷ₕ_
+  -- A matrix of height 0
+  []ₕ : Matrix A n 0
+  []ₕ = []
 
+  -- The first column of a matrix
   headₕ : Matrix A (suc n) m → Vec A m
   headₕ = Vec.map Vec.head
 
+  -- The first row of a matrix
+  headᵥ : Matrix A n (suc m) → Vec A n
+  headᵥ = head
+
+  -- All but the first column of a matrix
   tailₕ : Matrix A (suc n) m → Matrix A n m
   tailₕ = Vec.map Vec.tail
 
+  -- All but the first row of a matrix
+  tailᵥ : Matrix A n (suc m) → Matrix A n m
+  tailᵥ = tail
+
+  -- View a matrix as a vector of rows
+  rows : Matrix A n m → Vec (Vec A n) m
+  rows = id
+
+  -- View a matrix as a vector of columns
+  columns : Matrix A n m → Vec (Vec A m) n
+  columns {A = A} {n} = foldr (λ i → Vec (Vec A i) n) _∷ₕ_ []ᵥ
+
+  -- Intepret a vector of rows as a matrix
+  ∷ᵥⁿ : Vec (Vec A n) m → Matrix A n m
+  ∷ᵥⁿ = id
+
+  -- Interpret a vector of columns as a matrix
+  ∷ₕⁿ : Vec (Vec A m) n → Matrix A n m
+  ∷ₕⁿ = columns
+
+-- Transpose
+_ᵀ : Matrix A n m → Matrix A m n
+_ᵀ = ∷ᵥⁿ ∘ columns
+
+infix 10 _ᵀ
+
+-- Apply a function to each row
+mapₕ : (Vec A n → B) → Matrix A n m → Vec B m
+mapₕ f M = Vec.map f (rows M)
+
+-- Apply a function to each column
+mapᵥ : (Vec A m → B) → Matrix A n m → Vec B n
+mapᵥ f M = Vec.map f (columns M)
+
+-- Horizontally flatten a vector of same-height matrices
+∥ⁿ : Vec (Matrix A n m) p → Matrix A (p * n) m
+∥ⁿ [] = []ᵥ
+∥ⁿ (M ∷ Ms) = M ∥ ∥ⁿ Ms
+
+-- Vertically flatten a vector of same-width matrices
+≑ⁿ : Vec (Matrix A n m) p → Matrix A n (p * m)
+≑ⁿ [] = []ₕ
+≑ⁿ (M ∷ Ms) = M ≑ ≑ⁿ Ms
+
+-- Flatten a matrix of matrices
+join : Matrix (Matrix A p q) n m → Matrix A (n * p) (m * q)
+join M = ≑ⁿ (mapₕ ∥ⁿ M)
+
+opaque
+
+  unfolding Matrix
+
+  head-∷-tailᵥ : (M : Matrix A n (suc m)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
+  head-∷-tailᵥ (_ ∷ _) = ≡.refl
+
   head-∷-tailₕ : (M : Matrix A (suc n) m) → headₕ M ∷ₕ tailₕ M ≡ M
   head-∷-tailₕ M = begin
       zipWith _∷_ (Vec.map Vec.head M) (Vec.map Vec.tail M) ≡⟨ zipWith-map head tail _∷_ M ⟩
@@ -82,9 +159,6 @@ opaque
       Vec.map id M                                          ≡⟨ map-id M ⟩
       M ∎
 
-  []ᵥ : Matrix A 0 m
-  []ᵥ = replicate _ []
-
   []ᵥ-! : (E : Matrix A 0 m) → E ≡ []ᵥ
   []ᵥ-! [] = ≡.refl
   []ᵥ-! ([] ∷ E) = ≡.cong ([] ∷_) ([]ᵥ-! E)
@@ -107,18 +181,6 @@ opaque
   ∷ᵥ-∥ : (V : Vec A n) (W : Vec A m) (M : Matrix A n p) (N : Matrix A m p) → (V ++ W) ∷ᵥ (M ∥ N) ≡ (V ∷ᵥ M) ∥ (W ∷ᵥ N)
   ∷ᵥ-∥ {_} {A} {n} {m} {p} V W M N = ≡.refl
 
-  headᵥ : Matrix A n (suc m) → Vec A n
-  headᵥ = head
-
-  tailᵥ : Matrix A n (suc m) → Matrix A n m
-  tailᵥ = tail
-
-  head-∷-tailᵥ : (M : Matrix A n (suc m)) → headᵥ M ∷ᵥ tailᵥ M ≡ M
-  head-∷-tailᵥ (_ ∷ _) = ≡.refl
-
-  []ₕ : Matrix A n 0
-  []ₕ = []
-
   []ₕ-! : (E : Matrix A n 0) → E ≡ []ₕ
   []ₕ-! [] = ≡.refl
 
@@ -128,19 +190,51 @@ opaque
   ∷ᵥ-≑ : (V : Vec A n) (M : Matrix A n m) (N : Matrix A n p) → V ∷ᵥ (M ≑ N) ≡ (V ∷ᵥ M) ≑ N
   ∷ᵥ-≑ V M N = ≡.refl
 
-  _ᵀ : Matrix A n m → Matrix A m n
-  _ᵀ [] = []ᵥ
-  _ᵀ (M₀ ∷ M) = M₀ ∷ₕ M ᵀ
+  ≑-∥
+      : (M : Matrix A n m)
+        (N : Matrix A p m)
+        (P : Matrix A n q)
+        (Q : Matrix A p q)
+      → M ∥ N ≑ P ∥ Q ≡ (M ≑ P) ∥ (N ≑ Q)
+  ≑-∥ M N P Q = begin
+      zipWith _++_ M N ++ zipWith _++_ P Q  ≡⟨ zipWith-++ _++_ M P N Q ⟨
+      zipWith _++_ (M ++ P) (N ++ Q)        ∎
+
+  columns-∷ₕ : (V : Vec A n) (M : Matrix A m n) → columns (V ∷ₕ M) ≡ V ∷ columns M
+  columns-∷ₕ {A = A} {n} {m} [] [] = ≡.refl
+  columns-∷ₕ {A = A} {n} {m} (x ∷ V) (M₀ ∷ M) = begin
+      (x ∷ M₀) ∷ₕ (columns (V ∷ₕ M))  ≡⟨ ≡.cong ((x ∷ M₀) ∷ₕ_) (columns-∷ₕ V M) ⟩
+      (x ∷ V) ∷ columns (M₀ ∷ M)      ∎
+
+  columns-∥ : (M : Matrix A m p) (N : Matrix A n p) → columns (M ∥ N) ≡ columns M ++ columns N
+  columns-∥ {m = m} {n = n} [] [] = ≡.sym (replicate-++ m n [])
+  columns-∥ (M₀ ∷ M) (N₀ ∷ N) = begin
+      zipWith _∷_ (M₀ ++ N₀) (columns (M ∥ N))                  ≡⟨ ≡.cong (zipWith _∷_ (M₀ ++ N₀)) (columns-∥ M N) ⟩
+      zipWith _∷_ (M₀ ++ N₀) (columns M ++ columns N)           ≡⟨ zipWith-++ _∷_ M₀ N₀ (columns M) (columns N) ⟩
+      zipWith _∷_ M₀ (columns M) ++ zipWith _∷_ N₀ (columns N)  ∎
+
+  columns-≑ : (M : Matrix A m n) (N : Matrix A m p) → columns (M ≑ N) ≡ zipWith _++_ (columns M) (columns N)
+  columns-≑ [] N = ≡.sym ([]ᵥ-∥ (columns N))
+  columns-≑ (V ∷ M) N = begin
+      zipWith _∷_ V (columns (M ++ N))                      ≡⟨ ≡.cong (zipWith _∷_ V) (columns-≑ M N) ⟩
+      zipWith _∷_ V (zipWith _++_ (columns M) (columns N))  ≡⟨ ∷ₕ-∥ V (M ᵀ) (N ᵀ) ⟩
+      zipWith _++_ (zipWith _∷_ V (columns M)) (columns N)  ∎
+
+join-[]ᵥ : join ([]ᵥ {a} {Matrix A m p} {n}) ≡ []ᵥ
+join-[]ᵥ = []ᵥ-! (join []ᵥ)
+
+join-[]ₕ : join ([]ₕ {a} {Matrix A m p} {n}) ≡ []ₕ
+join-[]ₕ = []ₕ-! (join []ₕ)
+
+[]ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n}
+[]ᵥ-ᵀ = []ₕ-! ([]ᵥ ᵀ)
 
-  infix 10 _ᵀ
+opaque
 
-  []ᵥ-ᵀ : []ᵥ ᵀ ≡ []ₕ {A = A} {n}
-  []ᵥ-ᵀ {n = zero} = ≡.refl
-  []ᵥ-ᵀ {n = suc n} = ≡.cong (zipWith _∷_ []) ([]ᵥ-ᵀ)
+  unfolding Matrix
 
   ∷ₕ-ᵀ : (V : Vec A n) (M : Matrix A m n) → (V ∷ₕ M) ᵀ ≡ V ∷ᵥ M ᵀ
-  ∷ₕ-ᵀ [] [] = ≡.refl
-  ∷ₕ-ᵀ (x ∷ V) (M₀ ∷ M) = ≡.cong ((x ∷ M₀) ∷ₕ_) (∷ₕ-ᵀ V M)
+  ∷ₕ-ᵀ V M = columns-∷ₕ V M
 
   ∷ᵥ-ᵀ : (V : Vec A m) (M : Matrix A m n) → (V ∷ᵥ M) ᵀ ≡ V ∷ₕ M ᵀ
   ∷ᵥ-ᵀ V M = ≡.refl
@@ -154,6 +248,68 @@ opaque
 
   infix 10 _ᵀᵀ
 
+  ≑ⁿ-∥ : (Ms : Vec (Matrix A n p) q) (Ns : Vec (Matrix A m p) q) → ≑ⁿ (zipWith _∥_ Ms Ns) ≡ ≑ⁿ Ms ∥ ≑ⁿ Ns
+  ≑ⁿ-∥ {n = n} [] [] = ≡.sym ([]ₕ-! ([]ₕ {n = n} ∥ []ₕ))
+  ≑ⁿ-∥ (M ∷ Ms) (N ∷ Ns) = begin
+      M ∥ N ≑ ≑ⁿ (zipWith _∥_ Ms Ns)  ≡⟨ ≡.cong (M ∥ N ≑_) (≑ⁿ-∥ Ms Ns) ⟩
+      M ∥ N ≑ ≑ⁿ Ms ∥ ≑ⁿ Ns           ≡⟨ ≑-∥ M N (≑ⁿ Ms) (≑ⁿ Ns) ⟩
+      (M ≑ ≑ⁿ Ms) ∥ (N ≑ ≑ⁿ Ns)       ∎
+
+  join-∷ₕ : (V : Vec (Matrix A n m) q) (M : Matrix (Matrix A n m) p q) → join (V ∷ₕ M) ≡ ≑ⁿ V ∥ join M
+  join-∷ₕ V M = begin
+      ≑ⁿ (mapₕ ∥ⁿ (V ∷ₕ M))               ≡⟨ ≡.cong ≑ⁿ (map-zipWith ∥ⁿ _∷_ V M) ⟩
+      ≑ⁿ (zipWith (λ x y → x ∥ ∥ⁿ y) V M) ≡⟨ ≡.cong ≑ⁿ (zipWith-map₂ _∥_ ∥ⁿ V M) ⟨
+      ≑ⁿ (zipWith _∥_ V (mapₕ ∥ⁿ M))      ≡⟨ ≑ⁿ-∥ V (mapₕ ∥ⁿ M) ⟩
+      ≑ⁿ V ∥ ≑ⁿ (mapₕ ∥ⁿ M)               ∎
+
+  join-∷ᵥ : (V : Vec (Matrix A n m) p) (M : Matrix (Matrix A n m) p q) → join (V ∷ᵥ M) ≡ ∥ⁿ V ≑ join M
+  join-∷ᵥ V M = ≡.refl
+
+  ≑ⁿ-∷ₕ : (Vs : Vec (Vec A m) p) (Ms : Vec (Matrix A n m) p) → ≑ⁿ (zipWith _∷ₕ_ Vs Ms) ≡ concat Vs ∷ₕ ≑ⁿ Ms
+  ≑ⁿ-∷ₕ [] [] = ≡.sym ([]ₕ-! ([] ∷ₕ []ₕ))
+  ≑ⁿ-∷ₕ (V ∷ Vs) (M ∷ Ms) = begin
+      (V ∷ₕ M) ≑ ≑ⁿ (zipWith _∷ₕ_ Vs Ms)  ≡⟨ ≡.cong ((V ∷ₕ M) ≑_) (≑ⁿ-∷ₕ Vs Ms) ⟩
+      (V ∷ₕ M) ≑ (concat Vs ∷ₕ ≑ⁿ Ms)     ≡⟨ ∷ₕ-≑ V (concat Vs) M (≑ⁿ Ms) ⟨
+      (V ++ concat Vs) ∷ₕ (M ≑ ≑ⁿ Ms)     ∎
+
+  replicate-∷ₕ : (V : Vec A m) (M : Matrix A n m) → replicate p (V ∷ₕ M) ≡ zipWith _∷ₕ_ (replicate p V) (replicate p M)
+  replicate-∷ₕ V M = ≡.sym (zipWith-replicate _∷ₕ_ V M)
+
+  ≑ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ≑ⁿ (replicate p M) ≡ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M)
+  ≑ⁿ-replicate {n = zero} p M = ≡.trans ([]ᵥ-! (≑ⁿ (replicate p M))) (≡.sym ([]ᵥ-! (∷ₕⁿ (mapᵥ (concat ∘ replicate p) M))))
+  ≑ⁿ-replicate {n = suc n} p M = begin
+      ≑ⁿ (replicate p M)                                                            ≡⟨ ≡.cong (≑ⁿ ∘ replicate p) (head-∷-tailₕ M) ⟨
+      ≑ⁿ (replicate p (headₕ M ∷ₕ tailₕ M))                                         ≡⟨ ≡.cong ≑ⁿ (replicate-∷ₕ {p = p} (headₕ M) (tailₕ M)) ⟩
+      ≑ⁿ (zipWith _∷ₕ_ (replicate p (headₕ M)) (replicate p (tailₕ M)))             ≡⟨ ≑ⁿ-∷ₕ (replicate p (headₕ M)) (replicate p (tailₕ M)) ⟩
+      concat (replicate p (headₕ M)) ∷ₕ (≑ⁿ (replicate p (tailₕ M)))                ≡⟨ ≡.cong (concat (replicate p (headₕ M)) ∷ₕ_) (≑ⁿ-replicate p (tailₕ M)) ⟩
+      concat (replicate p (headₕ M)) ∷ₕ ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (tailₕ M)) ≡⟨ ≡.cong (∷ₕⁿ ∘ Vec.map (concat ∘ replicate p)) (∷ₕ-ᵀ (headₕ M) (tailₕ M)) ⟨
+      ∷ₕⁿ (mapᵥ (concat ∘ replicate p) (headₕ M ∷ₕ tailₕ M))                        ≡⟨ ≡.cong (∷ₕⁿ ∘ mapᵥ (concat ∘ replicate p)) (head-∷-tailₕ M) ⟩
+      ∷ₕⁿ (mapᵥ (concat ∘ replicate p) M)                                           ∎
+
+  ∥ⁿ-replicate : (p : ℕ) (M : Matrix A n m) → ∥ⁿ (replicate p M) ≡ ∷ᵥⁿ (mapₕ (concat ∘ replicate p) M)
+  ∥ⁿ-replicate zero M = ≡.sym (map-const M [])
+  ∥ⁿ-replicate (suc p) M = begin
+      zipWith _++_ M (∥ⁿ (replicate p M))                             ≡⟨ ≡.cong (zipWith _++_ M) (∥ⁿ-replicate p M) ⟩
+      zipWith _++_ M (Vec.map (concat ∘ replicate p) M)               ≡⟨ ≡.cong (λ h → zipWith _++_ h (Vec.map (concat ∘ replicate p) M)) (map-id M) ⟨
+      zipWith _++_ (Vec.map id M) (Vec.map (concat ∘ replicate p) M)  ≡⟨ zipWith-map id (concat ∘ replicate p) _++_ M ⟩
+      Vec.map (λ V → V ++ concat (replicate p V)) M                   ∎
+
+opaque
+
+  unfolding ∷ₕⁿ
+
+  columns-∷ₕⁿ : (Vs : Vec (Vec A n) m) → columns (∷ₕⁿ Vs) ≡ Vs
+  columns-∷ₕⁿ Vs = Vs ᵀᵀ
+
+  ∷ₕⁿ-columns : (M : Matrix A n m) → ∷ₕⁿ (columns M) ≡ M
+  ∷ₕⁿ-columns M = M ᵀᵀ
+
+  ∷ᵥⁿ-rows : (M : Matrix A n m) → ∷ᵥⁿ (rows M) ≡ M
+  ∷ᵥⁿ-rows M = ≡.refl
+
+  ∷ᵥⁿ-ᵀ : (Vs : Vec (Vec A n) m) → ∷ᵥⁿ Vs ᵀ ≡ ∷ₕⁿ Vs
+  ∷ᵥⁿ-ᵀ Vs = ≡.refl
+
 open Pointwise
 
 module Natural (f : A → B) where
@@ -162,7 +318,7 @@ module Natural (f : A → B) where
 
   opaque
 
-    unfolding map
+    unfolding Matrix
 
     α-∥ : (M : Matrix A n p) (N : Matrix A m p) → map f (M ∥ N) ≡ map f M ∥ map f N
     α-∥ M N = begin
@@ -216,23 +372,6 @@ module Natural (f : A → B) where
         Vec.map f V ∷ₕ map f (M ᵀ)  ≡⟨ ≡.cong (Vec.map f V ∷ₕ_) (α-ᵀ M) ⟩
         Vec.map f V ∷ₕ map f M ᵀ    ∎
 
-opaque
-
-  unfolding PW
-
-  -- TODO double functor
-  map₂
-      : {R : REL A B ℓ}
-        {S : REL C D ℓ}
-        {f : A → C}
-        {g : B → D}
-      → (∀ {x y} → R x y → S (f x) (g y))
-      → {M₁ : Matrix A m n}
-        {M₂ : Matrix B m n}
-      → PW R M₁ M₂
-      → PW S (map f M₁) (map g M₂)
-  map₂ R⇒S = map⁺ (map⁺ R⇒S)
-
 module Relation {R : REL A B ℓ} where
 
   open Vector.Relation