summaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Field_tac.v
blob: eee89e61c55bbdd7a60a1e8b9ee447bac23626f7 (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
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Require Import Ring_tac BinList Ring_polynom InitialRing.
Require Export Field_theory.

 (* syntaxification *)
 Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv :=
 let rec mkP t :=
    let f :=
    match Cst t with
    | InitialRing.NotConstant =>
        match t with
        | (radd ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(FEadd e1 e2)
        | (rmul ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(FEmul e1 e2)
        | (rsub ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(FEsub e1 e2)
        | (ropp ?t1) =>
          fun _ => let e1 := mkP t1 in constr:(FEopp e1)
        | (rdiv ?t1 ?t2) =>
          fun _ =>
          let e1 := mkP t1 in
          let e2 := mkP t2 in constr:(FEdiv e1 e2)
        | (rinv ?t1) =>
          fun _ => let e1 := mkP t1 in constr:(FEinv e1)
        | (rpow ?t1 ?n) =>
          match CstPow n with
          | InitialRing.NotConstant =>
            fun _ =>
            let p := Find_at t fv in
            constr:(@FEX C p)
          | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c)
          end
        | _ =>
          fun _ =>
          let p := Find_at t fv in
          constr:(@FEX C p)
        end
    | ?c => fun _ => constr:(FEc c)
    end in
    f ()
 in mkP t.

Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
 let rec TFV t fv :=
  match Cst t with
  | InitialRing.NotConstant =>
      match t with
      | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
      | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
      | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
      | (opp ?t1) => TFV t1 fv
      | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
      | (inv ?t1) => TFV t1 fv
      | (pow ?t1 ?n) =>
        match CstPow n with
        | InitialRing.NotConstant =>
            AddFvTail t fv
        | _ => TFV t1 fv
        end
      | _ => AddFvTail t fv
      end
  | _ => fv
  end
 in TFV t fv.

(* packaging the field structure *)

(* TODO: inline PackField into field_lookup *)
Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
  let FLD :=
    match type of L1 with
    | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv
                                      ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
        (fun proj =>
           proj Cst_tac Pow_tac pre post
             req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
    | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
    end in
  F FLD.

Ltac get_FldPre FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       pre).

Ltac get_FldPost FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       post).

Ltac get_L1 FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       L1).

Ltac get_SimplifyEqLemma FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       L2).

Ltac get_SimplifyLemma FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       L3).

Ltac get_L4 FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       L4).

Ltac get_CondLemma FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       cond_ok).

Ltac get_FldEq FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       req).

Ltac get_FldCarrier FLD :=
  let req := get_FldEq FLD in
  relation_carrier req.

Ltac get_RingFV FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       FV Cst_tac Pow_tac radd rmul rsub ropp rpow).

Ltac get_FFV FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).

Ltac get_RingMeta FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow).

Ltac get_Meta FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).

Ltac get_Hyp_tac FLD :=
  FLD ltac:
      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
           L1 L2 L3 L4 cond_ok =>
       let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
       fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).

Ltac get_FEeval FLD :=
  let L1 := get_L1 FLD in
  match type of L1 with
  | context
    [(@FEeval
      ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
       constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow)
  | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
  end.

(* simplifying the non-zero condition... *)

Ltac fold_field_cond req :=
  let rec fold_concl t :=
    match t with
      ?x /\ ?y =>
        let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy)
    | req ?x ?y -> False => constr:(~ req x y)
    | _ => t
    end in
  let ft := fold_concl Get_goal in
  change ft.

Ltac simpl_PCond FLD :=
  let req := get_FldEq FLD in
  let lemma := get_CondLemma FLD in
  try apply lemma;
  protect_fv "field_cond";
  fold_field_cond req;
  try exact I.

Ltac simpl_PCond_BEURK FLD :=
  let req := get_FldEq FLD in
  let lemma := get_CondLemma FLD in
  apply lemma;
  protect_fv "field_cond";
  fold_field_cond req.

