blob: b7638f6a0ec4480439c66c9ce04610fde88286ff (
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
|
{-# 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
|
