← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/setoid_ring/Field_tac.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/setoid_ring/Field_tac.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
Require Import Ring_tac BinList Ring_polynom InitialRing.
 
10
Require Export Field_theory.
 
11
 
 
12
 (* syntaxification *)
 
13
 Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := 
 
14
 let rec mkP t :=
 
15
    match Cst t with
 
16
    | InitialRing.NotConstant =>
 
17
        match t with 
 
18
        | (radd ?t1 ?t2) => 
 
19
          let e1 := mkP t1 in
 
20
          let e2 := mkP t2 in constr:(FEadd e1 e2)
 
21
        | (rmul ?t1 ?t2) => 
 
22
          let e1 := mkP t1 in
 
23
          let e2 := mkP t2 in constr:(FEmul e1 e2)
 
24
        | (rsub ?t1 ?t2) => 
 
25
          let e1 := mkP t1 in
 
26
          let e2 := mkP t2 in constr:(FEsub e1 e2)
 
27
        | (ropp ?t1) =>
 
28
          let e1 := mkP t1 in constr:(FEopp e1)
 
29
        | (rdiv ?t1 ?t2) => 
 
30
          let e1 := mkP t1 in
 
31
          let e2 := mkP t2 in constr:(FEdiv e1 e2)
 
32
        | (rinv ?t1) =>
 
33
          let e1 := mkP t1 in constr:(FEinv e1)
 
34
        | (rpow ?t1 ?n) =>
 
35
          match CstPow n with
 
36
          | InitialRing.NotConstant => 
 
37
            let p := Find_at t fv in constr:(@FEX C p)
 
38
          | ?c => let e1 := mkP t1 in constr:(FEpow e1 c)
 
39
          end
 
40
  
 
41
        | _ =>
 
42
          let p := Find_at t fv in constr:(@FEX C p)
 
43
        end
 
44
    | ?c => constr:(FEc c)
 
45
    end
 
46
 in mkP t.
 
47
 
 
48
Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
 
49
 let rec TFV t fv :=
 
50
  match Cst t with
 
51
  | InitialRing.NotConstant =>
 
52
      match t with
 
53
      | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
 
54
      | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
 
55
      | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
 
56
      | (opp ?t1) => TFV t1 fv
 
57
      | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
 
58
      | (inv ?t1) => TFV t1 fv
 
59
      | (pow ?t1 ?n) =>
 
60
        match CstPow n with
 
61
        | InitialRing.NotConstant => AddFvTail t fv
 
62
        | _ => TFV t1 fv
 
63
        end
 
64
      | _ => AddFvTail t fv
 
65
      end
 
66
  | _ => fv
 
67
  end 
 
68
 in TFV t fv.
 
69
 
 
70
Ltac ParseFieldComponents lemma req :=
 
71
  match type of lemma with
 
72
  | context [
 
73
     (*   PCond _ _ _  _ _ _ _  _ _  _ _ -> *)
 
74
        req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv 
 
75
                          ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
 
76
      (fun f => f radd rmul rsub ropp rdiv rinv rpow C)
 
77
  | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
 
78
  end.
 
79
 
 
80
(* simplifying the non-zero condition... *)
 
81
 
 
82
Ltac fold_field_cond req :=
 
83
  let rec fold_concl t :=
 
84
    match t with
 
85
      ?x /\ ?y =>
 
86
        let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy)
 
87
    | req ?x ?y -> False => constr:(~ req x y)
 
88
    | _ => t
 
89
    end in
 
90
  match goal with
 
91
    |- ?t => let ft := fold_concl t in change ft
 
92
  end.
 
93
 
 
94
Ltac simpl_PCond req :=
 
95
  protect_fv "field_cond";
 
96
  (try exact I);
 
97
  fold_field_cond req.
 
98
 
 
99
Ltac simpl_PCond_BEURK req :=
 
100
  protect_fv "field_cond";
 
101
  fold_field_cond req.
 
102
 
 
103
(* Rewriting (field_simplify) *)
 
104
Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl :=
 
105
  let Main radd rmul rsub ropp rdiv rinv rpow C :=
 
106
    let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
107
    let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
108
    let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
109
    let mkFE := 
 
110
       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
111
    let fv := FV_hypo_tac mkFV req lH in
 
