← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/field/LegacyField_Tactic.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/field/LegacyField_Tactic.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: LegacyField_Tactic.v 9319 2006-10-30 12:41:21Z barras $ *)
 
10
 
 
11
Require Import List.
 
12
Require Import LegacyRing.
 
13
Require Export LegacyField_Compl.
 
14
Require Export LegacyField_Theory.
 
15
 
 
16
(**** Interpretation A --> ExprA ****)
 
17
 
 
18
Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
 
19
 
 
20
Ltac body_of s := eval cbv beta iota delta [s] in s.
 
21
 
 
22
Ltac mem_assoc var lvar :=
 
23
  match constr:lvar with
 
24
  | nil => constr:false
 
25
  | ?X1 :: ?X2 =>
 
26
      match constr:(X1 = var) with
 
27
      | (?X1 = ?X1) => constr:true
 
28
      | _ => mem_assoc var X2
 
29
      end
 
30
  end.
 
31
 
 
32
Ltac number lvar := 
 
33
  let rec number_aux lvar cpt :=
 
34
    match constr:lvar with
 
35
    | (@nil ?X1) => constr:(@nil (prod X1 nat))
 
36
    | ?X2 :: ?X3 =>
 
37
        let l2 := number_aux X3 (S cpt) in
 
38
        constr:((X2,cpt) :: l2) 
 
39
    end
 
40
  in number_aux lvar 0.
 
41
 
 
42
Ltac build_varlist FT trm := 
 
43
  let rec seek_var lvar trm :=
 
44
    let AT := get_component A FT
 
45
    with AzeroT := get_component Azero FT
 
46
    with AoneT := get_component Aone FT
 
47
    with AplusT := get_component Aplus FT
 
48
    with AmultT := get_component Amult FT
 
49
    with AoppT := get_component Aopp FT
 
50
    with AinvT := get_component Ainv FT in
 
51
    match constr:trm with
 
52
    | AzeroT => lvar
 
53
    | AoneT => lvar
 
54
    | (AplusT ?X1 ?X2) =>
 
55
        let l1 := seek_var lvar X1 in
 
56
        seek_var l1 X2
 
57
    | (AmultT ?X1 ?X2) =>
 
58
        let l1 := seek_var lvar X1 in
 
59
        seek_var l1 X2
 
60
    | (AoppT ?X1) => seek_var lvar X1
 
61
    | (AinvT ?X1) => seek_var lvar X1
 
62
    | ?X1 =>
 
63
        let res := mem_assoc X1 lvar in
 
64
        match constr:res with
 
65
        | true => lvar
 
66
        | false => constr:(X1 :: lvar)
 
67
        end
 
68
    end in
 
69
  let AT := get_component A FT in
 
70
  let lvar := seek_var (@nil AT) trm in
 
71
  number lvar.
 
72
 
 
73
Ltac assoc elt lst :=
 
74
  match constr:lst with
 
75
  | nil => fail
 
76
  | (?X1,?X2) :: ?X3 =>
 
77
      match constr:(elt = X1) with
 
78
      | (?X1 = ?X1) => constr:X2
 
79
      | _ => assoc elt X3
 
80
      end
 
81
  end.
 
82
 
 
83
Ltac interp_A FT lvar trm :=
 
84
  let AT := get_component A FT
 
85
  with AzeroT := get_component Azero FT
 
86
  with AoneT := get_component Aone FT
 
87
  with AplusT := get_component Aplus FT
 
88
  with AmultT := get_component Amult FT
 
89
  with AoppT := get_component Aopp FT
 
90
  with AinvT := get_component Ainv FT in
 
91
  match constr:trm with
 
92
  | AzeroT => constr:EAzero
 
93
  | AoneT => constr:EAone
 
94
  | (AplusT ?X1 ?X2) =>
 
95
      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
 
96
      constr:(EAplus e1 e2)
 
97
  | (AmultT ?X1 ?X2) =>
 
98
      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
 
99
      constr:(EAmult e1 e2)
 
100
  | (AoppT ?X1) =>
 
101
      let e := interp_A FT lvar X1 in
 
102
      constr:(EAopp e)
 
103
  | (AinvT ?X1) => let e := interp_A FT lvar X1 in
 
104
                   constr:(EAinv e)
 
105
  | ?X1 => let idx := assoc X1 lvar in
 
