1 files changed, 567 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
new file mode 100644
index 000000000..b31ebda55
--- /dev/null
+++ b/plugins/setoid_ring/Field_tac.v
@@ -0,0 +1,567 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \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 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().
+
+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).
+
+(* 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).