(* Rewriting (field_simplify) *)
Ltac Field_norm_gen f n FLD lH rl :=
  let mkFV := get_RingFV FLD in
  let mkFFV := get_FFV FLD in
  let mkFE :=  get_Meta FLD in
  let fv0 := FV_hypo_tac mkFV ltac:(get_FldEq FLD) lH in
  let lemma_tac fv kont :=
    let lemma := get_SimplifyLemma FLD in
    (* reify equations of the context *)
    let lpe := get_Hyp_tac FLD fv lH in
    let vlpe := fresh "hyps" in
    pose (vlpe := lpe);
    let prh := proofHyp_tac lH in
    (* compute the normal form of the reified hyps *)
    let vlmp := fresh "hyps'" in
    let vlmp_eq := fresh "hyps_eq" in
    let mk_monpol := get_MonPol lemma in
    compute_assertion vlmp_eq vlmp (mk_monpol vlpe);
    (* partially instantiate the lemma *)
    let lem := fresh "f_rw_lemma" in
    (assert (lem := lemma n vlpe fv prh vlmp vlmp_eq)
     || fail "type error when building the rewriting lemma");
    (* continuation will call main_tac for all reified terms *)
    kont lem;
    (* at the end, cleanup *)
    (clear lem vlmp_eq vlmp vlpe||idtac"Field_norm_gen:cleanup failed") in
  (* each instance of the lemma is simplified then passed to f *)
  let main_tac H := protect_fv "field" in H; f H in
  (* generate and use equations for each expression *)
  ReflexiveRewriteTactic mkFFV mkFE lemma_tac main_tac fv0 rl;
  try simpl_PCond FLD.

Ltac Field_simplify_gen f FLD lH rl :=
  get_FldPre FLD ();
  Field_norm_gen f ring_subst_niter FLD lH rl;
  get_FldPost FLD ().

Ltac Field_simplify :=
  Field_simplify_gen ltac:(fun H => rewrite H).

Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
  let G := Get_goal in
  field_lookup (PackField Field_simplify) [] rl G.

Tactic Notation (at level 0)
  "field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
  let G := Get_goal in
  field_lookup (PackField Field_simplify) [lH] rl G.

Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
  let G := Get_goal in
  let t := type of H in
  let g := fresh "goal" in
  set (g:= G);
  revert H;
  field_lookup (PackField Field_simplify) [] rl t;
  intro H;
  unfold g;clear g.

Tactic Notation "field_simplify"
    "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):=
  let G := Get_goal in
  let t := type of H in
  let g := fresh "goal" in
  set (g:= G);
  revert H;
  field_lookup (PackField Field_simplify) [lH] rl t;
  intro H;
  unfold g;clear g.

(*
Ltac Field_simplify_in hyp:=
   Field_simplify_gen ltac:(fun H => rewrite H in hyp).

Tactic Notation (at level 0)
  "field_simplify" constr_list(rl) "in" hyp(h) :=
  let t := type of h in
  field_lookup (Field_simplify_in h) [] rl t.

Tactic Notation (at level 0)
  "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
  let t := type of h in
  field_lookup (Field_simplify_in h) [lH] rl t.
*)

(** Generic tactic for solving equations *)

Ltac Field_Scheme Simpl_tac n lemma FLD lH :=
  let req := get_FldEq FLD in
  let mkFV := get_RingFV FLD in
  let mkFFV := get_FFV FLD in
  let mkFE := get_Meta FLD in
  let Main_eq t1 t2 :=
    let fv := FV_hypo_tac mkFV req lH in
    let fv := mkFFV t1 fv in
    let fv := mkFFV t2 fv in
    let lpe := get_Hyp_tac FLD fv lH in
    let prh := proofHyp_tac lH in
    let vlpe := fresh "list_hyp" in
    let fe1 := mkFE t1 fv in
    let fe2 := mkFE t2 fv in
    pose (vlpe := lpe);
    let nlemma := fresh "field_lemma" in
    (assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
     || fail "field anomaly:failed to build lemma");
    ProveLemmaHyps nlemma
      ltac:(fun ilemma =>
              apply ilemma
               || fail "field anomaly: failed in applying lemma";
              [ Simpl_tac | simpl_PCond FLD]);
    clear nlemma;
    subst vlpe in
  OnEquation req Main_eq.

(* solve completely a field equation, leaving non-zero conditions to be
   proved (field) *)

Ltac FIELD FLD lH rl :=
  let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
  let lemma := get_L1 FLD in
  get_FldPre FLD ();
  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
  try exact I;
  get_FldPost FLD().

Tactic Notation (at level 0) "field" :=
  let G := Get_goal in
  field_lookup (PackField FIELD) [] G.

Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
  let G := Get_goal in
  field_lookup (PackField FIELD) [lH] G.

(* transforms a field equation to an equivalent (simplified) ring equation,
   and leaves non-zero conditions to be proved (field_simplify_eq) *)