112
    let simpl_field H := (protect_fv "field" in H;f H) in
 
113
    let lemma_tac fv RW_tac :=
 
114
      let rr_lemma := fresh "f_rw_lemma" in
 
115
      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
 
116
      let vlpe := fresh "list_hyp" in
 
117
      let vlmp := fresh "list_hyp_norm" in
 
118
      let vlmp_eq := fresh "list_hyp_norm_eq" in
 
119
      let prh := proofHyp_tac lH in
 
120
      pose (vlpe := lpe);
 
121
      match type of lemma with
 
122
      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] =>
 
123
        compute_assertion vlmp_eq vlmp 
 
124
            (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
 
125
         (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq)
 
126
          || fail 1 "type error when build the rewriting lemma");
 
127
         RW_tac rr_lemma;
 
128
        try clear rr_lemma vlmp_eq vlmp vlpe
 
129
      | _ => fail 1 "field_simplify anomaly: bad correctness lemma"
 
130
      end in
 
131
    ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl;
 
132
    try (apply Cond_lemma; simpl_PCond req) in
 
133
  ParseFieldComponents lemma req Main.
 
134
 
 
135
Ltac Field_simplify_gen f := 
 
136
     fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl =>
 
137
       pre(); 
 
138
       Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req 
 
139
                  ring_subst_niter lH rl; 
 
140
      post().
 
141
 
 
142
Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
 
143
 
 
144
Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
 
145
  let G := Get_goal in
 
146
  field_lookup Field_simplify [] rl G.
 
147
 
 
148
Tactic Notation (at level 0) 
 
149
  "field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
 
150
  let G := Get_goal in
 
151
  field_lookup Field_simplify [lH] rl G.
 
152
 
 
153
Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=   
 
154
  let G := Get_goal in
 
155
  let t := type of H in   
 
156
  let g := fresh "goal" in
 
157
  set (g:= G);
 
158
  generalize H;clear H;
 
159
  field_lookup Field_simplify [] rl t;
 
160
  intro H;
 
161
  unfold g;clear g.
 
162
 
 
163
Tactic Notation "field_simplify" 
 
164
    "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=   
 
165
  let G := Get_goal in
 
166
  let t := type of H in   
 
167
  let g := fresh "goal" in
 
168
  set (g:= G);
 
169
  generalize H;clear H;
 
170
  field_lookup Field_simplify [lH] rl t;
 
171
  intro H;
 
172
  unfold g;clear g.
 
173
 
 
174
(*
 
175
Ltac Field_simplify_in hyp:= 
 
176
   Field_simplify_gen ltac:(fun H => rewrite H in hyp).
 
177
 
 
178
Tactic Notation (at level 0) 
 
179
  "field_simplify" constr_list(rl) "in" hyp(h) :=
 
180
  let t := type of h in
 
181
  field_lookup (Field_simplify_in h) [] rl t.
 
182
 
 
183
Tactic Notation (at level 0) 
 
184
  "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
 
185
  let t := type of h in
 
186
  field_lookup (Field_simplify_in h) [lH] rl t.
 
187
*)
 
188
 
 
189
(** Generic tactic for solving equations *)
 
190
 
 
191
Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
 
192
  let Main radd rmul rsub ropp rdiv rinv rpow C :=
 
193
    let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
194
    let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
195
    let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
196
    let mkFE := 
 
197
       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
198
    let rec ParseExpr ilemma :=
 
199
      match type of ilemma with
 
200
        forall nfe, ?fe = nfe -> _ =>
 
201
          (fun t => 
 
202
            let x := fresh "fld_expr" in 
 
203
            let H := fresh "norm_fld_expr" in
 
204
            compute_assertion H x fe;
 
205
            ParseExpr (ilemma x H) t;
 
206
            try clear x H)
 
207
      | _ => (fun t => t ilemma)
 
208
      end in
 
209
    let Main_eq t1 t2 :=
 
210
      let fv := FV_hypo_tac mkFV req lH in
 
211
      let fv := mkFFV t1 fv in
 
212
      let fv := mkFFV t2 fv in
 
213
      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
 
214
      let prh := proofHyp_tac lH in
 
215
      let vlpe := fresh "list_hyp" in
 
216
      let fe1 := mkFE t1 fv in
 
