Reorganize matrix code

1 files changed, 93 insertions, 0 deletions

diff --git a/Data/Matrix/Monoid.agda b/Data/Matrix/Monoid.agda
new file mode 100644
index 0000000..b7638f6
--- /dev/null
+++ b/Data/Matrix/Monoid.agda
@@ -0,0 +1,93 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra using (Monoid)
+open import Level using (Level)
+
+module Data.Matrix.Monoid {c ℓ : Level} (M : Monoid c ℓ) where
+
+module M = Monoid M
+
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+open import Data.Matrix.Core M.setoid using (Matrix; _≋_; _ᵀ; _∷ₕ_; []ᵥ; _≑_; _∥_; []ᵥ-!; []ᵥ-∥; ∷ₕ-∥)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec; replicate; zipWith)
+open import Data.Vec.Properties using (zipWith-replicate)
+open import Data.Vector.Monoid M using (_⊕_; ⊕-cong; ⊕-identityˡ; ⊕-identityʳ; ⟨ε⟩)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+
+open M
+open Vec
+open ℕ
+
+private
+  variable
+    A B C : ℕ
+
+opaque
+
+  unfolding Matrix
+
+  𝟎 : Matrix A B
+  𝟎 {A} {B} = replicate B ⟨ε⟩
+
+  opaque
+
+    unfolding _ᵀ []ᵥ ⟨ε⟩
+
+    𝟎ᵀ : 𝟎 ᵀ ≡ 𝟎 {A} {B}
+    𝟎ᵀ {zero} = ≡.refl
+    𝟎ᵀ {suc A} = let open ≡-Reasoning in begin
+        ⟨ε⟩ ∷ₕ (𝟎 ᵀ)  ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎ᵀ ⟩
+        ⟨ε⟩ ∷ₕ 𝟎      ≡⟨ zipWith-replicate _∷_ ε ⟨ε⟩ ⟩
+        𝟎             ∎
+
+  opaque
+
+    unfolding _≑_
+
+    𝟎≑𝟎 : 𝟎 {A} {B} ≑ 𝟎 {A} {C} ≡ 𝟎
+    𝟎≑𝟎 {B = zero} = ≡.refl
+    𝟎≑𝟎 {B = suc B} = ≡.cong (⟨ε⟩ ∷_) (𝟎≑𝟎 {B = B})
+
+  opaque
+
+    unfolding _∷ₕ_ ⟨ε⟩
+
+    ⟨ε⟩∷ₕ𝟎 : ⟨ε⟩ ∷ₕ 𝟎 {A} {B} ≡ 𝟎
+    ⟨ε⟩∷ₕ𝟎 {A} {zero} = ≡.refl
+    ⟨ε⟩∷ₕ𝟎 {A} {suc B} = ≡.cong (⟨ε⟩ ∷_) ⟨ε⟩∷ₕ𝟎
+
+𝟎∥𝟎 : 𝟎 {A} {C} ∥ 𝟎 {B} {C} ≡ 𝟎
+𝟎∥𝟎 {zero} {C} rewrite []ᵥ-! (𝟎 {0} {C}) = []ᵥ-∥ 𝟎
+𝟎∥𝟎 {suc A} {C} {B} = begin
+    𝟎 ∥ 𝟎               ≡⟨ ≡.cong (_∥ 𝟎) (⟨ε⟩∷ₕ𝟎 {A} {C}) ⟨
+    (⟨ε⟩ ∷ₕ 𝟎 {A}) ∥ 𝟎  ≡⟨ ∷ₕ-∥ ⟨ε⟩ 𝟎 𝟎 ⟨
+    ⟨ε⟩ ∷ₕ 𝟎 {A} ∥ 𝟎    ≡⟨ ≡.cong (⟨ε⟩ ∷ₕ_) 𝟎∥𝟎 ⟩
+    ⟨ε⟩ ∷ₕ 𝟎            ≡⟨ ⟨ε⟩∷ₕ𝟎 ⟩
+    𝟎                   ∎
+  where
+    open ≡-Reasoning
+
+opaque
+
+  unfolding Matrix
+
+  _[+]_ : Matrix A B → Matrix A B → Matrix A B
+  _[+]_ = zipWith _⊕_
+
+  [+]-cong : {M M′ N N′ : Matrix A B} → M ≋ M′ → N ≋ N′ → M [+] N ≋ M′ [+] N′
+  [+]-cong = PW.zipWith-cong ⊕-cong
+
+  opaque
+
+    unfolding 𝟎
+
+    [+]-𝟎ˡ : (M : Matrix A B) → 𝟎 [+] M ≋ M
+    [+]-𝟎ˡ [] = PW.[]
+    [+]-𝟎ˡ (M₀ ∷ M) = ⊕-identityˡ M₀ PW.∷ [+]-𝟎ˡ M
+
+    [+]-𝟎ʳ : (M : Matrix A B) → M [+] 𝟎 ≋ M
+    [+]-𝟎ʳ [] = PW.[]
+    [+]-𝟎ʳ (M₀ ∷ M) = ⊕-identityʳ M₀ PW.∷ [+]-𝟎ʳ M