106
           constr:(EAvar idx)
 
107
  end.
 
108
 
 
109
(************************)
 
110
(*    Simplification    *)
 
111
(************************)
 
112
 
 
113
(**** Generation of the multiplier ****)
 
114
 
 
115
Ltac remove e l :=
 
116
  match constr:l with
 
117
  | nil => l
 
118
  | e :: ?X2 => constr:X2
 
119
  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
 
120
  end.
 
121
 
 
122
Ltac union l1 l2 :=
 
123
  match constr:l1 with
 
124
  | nil => l2
 
125
  | ?X2 :: ?X3 =>
 
126
      let nl2 := remove X2 l2 in
 
127
      let nl := union X3 nl2 in
 
128
      constr:(X2 :: nl)
 
129
  end.
 
130
 
 
131
Ltac raw_give_mult trm :=
 
132
  match constr:trm with
 
133
  | (EAinv ?X1) => constr:(X1 :: nil)
 
134
  | (EAopp ?X1) => raw_give_mult X1
 
135
  | (EAplus ?X1 ?X2) =>
 
136
      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
 
137
      union l1 l2
 
138
  | (EAmult ?X1 ?X2) =>
 
139
      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
 
140
      eval compute in (app l1 l2)
 
141
  | _ => constr:(@nil ExprA)
 
142
  end.
 
143
 
 
144
Ltac give_mult trm :=
 
145
  let ltrm := raw_give_mult trm in
 
146
  constr:(mult_of_list ltrm).
 
147
 
 
148
(**** Associativity ****)
 
149
 
 
150
Ltac apply_assoc FT lvar trm :=
 
151
  let t := eval compute in (assoc trm) in
 
152
  match constr:(t = trm) with
 
153
  | (?X1 = ?X1) => idtac
 
154
  | _ =>
 
155
      rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- *
 
156
  end.
 
157
 
 
158
(**** Distribution *****)
 
159
 
 
160
Ltac apply_distrib FT lvar trm :=
 
161
  let t := eval compute in (distrib trm) in
 
162
  match constr:(t = trm) with
 
163
  | (?X1 = ?X1) => idtac
 
164
  | _ =>
 
165
      rewrite <- (distrib_correct FT trm);
 
166
       change (distrib trm) with t in |- *
 
167
  end.
 
168
 
 
169
(**** Multiplication by the inverse product ****)
 
170
 
 
171
Ltac grep_mult := match goal with
 
172
                  | id:(interp_ExprA _ _ _ <> _) |- _ => id
 
173
                  end.
 
174
 
 
175
Ltac weak_reduce :=
 
176
  match goal with
 
177
  |  |- context [(interp_ExprA ?X1 ?X2 _)] =>
 
178
      cbv beta iota zeta
 
179
       delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
 
180
             Aone Aplus Amult Aopp Ainv] in |- *
 
181
  end.
 
182
 
 
183
Ltac multiply mul :=
 
184
  match goal with
 
185
  |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
 
186
      let AzeroT := get_component Azero FT in
 
187
      cut (interp_ExprA FT X2 mul <> AzeroT);
 
188
       [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
 
189
       | weak_reduce;
 
190
          (let AoneT := get_component Aone ltac:(body_of FT)
 
191
           with AmultT := get_component Amult ltac:(body_of FT) in
 
192
           try
 
193
             match goal with
 
194
             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
 
195
             end; clear FT X2) ]
 
196
  end.
 
197
 
 
198
Ltac apply_multiply FT lvar trm :=
 
199
  let t := eval compute in (multiply trm) in
 
200
  match constr:(t = trm) with
 
201
  | (?X1 = ?X1) => idtac
 
202
  | _ =>
 
203
      rewrite <- (multiply_correct FT trm);
 
204
       change (multiply trm) with t in |- *
 
205
  end.
 
206
 
 
207
(**** Permutations and simplification ****)
 
208
 
 
209
Ltac apply_inverse mul FT lvar trm :=
 
210
  let t := eval compute in (inverse_simplif mul trm) in
 
211
  match constr:(t = trm) with
 
212
  | (?X1 = ?X1) => idtac
 
213
  | _ =>
 
214
      rewrite <- (inverse_correct FT trm mul);
 
215
       [ change (inverse_simplif mul trm) with t in |- * | assumption ]
 
