blob: 906d1dd1d1aa95f193150e7caaa34c436dadee88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
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
}
|
