blob: 00f0cbe896e917f77af089e7ccf950a935e388c0 (
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
Require Ring.
Require Export Field_Compl.
Require Export Field_Theory.
(**** Interpretation A --> ExprA ****)
Recursive Tactic Definition MemAssoc var lvar :=
Match lvar With
| [(nil ?)] -> false
| [(cons ? ?1 ?2)] ->
(Match ?1==var With
| [?1== ?1] -> true
| _ -> (MemAssoc var ?2)).
Recursive Tactic Definition SeekVarAux FT lvar trm :=
Let AT = Eval Compute in (A FT)
And AzeroT = Eval Compute in (Azero FT)
And AoneT = Eval Compute in (Aone FT)
And AplusT = Eval Compute in (Aplus FT)
And AmultT = Eval Compute in (Amult FT)
And AoppT = Eval Compute in (Aopp FT)
And AinvT = Eval Compute in (Ainv FT) In
Match trm With
| [(AzeroT)] -> lvar
| [(AoneT)] -> lvar
| [(AplusT ?1 ?2)] ->
Let l1 = (SeekVarAux FT lvar ?1) In
(SeekVarAux FT l1 ?2)
| [(AmultT ?1 ?2)] ->
Let l1 = (SeekVarAux FT lvar ?1) In
(SeekVarAux FT l1 ?2)
| [(AoppT ?1)] -> (SeekVarAux FT lvar ?1)
| [(AinvT ?1)] -> (SeekVarAux FT lvar ?1)
| [?1] ->
Let res = (MemAssoc ?1 lvar) In
Match res With
| [(true)] -> lvar
| [(false)] -> '(cons AT ?1 lvar).
Tactic Definition SeekVar FT trm :=
Let AT = Eval Compute in (A FT) In
(SeekVarAux FT '(nil AT) trm).
Recursive Tactic Definition NumberAux lvar cpt :=
Match lvar With
| [(nil ?1)] -> '(nil (Sprod ?1 nat))
| [(cons ?1 ?2 ?3)] ->
Let l2 = (NumberAux ?3 '(S cpt)) In
'(cons (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
Tactic Definition Number lvar := (NumberAux lvar O).
Tactic Definition BuildVarList FT trm :=
Let lvar = (SeekVar FT trm) In
(Number lvar).
Recursive Tactic Definition Assoc elt lst :=
Match lst With
| [(nil ?)] -> Fail
| [(cons (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
Match elt== ?1 With
| [?1== ?1] -> ?2
| _ -> (Assoc elt ?3).
Recursive Tactic Definition interp_A FT lvar trm :=
Let AT = Eval Compute in (A FT)
And AzeroT = Eval Compute in (Azero FT)
And AoneT = Eval Compute in (Aone FT)
And AplusT = Eval Compute in (Aplus FT)
And AmultT = Eval Compute in (Amult FT)
And AoppT = Eval Compute in (Aopp FT)
And AinvT = Eval Compute in (Ainv FT) In
Match trm With
| [(AzeroT)] -> EAzero
| [(AoneT)] -> EAone
| [(AplusT ?1 ?2)] ->
Let e1 = (interp_A FT lvar ?1)
And e2 = (interp_A FT lvar ?2) In
'(EAplus e1 e2)
| [(AmultT ?1 ?2)] ->
Let e1 = (interp_A FT lvar ?1)
And e2 = (interp_A FT lvar ?2) In
'(EAmult e1 e2)
| [(AoppT ?1)] ->
Let e = (interp_A FT lvar ?1) In
'(EAopp e)
| [(AinvT ?1)] ->
Let e = (interp_A FT lvar ?1) In
'(EAinv e)
| [?1] ->
Let idx = (Assoc ?1 lvar) In
'(EAvar idx).
(************************)
(* Simplification *)
(************************)
(**** Generation of the multiplier ****)
Recursive Tactic Definition Remove e l :=
Match l With
| [(nil ?)] -> l
| [(cons ?1 e ?2)] -> ?2
| [(cons ?1 ?2 ?3)] ->
Let nl = (Remove e ?3) In
'(cons ?1 ?2 nl).
Recursive Tactic Definition Union l1 l2 :=
Match l1 With
| [(nil ?)] -> l2
| [(cons ?1 ?2 ?3)] ->
Let nl2 = (Remove ?2 l2) In
Let nl = (Union ?3 nl2) In
'(cons ?1 ?2 nl).
Recursive Tactic Definition RawGiveMult trm :=
Match trm With
| [(EAinv ?1)] -> '(cons ExprA ?1 (nil ExprA))
| [(EAopp ?1)] -> (RawGiveMult ?1)
| [(EAplus ?1 ?2)] ->
Let l1 = (RawGiveMult ?1)
And l2 = (RawGiveMult ?2) In
(Union l1 l2)
| [(EAmult ?1 ?2)] ->
Let l1 = (RawGiveMult ?1)
And l2 = (RawGiveMult ?2) In
Eval Compute in (app ExprA l1 l2)
| _ -> '(nil ExprA).
Tactic Definition GiveMult trm :=
Let ltrm = (RawGiveMult trm) In
'(mult_of_list ltrm).
(**** Associativity ****)
Tactic Definition ApplyAssoc FT lvar trm :=
Cut (interp_ExprA FT lvar (assoc trm))==(interp_ExprA FT lvar trm);
[Intro;
(Match Context With
| [id:(interp_ExprA ?1 ?2 (assoc ?3))== ?4 |- ?] ->
Let t=Eval Compute in (assoc ?3) In
Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
|Apply assoc_correct].
(**** Distribution *****)
Tactic Definition ApplyDistrib FT lvar trm :=
Cut (interp_ExprA FT lvar (distrib trm))==(interp_ExprA FT lvar trm);
[Intro;
(Match Context With
| [id:(interp_ExprA ?1 ?2 (distrib ?3))== ?4 |- ?] ->
Let t=Eval Compute in (distrib ?3) In
Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
|Apply distrib_correct].
(**** Multiplication by the inverse product ****)
Tactic Definition GrepMult :=
Match Context With
| [ id: ~(interp_ExprA ? ? ?)== ? |- ?] -> id.
Tactic Definition Multiply mul :=
Match Context With
| [|-(interp_ExprA ?1 ?2 ?3)==(interp_ExprA ?1 ?2 ?4)] ->
Let AzeroT = Eval Compute in (Azero ?1) In
Cut ~(interp_ExprA ?1 ?2 mul)==AzeroT;
[Intro;
Let id = GrepMult In
Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*;
Cbv Beta Delta -[interp_ExprA] Zeta Iota*)
|Cbv Beta Delta -[not] Zeta Iota;
Let AmultT = Eval Compute in (Amult ?1)
And AoneT = Eval Compute in (Aone ?1) In
(Match Context With
| [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2].
Tactic Definition ApplyMultiply FT lvar trm :=
Cut (interp_ExprA FT lvar (multiply trm))==(interp_ExprA FT lvar trm);
[Intro;
(Match Context With
| [id:(interp_ExprA ?1 ?2 (multiply ?3))== ?4 |- ?] ->
Let t=Eval Compute in (multiply ?3) In
Change (interp_ExprA ?1 ?2 t)== ?4 in id;Try (Rewrite <- id);Clear id)
|Apply multiply_correct].
(**** Permutations and simplification ****)
Tactic Definition ApplyInverse mul FT lvar trm :=
Cut (interp_ExprA FT lvar (inverse_simplif mul trm))==
(interp_ExprA FT lvar trm);
[Intro;
(Match Context With
| [id:(interp_ExprA ?1 ?2 (inverse_simplif ?3 ?4))== ?5 |- ?] ->
Let t=Eval Compute in (inverse_simplif ?3 ?4) In
Change (interp_ExprA ?1 ?2 t)== ?5 in id;Try (Rewrite <- id);Clear id)
|Apply inverse_correct;Assumption].
(**** Inverse test ****)
Tactic Definition StrongFail tac := First [tac|Fail 2].
Tactic Definition InverseTestAux FT trm :=
Let AplusT = Eval Compute in (Aplus FT)
And AmultT = Eval Compute in (Amult FT)
And AoppT = Eval Compute in (Aopp FT)
And AinvT = Eval Compute in (Ainv FT) In
Match trm With
| [(AinvT ?)] -> Fail 1
| [(AoppT ?1)] -> StrongFail (InverseTestAux FT ?1)
| [(AplusT ?1 ?2)] ->
StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
| [(AmultT ?1 ?2)] ->
StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
| _ -> Idtac.
Tactic Definition InverseTest FT :=
Let AplusT = Eval Compute in (Aplus FT) In
Match Context With
| [|- ?1==?2] -> (InverseTestAux FT '(AplusT ?1 ?2)).
(**** Field itself ****)
Tactic Definition ApplySimplif sfun :=
(Match Context With
| [|- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ? ?)] ->
(sfun ?1 ?2 ?3));
(Match Context With
| [|- (interp_ExprA ? ? ?)==(interp_ExprA ?1 ?2 ?3)] ->
(sfun ?1 ?2 ?3)).
Tactic Definition Unfolds FT :=
(Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With
| [(Some ? ?1)] -> Unfold ?1
| _ -> Idtac);
(Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
| [(Some ? ?1)] -> Unfold ?1
| _ -> Idtac).
Tactic Definition Field_Gen FT :=
Let AplusT = Eval Compute in (Aplus FT) In
Unfolds FT;
Match Context With
| [|- ?1==?2] ->
Let lvar = (BuildVarList FT '(AplusT ?1 ?2)) In
Let trm1 = (interp_A FT lvar ?1)
And trm2 = (interp_A FT lvar ?2) In
Let mul = (GiveMult '(EAplus trm1 trm2)) In
Cut [ft:=FT][vm:=lvar](interp_ExprA ft vm trm1)==(interp_ExprA ft vm trm2);
[Compute;Auto
|Intros;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
(Multiply mul);[(ApplySimplif ApplyMultiply);
(ApplySimplif (ApplyInverse mul));
(Let id = GrepMult In Clear id);Compute;
First [(InverseTest FT);Ring|Clear ft vm;(Field_Gen FT)]|Idtac]].
|
