Update matrices and vectors

1 files changed, 171 insertions, 0 deletions

diff --git a/Data/Matrix/BaseChange.agda b/Data/Matrix/BaseChange.agda
new file mode 100644
index 0000000..906d1dd
--- /dev/null
+++ b/Data/Matrix/BaseChange.agda
@@ -0,0 +1,171 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (Semiring)
+open import Algebra.Morphism.Bundles using (SemiringHomomorphism)
+open import Level using (Level)
+
+module Data.Matrix.BaseChange
+    {c ℓ : Level}
+    (R S : Semiring c ℓ)
+    (open Semiring using (rawSemiring))
+    (f : SemiringHomomorphism (rawSemiring R) (rawSemiring S))
+  where
+
+module R = Semiring R
+module S = Semiring S
+
+import Data.Matrix.Category as MCat
+import Data.Matrix.Core as MC
+import Data.Matrix.Endofunctor as Endo
+import Data.Matrix.Monoid as MM
+import Data.Matrix.Raw as MR
+import Data.Matrix.Transform as MT
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+import Data.Vector.Bisemimodule as VB
+import Data.Vector.Core as VC
+import Data.Vector.Endofunctor.Monoid as MonEndo
+import Data.Vector.Endofunctor.Setoid as VecEndo
+import Data.Vector.Monoid as VM
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+open import Categories.Functor using (Functor)
+open import Category.Instance.Monoids using (MonoidHomomorphism; mk-⇒)
+open import Data.Matrix.Category using (Mat)
+open import Data.Matrix.Transform using (I)
+open import Data.Nat using (ℕ)
+open import Data.Vec using (map; []; _∷_; zipWith; replicate)
+open import Data.Vec.Properties using (map-∘; map-replicate)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (map⁺)
+open import Data.Vector.Core S.setoid using (_≊_)
+open import Data.Vector.Core using (Vector)
+open import Data.Vector.Monoid using (⟨ε⟩)
+open import Data.Vector.Raw using (module Relation)
+open import Function using (id; Func; _⟶ₛ_; _⟨$⟩_; _∘_)
+open import Level using (0ℓ)
+
+open Func
+open Functor
+open MC using (Matrix)
+open SemiringHomomorphism f
+open ℕ
+private module Mat {A B : ℕ} = Functor (Endo.Mat A B {c} {ℓ})
+
+open MR hiding (map; Matrix)
+
+module MatR where
+  open MC R.setoid public
+  open MM R.+-monoid public
+  open MT R public
+  open MCat R using (_·_) public
+
+module MatS where
+  open MC S.setoid public
+  open MM S.+-monoid public
+  open MT S public
+  open MCat S using (_·_) public
+
+module VecR where
+  open VC R.setoid public
+  open VM R.+-monoid public
+  open VB R public
+
+module VecS where
+  open VC S.setoid public
+  open VM S.+-monoid public
+  open VB S public
+
+func : R.setoid ⟶ₛ S.setoid
+func .to = ⟦_⟧
+func .cong = ⟦⟧-cong
+
+change
+    : {A B : ℕ}
+    → Matrix R.setoid A B
+    → Matrix S.setoid A B
+change = to (Mat.₁ func)
+
+resp
+    : {A B : ℕ}
+      {M M′ : MatR.Matrix A B}
+    → M MatR.≋ M′
+    → change M MatS.≋ change M′
+resp = cong (Mat.₁ func)
+
+opaque
+  unfolding I _ᵀ _∷ₕ_ Endo.mapₛ
+  ident : {A : ℕ} → change (I R) MatS.≋ I S {A}
+  ident {zero} = PW.[]
+  ident {suc A} = (1#-homo PW.∷ ⟨ε⟩-homo) PW.∷ map-⟨ε⟩∷ₕI
+    where
+      ⟨ε⟩-homo : (map ⟦_⟧) VecR.⟨ε⟩ ≊ VecS.⟨ε⟩ {A}
+      ⟨ε⟩-homo = MonoidHomomorphism.ε-homo (MonEndo.mapₘ A (mk-⇒ +-monoidHomomorphism))
+      map-⟨ε⟩∷ₕI : map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I) MatS.≋ VecS.⟨ε⟩ ∷ₕ MatS.I {A}
+      map-⟨ε⟩∷ₕI = begin
+          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I)            ≡⟨ ≡.cong (λ h → map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ h)) MatR.Iᵀ ⟨
+          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ₕ MatR.I ᵀ)          ≡⟨ ≡.cong (map (map ⟦_⟧)) (∷ᵥ-ᵀ VecR.⟨ε⟩ MatR.I) ⟨
+          map (map ⟦_⟧) ((VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ)        ≡⟨ Natural.α-ᵀ ⟦_⟧ (VecR.⟨ε⟩ ∷ᵥ MatR.I) ⟩
+          map (map ⟦_⟧) (VecR.⟨ε⟩ ∷ᵥ MatR.I) ᵀ          ≡⟨⟩
+          (map ⟦_⟧ VecR.⟨ε⟩ ∷ᵥ map (map ⟦_⟧) MatR.I) ᵀ  ≡⟨ ∷ᵥ-ᵀ (map ⟦_⟧ VecR.⟨ε⟩) (map (map ⟦_⟧) MatR.I) ⟩
+          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ (map (map ⟦_⟧) MatR.I ᵀ)  ≡⟨ ≡.cong (map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ_) (Natural.α-ᵀ ⟦_⟧ MatR.I) ⟨
+          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) (MatR.I ᵀ)  ≡⟨ ≡.cong (λ h → map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) h) MatR.Iᵀ ⟩
+          map ⟦_⟧ VecR.⟨ε⟩ ∷ₕ map (map ⟦_⟧) MatR.I      ≈⟨ MatS.∷ₕ-cong ⟨ε⟩-homo ident ⟩
+          VecS.⟨ε⟩ ∷ₕ MatS.I                            ∎
+        where
+          open ≈-Reasoning (MatS.Matrixₛ (suc A) A)
+
+opaque
+  unfolding VecR._∙_
+  ⟦⟧-∙ : {n : ℕ} (V W : VecR.Vector n) → ⟦ V VecR.∙ W ⟧ S.≈ map ⟦_⟧ V VecS.∙ map ⟦_⟧ W
+  ⟦⟧-∙ {zero} [] [] = 0#-homo
+  ⟦⟧-∙ {suc n} (x ∷ V) (y ∷ W) = begin
+      ⟦ x VecR.R.* y VecR.R.+ V VecR.∙ W ⟧                  ≈⟨ +-homo (x VecR.R.* y) (V VecR.∙ W) ⟩
+      ⟦ x VecR.R.* y ⟧ S.+ ⟦ V VecR.∙ W ⟧                   ≈⟨ S.+-cong (*-homo x y) (⟦⟧-∙ V W) ⟩
+      ⟦ x ⟧ VecS.R.* ⟦ y ⟧ S.+ (map ⟦_⟧ V VecS.∙ map ⟦_⟧ W) ∎
+    where
+      open ≈-Reasoning S.setoid
+
+opaque
+  unfolding VecR.⟨ε⟩
+  ⟦⟧-⟨ε⟩ : {n : ℕ} → map ⟦_⟧ (VecR.⟨ε⟩ {n}) VecS.≊ VecS.⟨ε⟩
+  ⟦⟧-⟨ε⟩ {n} = begin
+      map ⟦_⟧ (replicate n R.0#)  ≡⟨ map-replicate ⟦_⟧ R.0# n ⟩
+      replicate n ⟦ R.0# ⟧        ≈⟨ VecS.replicate-cong 0#-homo ⟩
+      replicate n VecS.R.0#       ∎
+    where
+      open ≈-Reasoning (VecS.Vectorₛ n)
+
+opaque
+  unfolding MatR.[_]_ Endo.mapₛ
+  ⟦⟧-[-]-
+      : {n m : ℕ}
+        (V : VecR.Vector n)
+        (M : MatR.Matrix m n)
+      → map ⟦_⟧ (MatR.[ V ] M) VecS.≊ MatS.[ map ⟦_⟧ V ] (change M)
+  ⟦⟧-[-]- {n} {m} V M = begin
+      map ⟦_⟧ (map (V VecR.∙_) (M ᵀ))                 ≡⟨ map-∘ ⟦_⟧ (V VecR.∙_) (M ᵀ) ⟨
+      map (λ x → ⟦ V VecR.∙ x ⟧) (M ᵀ)                ≈⟨ PW.map⁺ (λ {x y} ≈xy → S.trans (⟦⟧-cong (VecR.∙-cong VecR.≊.refl ≈xy)) (⟦⟧-∙ V y)) MatR.≋.refl ⟩
+      map (λ x → map ⟦_⟧ V VecS.∙ map ⟦_⟧ x) (M ᵀ)    ≡⟨ map-∘ ((map ⟦_⟧ V) VecS.∙_) (map ⟦_⟧) (M ᵀ) ⟩
+      map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) (M ᵀ)) ≡⟨ ≡.cong ( map ((map ⟦_⟧ V) VecS.∙_)) (Natural.α-ᵀ ⟦_⟧ M) ⟩
+      map ((map ⟦_⟧ V) VecS.∙_) (map (map ⟦_⟧) M ᵀ)   ∎
+    where
+      open ≈-Reasoning (VecS.Vectorₛ m)
+
+opaque
+  unfolding Endo.mapₛ MatR.[_]_
+  homo
+      : {X Y Z : ℕ}
+        {M : MatR.Matrix X Y}
+        {N : MatR.Matrix Y Z}
+      → change (N MatR.· M) MatS.≋ change N MatS.· change M
+  homo {X} {Y} {Z} {M} {[]} = PW.[]
+  homo {X} {Y} {suc Z} {M} {N₀ ∷ N} = ⟦⟧-[-]- N₀ M PW.∷ homo {X} {Y} {Z} {M} {N}
+
+ChangeBase : Functor (Mat R) (Mat S)
+ChangeBase = record
+    { F₀ = id
+    ; F₁ = change
+    ; identity = ident
+    ; homomorphism = homo
+    ; F-resp-≈ = resp
+    }