216
  end.
 
217
(**** Inverse test ****)
 
218
 
 
219
Ltac strong_fail tac := first [ tac | fail 2 ].
 
220
 
 
221
Ltac inverse_test_aux FT trm :=
 
222
  let AplusT := get_component Aplus FT
 
223
  with AmultT := get_component Amult FT
 
224
  with AoppT := get_component Aopp FT
 
225
  with AinvT := get_component Ainv FT in
 
226
  match constr:trm with
 
227
  | (AinvT _) => fail 1
 
228
  | (AoppT ?X1) =>
 
229
      strong_fail ltac:(inverse_test_aux FT X1; idtac)
 
230
  | (AplusT ?X1 ?X2) =>
 
231
      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
 
232
  | (AmultT ?X1 ?X2) =>
 
233
      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
 
234
  | _ => idtac
 
235
  end.
 
236
 
 
237
Ltac inverse_test FT :=
 
238
  let AplusT := get_component Aplus FT in
 
239
  match goal with
 
240
  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
 
241
  end.
 
242
 
 
243
(**** Field itself ****)
 
244
 
 
245
Ltac apply_simplif sfun :=
 
246
  match goal with
 
247
  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) => 
 
248
  sfun X1 X2 X3
 
249
  end;
 
250
   match goal with
 
251
   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) => 
 
252
   sfun X1 X2 X3
 
253
   end.
 
254
 
 
255
Ltac unfolds FT :=
 
256
  match get_component Aminus FT with
 
257
  | Some ?X1 => unfold X1 in |- *
 
258
  | _ => idtac
 
259
  end;
 
260
  match get_component Adiv FT with
 
261
  | Some ?X1 => unfold X1 in |- *
 
262
  | _ => idtac
 
263
  end.
 
264
 
 
265
Ltac reduce FT :=
 
266
  let AzeroT := get_component Azero FT
 
267
  with AoneT := get_component Aone FT
 
268
  with AplusT := get_component Aplus FT
 
269
  with AmultT := get_component Amult FT
 
270
  with AoppT := get_component Aopp FT
 
271
  with AinvT := get_component Ainv FT in
 
272
  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
 
273
     compute in |- *).
 
274
 
 
275
Ltac field_gen_aux FT :=
 
276
  let AplusT := get_component Aplus FT in
 
277
  match goal with
 
278
  |  |- (?X1 = ?X2) =>
 
279
      let lvar := build_varlist FT (AplusT X1 X2) in
 
280
      let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
 
281
      let mul := give_mult (EAplus trm1 trm2) in
 
282
      cut
 