Ltac FIELD_SIMPL FLD lH rl :=
  let Simpl := (protect_fv "field") in
  let lemma := get_SimplifyEqLemma FLD in
  get_FldPre FLD ();
  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
  get_FldPost FLD ().

Tactic Notation (at level 0) "field_simplify_eq" :=
  let G := Get_goal in
  field_lookup (PackField FIELD_SIMPL) [] G.

Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=
  let G := Get_goal in
  field_lookup (PackField FIELD_SIMPL) [lH] G.

(* Same as FIELD_SIMPL but in hypothesis *)

Ltac Field_simplify_eq n FLD lH :=
  let req := get_FldEq FLD in
  let mkFV := get_RingFV FLD in
  let mkFFV := get_FFV FLD in
  let mkFE := get_Meta FLD in
  let lemma := get_L4 FLD in
  let hyp := fresh "hyp" in
  intro hyp;
  OnEquationHyp req hyp ltac:(fun t1 t2 =>
      let fv := FV_hypo_tac mkFV req lH in
      let fv := mkFFV t1 fv in
      let fv := mkFFV t2 fv in
      let lpe := get_Hyp_tac FLD fv lH in
      let prh := proofHyp_tac lH in
      let fe1 := mkFE t1 fv in
      let fe2 := mkFE t2 fv in
      let vlpe := fresh "vlpe" in
      ProveLemmaHyps (lemma n fv lpe fe1 fe2 prh)
         ltac:(fun ilemma =>
             match type of ilemma with
             | req _ _ ->  _ -> ?EQ =>
               let tmp := fresh "tmp" in
               assert (tmp : EQ);
               [ apply ilemma; [ exact hyp | simpl_PCond_BEURK FLD]
               | protect_fv "field" in tmp; revert tmp ];
               clear hyp
             end)).

Ltac FIELD_SIMPL_EQ FLD lH rl :=
  get_FldPre FLD ();
  Field_simplify_eq Ring_tac.ring_subst_niter FLD lH;
  get_FldPost FLD ().

Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
  let t := type of H in
  generalize H;
  field_lookup (PackField FIELD_SIMPL_EQ) [] t;
  [ try exact I
  | clear H;intro H].


Tactic Notation (at level 0)
  "field_simplify_eq" "[" constr_list(lH) "]"  "in" hyp(H) :=
  let t := type of H in
  generalize H;
  field_lookup (PackField FIELD_SIMPL_EQ) [lH] t;
  [ try exact I
  |clear H;intro H].

(* More generic tactics to build variants of field *)

(* This tactic reifies c and pass to F:
   - the FLD structure gathering all info in the field DB
   - the atom list
   - the expression (FExpr)
 *)
Ltac gen_with_field F c :=
  let MetaExpr FLD _ rl :=
    let R := get_FldCarrier FLD in
    let mkFFV := get_FFV FLD in
    let mkFE  := get_Meta FLD in
    let csr :=
      match rl with
      | List.cons ?r _ => r
      | _ => fail 1 "anomaly: ill-formed list"
      end in
    let fv := mkFFV csr (@List.nil R) in
    let expr := mkFE csr fv in
    F FLD fv expr in
  field_lookup (PackField MetaExpr) [] (c=c).


(* pushes the equation expr = ope(expr) in the goal, and
   discharge it with field *)