217
      let fe2 := mkFE t2 fv in
 
218
      pose (vlpe := lpe);
 
219
      let nlemma := fresh "field_lemma" in
 
220
      (assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
 
221
       || fail "field anomaly:failed to build lemma"); 
 
222
      ParseExpr nlemma
 
223
         ltac:(fun ilemma =>
 
224
                  apply ilemma 
 
225
                  || fail "field anomaly: failed in applying lemma";
 
226
                  [ Simpl_tac | apply Cond_lemma; simpl_PCond req]);
 
227
      clear vlpe nlemma in
 
228
    OnEquation req Main_eq in
 
229
  ParseFieldComponents lemma req Main.
 
230
 
 
231
(* solve completely a field equation, leaving non-zero conditions to be
 
232
   proved (field) *)
 
233
 
 
234
Ltac FIELD :=
 
235
   let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
 
236
   fun req cst_tac pow_tac field_ok _ _ _ cond_ok pre post lH rl =>
 
237
       pre(); 
 
238
       Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req 
 
239
         Ring_tac.ring_subst_niter lH;
 
240
       try exact I;
 
241
       post().
 
242
 
 
243
Tactic Notation (at level 0) "field" :=
 
244
  let G := Get_goal in
 
245
  field_lookup FIELD [] G.
 
246
 
 
247
Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
 
248
  let G := Get_goal in
 
249
  field_lookup FIELD [lH] G.
 
250
 
 
251
(* transforms a field equation to an equivalent (simplified) ring equation,
 
252
   and leaves non-zero conditions to be proved (field_simplify_eq) *)
 
253
Ltac FIELD_SIMPL  :=
 
254
  let Simpl := (protect_fv "field") in
 
255
  fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl =>
 
256
       pre(); 
 
257
       Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok 
 
258
          req Ring_tac.ring_subst_niter lH;
 
259
       post().
 
260
 
 
261
Tactic Notation (at level 0) "field_simplify_eq" :=  
 
262
  let G := Get_goal in
 
263
  field_lookup FIELD_SIMPL [] G.
 
264
 
 
265
Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=  
 
266
  let G := Get_goal in
 
267
  field_lookup FIELD_SIMPL [lH] G.
 
268
 
 
269
(* Same as FIELD_SIMPL but in hypothesis *)
 
270
 
 
271
Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH :=
 
272
   let Main radd rmul rsub ropp rdiv rinv rpow C :=
 
273
    let hyp := fresh "hyp" in
 
274
    intro hyp;   
 
275
    match type of hyp with
 
276
    | req ?t1 ?t2 =>
 
277
      let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
278
      let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
 
279
      let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
280
      let mkFE := 
 
281
        mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
 
282
      let rec ParseExpr ilemma :=
 
283
        match type of ilemma with
 
284
        |  forall nfe, ?fe = nfe -> _ =>
 
285
          (fun t => 
 
286
            let x := fresh "fld_expr" in 
 
287
            let H := fresh "norm_fld_expr" in
 
288
            compute_assertion H x fe;
 
289
            ParseExpr (ilemma x H) t;
 
290
            try clear H x)
 
291
        | _ => (fun t => t ilemma)
 
292
        end in
 
293
      let fv := FV_hypo_tac mkFV req lH in
 
294
      let fv := mkFFV t1 fv in
 
295
      let fv := mkFFV t2 fv in
 
296
      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
 
297
      let prh := proofHyp_tac lH in
 
298
      let fe1 := mkFE t1 fv in
 
299
      let fe2 := mkFE t2 fv in
 
300
      let vlpe := fresh "vlpe" in
 
301
      ParseExpr (lemma n fv lpe fe1 fe2 prh)
 
302
         ltac:(fun ilemma =>
 
303
             match type of ilemma with
 
304
             | req _ _ ->  _ -> ?EQ => 
 
305
               let tmp := fresh "tmp" in
 
306
               assert (tmp : EQ);
 
307
               [ apply ilemma; 
 
308
                 [ exact hyp | apply Cond_lemma; simpl_PCond_BEURK req]
 
309
               | protect_fv "field" in tmp;
 
310
                 generalize tmp;clear tmp ];
 
311
               clear hyp  
 
312
             end)
 
313
     end in
 