283
        (let ft := FT in
 
284
         let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
 
285
        [ compute in |- *; auto
 
286
        | intros ft vm; apply_simplif apply_distrib;
 
287
           apply_simplif apply_assoc; multiply mul;
 
288
           [ apply_simplif apply_multiply;
 
289
              apply_simplif ltac:(apply_inverse mul);
 
290
              (let id := grep_mult in
 
291
               clear id; weak_reduce; clear ft vm; first
 
292
              [ inverse_test FT; legacy ring | field_gen_aux FT ])
 
293
           | idtac ] ]
 
294
  end.
 
295
 
 
296
Ltac field_gen FT :=
 
297
  unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
 
298
 
 
299
(*****************************)
 
300
(*    Term Simplification    *)
 
301
(*****************************)
 
302
 
 
303
(**** Minus and division expansions ****)
 
304
 
 
305
Ltac init_exp FT trm :=
 
306
  let e :=
 
307
   (match get_component Aminus FT with
 
308
    | Some ?X1 => eval cbv beta delta [X1] in trm
 
309
    | _ => trm
 
310
    end) in
 
311
  match get_component Adiv FT with
 
312
  | Some ?X1 => eval cbv beta delta [X1] in e
 
313
  | _ => e
 
314
  end.
 
315
 
 
316
(**** Inverses simplification ****)
 
317
 
 
318
Ltac simpl_inv trm :=
 
319
  match constr:trm with
 
320
  | (EAplus ?X1 ?X2) =>
 
321
      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
 
322
      constr:(EAplus e1 e2)
 
323
  | (EAmult ?X1 ?X2) =>
 
324
      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
 
325
      constr:(EAmult e1 e2)
 
326
  | (EAopp ?X1) => let e := simpl_inv X1 in
 
327
                   constr:(EAopp e)
 
328
  | (EAinv ?X1) => SimplInvAux X1
 
329
  | ?X1 => constr:X1
 
330
  end
 
331
 with SimplInvAux trm :=
 
332
  match constr:trm with
 
333
  | (EAinv ?X1) => simpl_inv X1
 
334
  | (EAmult ?X1 ?X2) =>
 
335
      let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
 
336
      constr:(EAmult e1 e2)
 
337
  | ?X1 => let e := simpl_inv X1 in
 
338
           constr:(EAinv e)
 
339
  end.
 
340
 
 
341
(**** Monom simplification ****)
 
342
 
 
343
Ltac map_tactic fcn lst :=
 
344
  match constr:lst with
 
345
  | nil => lst
 
346
  | ?X2 :: ?X3 =>
 
347
      let r := fcn X2 with t := map_tactic fcn X3 in
 
348
      constr:(r :: t)
 
349
  end.
 
350
 
 
351
Ltac build_monom_aux lst trm :=
 
352
  match constr:lst with
 
353
  | nil => eval compute in (assoc trm)
 
354
  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
 
355
  end.
 
356
 
 
357
Ltac build_monom lnum lden :=
 
358
  let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
 
359
  let ltot := eval compute in (app lnum ildn) in
 
360
  let trm := build_monom_aux ltot EAone in
 
361
  match constr:trm with
 
362
  | (EAmult _ ?X1) => constr:X1
 
363
  | ?X1 => constr:X1
 
364
  end.
 
365
 
 
366
Ltac simpl_monom_aux lnum lden trm :=
 
367
  match constr:trm with
 
368
  | (EAmult (EAinv ?X1) ?X2) =>
 
369
      let mma := mem_assoc X1 lnum in
 
370
      match constr:mma with
 
371
      | true =>
 
372
          let newlnum := remove X1 lnum in
 
373
          simpl_monom_aux newlnum lden X2
 
374
      | false => simpl_monom_aux lnum (X1 :: lden) X2
 
375
      end
 
376
  | (EAmult ?X1 ?X2) =>
 
377
      let mma := mem_assoc X1 lden in
 
378
      match constr:mma with
 
379
      | true =>
 
380
          let newlden := remove X1 lden in
 
381
          simpl_monom_aux lnum newlden X2
 
382
      | false => simpl_monom_aux (X1 :: lnum) lden X2
 
383
      end
 
384
  | (EAinv ?X1) =>
 
385
      let mma := mem_assoc X1 lnum in
 
386
      match constr:mma with
 
387
      | true =>
 
388
          let newlnum := remove X1 lnum in
 
389
          build_monom newlnum lden
 
390
      | false => build_monom lnum (X1 :: lden)
 
391
      end
 
392
  | ?X1 =>
 
393
      let mma := mem_assoc X1 lden in
 
394
      match constr:mma with
 
395
      | true =>
 
396
          let newlden := remove X1 lden in
 
397
          build_monom lnum newlden
 
398
      | false => build_monom (X1 :: lnum) lden
 
399
      end
 
400
  end.
 
401
 
 
402
Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
 
403
 
 
404
Ltac simpl_all_monomials trm :=
 
405
  match constr:trm with
 
406
  | (EAplus ?X1 ?X2) =>
 
407
      let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
 
408
      constr:(EAplus e1 e2)
 
409
  | ?X1 => simpl_monom X1
 
410
  end.
 
411
 
 
412
(**** Associativity and distribution ****)
 
413
 
 
414
Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
 
415
 
 
416
(**** The tactic Field_Term ****)
 
417
 
 
418
Ltac eval_weak_reduce trm :=
 
419
  eval
 
420
   cbv beta iota zeta
 
421
    delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
 
422
          Amult Aopp Ainv] in trm.
 
423
 
 
424
Ltac field_term FT exp :=
 
425
  let newexp := init_exp FT exp in
 
426
  let lvar := build_varlist FT newexp in
 
427
  let trm := interp_A FT lvar newexp in
 
428
  let tma := eval compute in (assoc trm) in
 
429
  let tsmp :=
 
430
   simpl_all_monomials
 
431
    ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
 
432
  let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
 
433
  (replace exp with trep; [ legacy ring trep | field_gen FT ]).