Ltac prove_field_eqn ope FLD fv expr :=
  let res := ope expr in
  let expr' := fresh "input_expr" in
  pose (expr' := expr);
  let res' := fresh "result" in
  pose (res' := res);
  let lemma := get_L1 FLD in
  let lemma :=
    constr:(lemma O fv List.nil expr' res' I List.nil (refl_equal _)) in
  let ty := type of lemma in
  let lhs := match ty with
    forall _, ?lhs=_ -> _ => lhs
    end in
  let rhs := match ty with
    forall _, _=_ -> forall _, ?rhs=_ -> _ => rhs
    end in
  let lhs' := fresh "lhs" in let lhs_eq := fresh "lhs_eq" in
  let rhs' := fresh "rhs" in let rhs_eq := fresh "rhs_eq" in
  compute_assertion lhs_eq lhs' lhs;
  compute_assertion rhs_eq rhs' rhs;
  let H := fresh "fld_eqn" in
  refine (_ (lemma lhs' lhs_eq rhs' rhs_eq _ _));
    (* main goal *)
    [intro H;protect_fv "field" in H; revert H
    (* ring-nf(lhs') = ring-nf(rhs') *)
    | vm_compute; reflexivity || fail "field cannot prove this equality"
    (* denominator condition *)
    | simpl_PCond FLD];
  clear lhs_eq rhs_eq; subst lhs' rhs'.

Ltac prove_with_field ope c :=
  gen_with_field ltac:(prove_field_eqn ope) c.

(* Prove an equation x=ope(x) and rewrite with it *)
Ltac prove_rw ope x :=
  prove_with_field ope x;
  [ let H := fresh "Heq_maple" in
    intro H; rewrite H; clear H
  |..].

(* Apply ope (FExpr->FExpr) on an expression *)
Ltac reduce_field_expr ope kont FLD fv expr :=
  let evfun := get_FEeval FLD in
  let res := ope expr in
  let c := (eval simpl_field_expr in (evfun fv res)) in
  kont c.

(* Hack to let a Ltac return a term in the context of a primitive tactic *)
Ltac return_term x := generalize (refl_equal x).
Ltac get_term :=
  match goal with
  | |- ?x = _ -> _ => x
  end.

(* Turn an operation on field expressions (FExpr) into a reduction
   on terms (in the field carrier). Because of field_lookup,
   the tactic cannot return a term directly, so it is returned
   via the conclusion of the goal (return_term). *)
Ltac reduce_field_ope ope c :=
  gen_with_field ltac:(reduce_field_expr ope return_term) c.


(* Adding a new field *)

Ltac ring_of_field f :=
  match type of f with
  | almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f)
  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f)
  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f)
  end.

Ltac coerce_to_almost_field set ext f :=
  match type of f with
  | almost_field_theory _ _ _ _ _ _ _ _ _ => f
  | field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f)
  | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f)
  end.

Ltac field_elements set ext fspec pspec sspec dspec rk :=
  let afth := coerce_to_almost_field set ext fspec in
  let rspec := ring_of_field fspec in
  ring_elements set ext rspec pspec sspec dspec rk
  ltac:(fun arth ext_r morph p_spec s_spec d_spec f => f afth ext_r morph p_spec s_spec d_spec).

Ltac field_lemmas set ext inv_m fspec pspec sspec dspec rk :=
  let get_lemma :=
    match pspec with None => fun x y => x | _ => fun x y => y end in
  let simpl_eq_lemma := get_lemma
       Field_simplify_eq_correct       Field_simplify_eq_pow_correct in
  let simpl_eq_in_lemma := get_lemma
       Field_simplify_eq_in_correct   Field_simplify_eq_pow_in_correct in
  let rw_lemma := get_lemma
       Field_rw_correct                    Field_rw_pow_correct in
  field_elements set ext fspec pspec sspec dspec rk
   ltac:(fun afth ext_r morph p_spec s_spec d_spec =>
     match morph with
     | _ =>
       let field_ok1 := constr:(Field_correct set ext_r inv_m afth morph) in
       match p_spec with
       | mkhypo ?pp_spec =>
         let field_ok2 := constr:(field_ok1 _ _ _ pp_spec) in
         match s_spec with
         | mkhypo ?ss_spec =>
           let field_ok3 := constr:(field_ok2 _ ss_spec) in
           match d_spec with
           | mkhypo ?dd_spec =>
             let field_ok := constr:(field_ok3 _ dd_spec) in
             let mk_lemma lemma :=
              constr:(lemma _ _ _  _ _ _  _ _ _ _
                   set ext_r inv_m afth
                   _ _ _  _ _ _  _ _ _ morph
                   _ _ _ pp_spec _ ss_spec _ dd_spec) in
             let field_simpl_eq_ok := mk_lemma simpl_eq_lemma  in
             let field_simpl_ok := mk_lemma rw_lemma in
             let field_simpl_eq_in := mk_lemma simpl_eq_in_lemma in
             let cond1_ok :=
                constr:(Pcond_simpl_gen set ext_r afth morph pp_spec dd_spec) in
             let cond2_ok :=
               constr:(Pcond_simpl_complete set ext_r afth morph pp_spec dd_spec) in
             (fun f =>
               f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in
                  cond1_ok cond2_ok)
           | _ => fail 4 "field: bad coefficiant division specification"
           end
         | _ => fail 3 "field: bad sign specification"
         end
       | _ => fail 2 "field: bad power specification"
       end
     | _ => fail 1 "field internal error : field_lemmas, please report"
     end).