314
  ParseFieldComponents lemma req Main.
 
315
 
 
316
Ltac FIELD_SIMPL_EQ :=
 
317
 fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl =>
 
318
       pre(); 
 
319
       Field_simplify_eq cst_tac pow_tac lemma cond_ok req
 
320
         Ring_tac.ring_subst_niter lH;
 
321
       post().
 
322
 
 
323
Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
 
324
  let t := type of H in
 
325
  generalize H;
 
326
  field_lookup FIELD_SIMPL_EQ [] t;
 
327
  [ try exact I
 
328
  | clear H;intro H].
 
329
 
 
330
 
 
331
Tactic Notation (at level 0) 
 
332
  "field_simplify_eq" "[" constr_list(lH) "]"  "in" hyp(H) :=  
 
333
  let t := type of H in
 
334
  generalize H;
 
335
  field_lookup FIELD_SIMPL_EQ [lH] t;
 
336
  [ try exact I
 
337
  |clear H;intro H].
 
338
 
 
339
(* Adding a new field *)
 
340
 
 
341
Ltac ring_of_field f :=
 
342
  match type of f with
 
343
  | almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f)
 
344
  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f)
 
345
  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f)
 
346
  end.
 
347
 
 
348
Ltac coerce_to_almost_field set ext f :=
 
349
  match type of f with
 
350
  | almost_field_theory _ _ _ _ _ _ _ _ _ => f
 
351
  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f)
 
352
  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
 
353
  end.
 
354
 
 
355
Ltac field_elements set ext fspec pspec sspec dspec rk :=
 
356
  let afth := coerce_to_almost_field set ext fspec in
 
357
  let rspec := ring_of_field fspec in
 
358
  ring_elements set ext rspec pspec sspec dspec rk
 
359
  ltac:(fun arth ext_r morph p_spec s_spec d_spec f => f afth ext_r morph p_spec s_spec d_spec).
 
360
 
 
361
Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
 
362
  let get_lemma :=
 
363
    match pspec with None => fun x y => x | _ => fun x y => y end in
 
364
  let simpl_eq_lemma := get_lemma 
 
365
       Field_simplify_eq_correct       Field_simplify_eq_pow_correct in
 
366
  let simpl_eq_in_lemma := get_lemma
 
367
       Field_simplify_eq_in_correct   Field_simplify_eq_pow_in_correct in
 
368
  let rw_lemma := get_lemma
 
369
       Field_rw_correct                    Field_rw_pow_correct in
 
370
  field_elements set ext fspec pspec sspec dspec rk
 
371
   ltac:(fun afth ext_r morph p_spec s_spec d_spec =>
 
372
     match morph with
 
373
     | _ =>
 
374
       let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in
 
375
       match p_spec with
 
376
       | mkhypo ?pp_spec =>  
 
377
         let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
 
378
         match s_spec with
 
379
         | mkhypo ?ss_spec => 
 
380
           let field_ok3 := constr:(field_ok2 _ ss_spec) in
 
381
           match d_spec with
 
382
           | mkhypo ?dd_spec => 
 
383
             let field_ok := constr:(field_ok3 _ dd_spec) in
 
384
             let mk_lemma lemma :=     
 
385
              constr:(lemma _ _ _  _ _ _  _ _ _ _ 
 
386
                   set ext_r inv_m afth 
 
387
                   _ _ _  _ _ _  _ _ _ morph 
 
388
                   _ _ _ pp_spec _ ss_spec _ dd_spec) in 
 
389
             let field_simpl_eq_ok := mk_lemma simpl_eq_lemma  in
 
390
             let field_simpl_ok := mk_lemma rw_lemma in
 
391
             let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in
 
392
             let cond1_ok := 
 
393
                constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in
 
394
             let cond2_ok := 
 
395
               constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in
 
396
             (fun f => 
 
397
               f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
 
398
                  cond1_ok cond2_ok)
 
399
           | _ => fail 4 "field: bad coefficiant division specification"
 
400
           end
 
401
         | _ => fail 3 "field: bad sign specification"
 
402
         end
 
403
       | _ => fail 2 "field: bad power specification"
 
404
       end  
 
405
     | _ => fail 1 "field internal error : field_lemmas, please report"
 
406
     end).