-
Notifications
You must be signed in to change notification settings - Fork 0
/
Fin_Sig.v
158 lines (116 loc) · 3.82 KB
/
Fin_Sig.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
Require Import
Coq.setoid_ring.Ring_theory
Coq.Vectors.Vector Setoid Morphisms BinPos BinNat
CoLoR.Util.Vector.VecUtil Lia
Coq.ZArith.ZArith.
Set Implicit Arguments.
Section General_Matrix_Multiplication.
Variable R : Type.
Variable (rO rI : R) (radd rmul : R->R->R).
Variable srt : semi_ring_theory rO rI radd rmul (@eq R).
Definition matrix m n := vector (vector R n) m.
Definition get_row {m n : nat} (M : matrix m n) i (ip : i < m) :=
Vnth M ip.
Definition get_col {m n : nat} (M : matrix m n) i (ip : i < n) :=
Vmap (fun v => Vnth v ip) M.
Definition get_elem {m n : nat} (M : matrix m n) i j (ip : i < m) (jp : j < n) :=
Vnth (get_row M ip) jp.
Definition vnth : forall (n : nat), vector R n -> forall (i : nat), i < n -> R.
Proof.
refine (fix IHn n :=
match n as np return n = np -> vector R np -> forall i, i < np -> R with
| 0 => fun Hn v i Hi => _
| S n' => fun Hn v i Hi =>
match i as ip return i = _ -> R with
| 0 => fun Hip => hd v
| S i' => fun Hip => _
end eq_refl
end eq_refl).
++ abstract lia.
++ subst. apply Lt.lt_S_n in Hi.
exact (IHn n' (tl v) i' Hi).
Defined.
Definition Matrix (m n : nat) := forall i, i < m -> forall j, j < n -> R.
Lemma f : forall m n, Matrix m n -> (Fin.t m -> Fin.t n -> R).
Proof.
induction m.
+ intros ? Hm Hf1 Hf2.
inversion Hf1.
+ (* m = S m*)
destruct n.
++ intros Hm Hf1 Hf2.
inversion Hf2.
++ intros Hm Hf1 Hf2.
remember Hf1 as Hf1'.
remember Hf2 as Hf2'.
(* destruct both.
1. F1, F1
2. F1, FS
3. FS, F1.
4. FS, FS *)
destruct Hf1, Hf2.
+++ assert (Hl1: 0 < S n0) by abstract lia.
assert (Hl2: 0 < S n1) by abstract lia.
exact (Hm 0 Hl1 0 Hl2).
+++ assert (Hl1: 0 < S n0) by abstract lia.
assert (Hl2: n1 < S n1) by abstract lia.
exact (Hm 0 Hl1 n1 Hl2).
+++ assert (Hl1: n0 < S n0) by abstract lia.
assert (Hl2 : 0 < S n1) by abstract lia.
exact (Hm n0 Hl1 0 Hl2).
+++ assert (Hl1: n0 < S n0) by abstract lia.
assert (Hl2: n1 < S n1) by abstract lia.
exact (Hm n0 Hl1 n1 Hl2).
Defined.
Theorem fin_cast : forall m n, m = n -> Fin.t m -> Fin.t n.
Proof.
intros ? ? Hm v.
refine
match Hm in _ = n return Fin.t n with
| eq_refl => v
end.
Defined.
Lemma fin_sig : forall m, Fin.t m -> sig (fun i => i < m). (* {i | i < m}*)
Proof.
refine (fix fn m :=
match m : nat as mt return m = mt -> Fin.t mt -> sig (fun i => i < mt) with
| 0 => _
| S m' => fun Hm Hf => _
end eq_refl).
+ intros Hm Hf.
inversion Hf.
+ remember Hf as Hf'.
destruct Hf.
++ exists 0.
apply Nat.lt_0_succ.
++ destruct m.
+++ inversion Hm.
+++ inversion Hm; clear Hm.
symmetry in H0.
pose proof (@fin_cast n m H0 Hf).
destruct (fn m H) as [hm Hm].
exists (S hm).
apply lt_n_S.
rewrite H0. exact Hm.
Defined.
Eval compute in (fin_sig (Fin.FS (Fin.FS Fin.F1))).
Lemma sig_fin : forall m, sig (fun i => i < m) -> Fin.t m.
Proof.
induction m.
+ intros [i Hi].
abstract lia.
+ intros [i Hi].
++ destruct i.
+++ exact (Fin.F1).
+++ assert (Ht : i < m) by abstract lia.
assert (Hv : {i | i < m}). exists i.
abstract lia.
exact (Fin.FS (IHm Hv)).
Defined.
Lemma g : forall m n, (Fin.t m -> Fin.t n -> R) -> Matrix m n.
Proof.
Admitted.
Theorem pf : forall m n (u : Matrix m n), g (f u) = u.
Proof.
Admitted.
End General_Matrix_Multiplication.