-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathMatrixLemmas.v
177 lines (141 loc) · 5.39 KB
/
MatrixLemmas.v
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
172
173
174
175
Require Import
Coq.Lists.List
Coq.Strings.String
Coq.Setoids.Setoid
Coq.Arith.PeanoNat
Coq.omega.Omega
Coq.setoid_ring.Ring
Coq.setoid_ring.Ring_theory
Matrix
SparseMatrix
DenseMatrix
MyHelpers.
Notation SDM n := (Mt (Matrix := DenseMatrix) n n).
Notation SSM n := (Mt (Matrix := SparseMatrix) n n).
Notation Vt n := (Mt (Matrix := DenseMatrix) n 1).
Global Opaque DenseMatrix.
Global Opaque SparseMatrix.
Section MatrixLemmas.
Context {E: MatrixElem}.
Definition transpose {n m MM} (A : @Mt E MM n m) :=
@Mfill E MM m n (fun i j => Mget A j i).
Definition MVtimes {n} (M: SDM n) (v: Vt n) := M @* v.
Axiom inversion : forall {n}, SDM n -> SDM n.
Global Add Parametric Morphism n: (MVtimes ) with
signature (Meq (m:=n)(n:=n)) ==> (Meq (m:=n)(n:=1)) ==> (Meq (m:=n)(n:=1)) as MVtimes_mor.
Admitted.
Global Add Parametric Morphism n m MM: (transpose ) with
signature (Meq (m:=m)(n:=n)(M1:=MM)) ==> (Meq (m:=n)(n:=m)(M1:=MM)) as transpose_mor.
Admitted.
Global Add Parametric Morphism n: (inversion ) with
signature (Meq (m:=n)(n:=n)) ==> (Meq (m:=n)(n:=n)) as inversion_mor.
Admitted.
Global Add Parametric Morphism m n: (Mget) with
signature (Meq (m:=m)(n:=n)(ME:=E)(M1:=DenseMatrix)) ==> (eq) ==> (eq) ==> (eq) as mget_mor.
Admitted.
Infix "&*" := MVtimes (at level 40, left associativity) : matrix_scope.
Definition Vplus {n} (v: Vt n) (u: Vt n):= v @+ u.
Infix "&+" := Vplus (at level 50, left associativity) : matrix_scope.
Global Add Parametric Morphism n: (Vplus ) with
signature (Meq (m:=n)(n:=1)) ==> (Meq (m:=n)(n:=1)) ==> (Meq (m:=n)(n:=1)) as Vplus_mor.
Admitted.
Definition Vminus {n} (v: Vt n) (u: Vt n):= v @- u.
Infix "&-" := Vminus (at level 50, left associativity) : matrix_scope.
Global Add Parametric Morphism n: (Vminus ) with
signature (Meq (m:=n)(n:=1)) ==> (Meq (m:=n)(n:=1)) ==> (Meq (m:=n)(n:=1)) as Vminus_mor.
Admitted.
Definition Id {n} := @I n E DenseMatrix.
Arguments Mtimes : simpl never.
Definition sparsify {n} (A: SDM n) := @Mfill E SparseMatrix n n (fun i j => Mget A i j).
Lemma sparsify_correct: forall n: nat, forall M : SDM n, M @= sparsify M.
Proof.
intros.
unfold sparsify.
unfold "@=".
intros.
rewrite Mfill_correct; try assumption.
reflexivity.
Qed.
(* can be optimized *)
Definition densify {n} (A: SSM n) := @Mfill E DenseMatrix n n (fun i j => Mget A i j).
Lemma densify_correct: forall n: nat, forall M : SSM n, M @= densify M.
Proof.
intros.
unfold densify.
unfold "@=".
intros.
rewrite Mfill_correct; try assumption.
reflexivity.
Qed.
Lemma densify_correct_rev: forall n: nat, forall M : SSM n, densify M @= M.
Proof.
intros.
unfold densify.
unfold "@=".
intros.
rewrite Mfill_correct; try assumption.
reflexivity.
Qed.
Lemma matrix_eq_commutes :
forall (m n: nat) ME M1 M2 (m1: @Mt ME M1 m n) (m2: @Mt ME M2 m n),
m1 @= m2 -> m2 @= m1.
Proof.
intros.
unfold "@=" in *.
intros.
rewrite H; auto.
Qed.
Axiom solveR: forall {n}, SDM n -> SDM n -> SDM n.
Axiom solveR_correct: forall n: nat, forall M1 M2:SDM n,
M1 @* (inversion M2) = solveR M2 M1.
Lemma multi_assoc: forall n: nat, forall M1 M2 M3 : SDM n,
(M1 @* M2) @* M3 @= M1 @* (M2 @* M3).
Proof.
intros.
rewrite mult_assoc.
reflexivity.
Qed.
Axiom Cholesky_DC: forall {n}, SDM n -> SDM n.
Axiom solveR_lower: forall {n}, SDM n -> SDM n -> SDM n.
Axiom solveR_upper: forall {n}, SDM n -> SDM n -> SDM n.
Lemma ABv_assoc: forall n:nat, forall A B: SDM n, forall v : Vt n,
MVtimes (A @* B) v @= MVtimes A (MVtimes B v).
Proof.
intros.
unfold "&*".
rewrite mult_assoc.
reflexivity.
Qed.
Axiom Cholesky_DC_correct: forall n:nat, forall M1 M2 : SDM n,
solveR M1 M2 = solveR_upper (transpose (Cholesky_DC M1)) (solveR_lower (Cholesky_DC M1) M2).
Axiom Densify_correct: forall n:nat, forall M : SDM n, forall S : SSM n,
M @= S -> M @= densify S.
Lemma Densify_correct_rev: forall n:nat, forall M : SDM n, forall S : SSM n,
M @= densify S -> M @= S.
Proof.
intros.
unfold densify in H.
unfold "@=" in *.
intros.
rewrite H; auto.
rewrite Mfill_correct; auto.
Qed.
Axiom dense_sparse_mul: forall {n}, SDM n -> SSM n -> SDM n.
Axiom dense_sparse_mul_correct: forall {n}, forall A: SDM n, forall B: SSM n,
dense_sparse_mul A B = A @* densify B.
Axiom sparse_dense_mul: forall {n}, SSM n -> SDM n -> SDM n.
Axiom sparse_dense_mul_correct: forall {n}, forall A: SSM n, forall B: SDM n,
sparse_dense_mul A B = densify A @* B.
Axiom dense_sparse_mul_to_sparse: forall {n}, SDM n -> SSM n -> SSM n.
Axiom dense_sparse_mul_to_sparse_correct: forall {n}, forall A: SDM n, forall B: SSM n,
sparsify (dense_sparse_mul A B) = dense_sparse_mul_to_sparse A B.
Lemma if_cond_helper {n m MM} : forall x1:bool, forall A B C D: @Mt E MM n m, A @= B -> C @= D -> (if x1 then A else C) @= (if x1 then B else D).
Proof.
intros.
destruct x1; auto.
Qed.
End MatrixLemmas.
Hint Resolve sparsify_correct densify_correct densify_correct_rev matrix_eq_commutes solveR_correct multi_assoc Densify_correct Densify_correct_rev dense_sparse_mul_correct sparse_dense_mul_correct dense_sparse_mul_to_sparse_correct eq_Mt_refl: matrices.
Infix "&*" := MVtimes (at level 40, left associativity) : matrix_scope.
Infix "&+" := Vplus (at level 50, left associativity) : matrix_scope.
Infix "&-" := Vminus (at level 50, left associativity) : matrix_scope.