Ajout de Field

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 1065 insertions, 0 deletions

diff --git a/contrib/field/Field.v b/contrib/field/Field.v
new file mode 100644
index 0000000000..1e5baf0167
--- /dev/null
+++ b/contrib/field/Field.v
@@ -0,0 +1,33 @@
+(* Field.v *)
+
+Require Export Field_Compl.
+Require Export Field_Theory.
+Require Export Field_Tactic.
+
+Declare ML Module "field".
+
+Grammar vernac opt_arg_list : List :=
+| noal [] -> []
+| minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] ->
+  [ "minus" $aminus ($LIST $l) ]
+| div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] ->
+  [ "div" $adiv ($LIST $l) ]
+
+with extra_args : List :=
+| nea [] -> []
+| with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ]
+
+with vernac : ast := 
+  addfield [ "Add" "Field" 
+      	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
+      	     constrarg($azero) constrarg($aopp) constrarg($aeq)
+             constrarg($ainv) constrarg($rth) constrarg($ainv_l) extra_args($l)
+             "." ]
+    -> [(AddField $a $aplus $amult $aone $azero $aopp $aeq $ainv $rth
+                  $ainv_l ($LIST $l))].
+
+Grammar tactic simple_tactic: ast :=
+  | field [ "Field" ] -> [(Field)].
+
+Syntax tactic level 0:
+  | field [(Field)] -> ["Field"].
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
new file mode 100644
index 0000000000..d18d19f764
--- /dev/null
+++ b/contrib/field/Field_Compl.v
@@ -0,0 +1,57 @@
+(* Field_Compl.v *)
+
+Inductive list [A:Type] : Type :=
+  nil : (list A) | cons : A->(list A)->(list A).
+
+Fixpoint app [A:Type][l:(list A)] : (list A) -> (list A) :=
+  [m:(list A)]
+  Cases l of
+  | nil => m 
+  | (cons a l1) => (cons A a (app A l1 m))
+  end.
+
+Inductive Sprod [A:Type;B:Set] : Type :=
+  Spair : A -> B -> (Sprod A B).
+
+Definition assoc_2nd :=
+Fix assoc_2nd_rec {assoc_2nd_rec/4:
+  (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(list (Sprod A B))->B->A->A:=
+    [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(list (Sprod A B));
+      key:B;default:A]
+  Cases lst of
+  | nil => default
+  | (cons (Spair v e) l) =>
+    (Cases (eq_dec e key) of
+    | (left _) => v
+    | (right _) => (assoc_2nd_rec A B eq_dec l key default)
+    end)
+  end}.
+
+Inductive prodT [A,B:Type] : Type :=
+  pairT: A->B->(prodT A B).
+
+Definition fstT [A,B:Type;c:(prodT A B)] :=
+  Cases c of
+  | (pairT a _) => a
+  end.
+
+Definition sndT [A,B:Type;c:(prodT A B)] :=
+  Cases c of
+  | (pairT _ a) => a
+  end.
+
+Definition mem :=
+Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(list A)->bool :=
+  [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(list A)]
+  Cases l of
+  | nil => false
+  | (cons a1 l1) =>
+    Cases (eq_dec a a1) of
+    | (left _) => true
+    | (right _) => (mem A eq_dec a l1)
+    end
+  end}.
+
+Inductive option [A:Type] : Type :=
+  | None : (option A)
+  | Some : (A -> A -> A) -> (option A).
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
new file mode 100644
index 0000000000..d0644e8d60
--- /dev/null
+++ b/contrib/field/Field_Tactic.v
@@ -0,0 +1,251 @@
+(* Field_Tactic.v *)
+
+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 ? ? (assoc ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |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 ? ? (distrib ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |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] Iota
+    |Cbv Beta Delta -[not] 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))].
+
+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 ? ? (multiply ?))== ? |- ?] ->
+      Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |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 ? ? (inverse_simplif ? ?))== ? |- ?] ->
+     Try (Rewrite <- id);Clear id;Cbv Beta Delta -[interp_ExprA] Iota)
+  |Apply inverse_correct;Assumption].
+
+(**** Inverse test ****)
+
+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
+  | [(AoppT ?1)] -> (InverseTestAux FT ?1)
+  | [(AplusT ?1 ?2)] -> (InverseTestAux FT ?1);(InverseTestAux FT ?2)
+  | [(AmultT ?1 ?2)] -> (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 ? ?4 ?5) ] ->
+    (sfun ?1 ?2 ?3);(sfun ?1 ?4 ?5).*)
+  (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 (interp_ExprA FT lvar trm1)==(interp_ExprA FT lvar trm2);
+    [Compute;Auto
+    |(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
+     (Multiply mul);[(ApplySimplif ApplyMultiply);
+       (ApplySimplif (ApplyInverse mul));
+       (Let id = GrepMult In Clear id);Compute;
+       First [(InverseTest FT);Ring|(Field_Gen FT)]|Idtac]].
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
new file mode 100644
index 0000000000..4baa98f6bc
--- /dev/null
+++ b/contrib/field/Field_Theory.v
@@ -0,0 +1,611 @@
+(* Field_Theory.v *)
+
+Require Peano_dec.
+Require Ring.
+Require Field_Compl.
+
+Record Field_Theory : Type :=
+{ A : Type;
+  Aplus : A -> A -> A;
+  Amult : A -> A -> A;
+  Aone : A;
+  Azero : A;
+  Aopp : A -> A;
+  Aeq : A -> A -> bool;
+  Ainv : A -> A;
+  Aminus : (option A);
+  Adiv : (option A);
+  RT : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq);
+  Th_inv_def : (n:A)~(n==Azero)->(Amult (Ainv n) n)==Aone
+}.
+
+(* The reflexion structure *)
+Inductive ExprA : Set :=
+| EAzero    : ExprA
+| EAone    : ExprA
+| EAplus : ExprA -> ExprA -> ExprA
+| EAmult : ExprA -> ExprA -> ExprA
+| EAopp  : ExprA -> ExprA
+| EAinv  : ExprA -> ExprA
+| EAvar  : nat -> ExprA.
+
+(**** Decidability of equality ****)
+
+Lemma eqExprA_O:(e1,e2:ExprA){e1=e2}+{~e1=e2}.
+Proof.
+  Double Induction 1 2;Try Intros;
+   Try (Left;Reflexivity) Orelse Try (Right;Discriminate).
+  Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
+    Try (Left; Rewrite y; Rewrite y0;Auto)
+    Orelse (Right;Red;Intro;Inversion H3;Auto).
+  Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
+    Try (Left; Rewrite y; Rewrite y0;Auto)
+    Orelse (Right;Red;Intro;Inversion H3;Auto).
+  Elim (H0 e);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red; Intro;Inversion H1;Auto.
+  Elim (H0 e);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red; Intro;Inversion H1;Auto.
+  Elim (eq_nat_dec n n0);Intro y.
+  Left; Rewrite y; Auto.
+  Right;Red;Intro;Inversion H;Auto. 
+Save.
+
+Transparent Peano_dec.eq_nat_dec.
+Transparent eqExprA_O.
+
+Definition eq_nat_dec := Eval Compute in Peano_dec.eq_nat_dec.
+Definition eqExprA := Eval Compute in eqExprA_O.
+
+(**** Generation of the multiplier ****)
+
+Fixpoint mult_of_list [e:(list ExprA)]: ExprA :=
+  Cases e of
+  | nil => EAone
+  | (cons e1 l1) => (EAmult e1 (mult_of_list l1))
+  end.
+
+Section Theory_of_fields.
+
+Variable T : Field_Theory.
+
+Local AT := (A T).
+Local AplusT := (Aplus T).
+Local AmultT := (Amult T).
+Local AoneT := (Aone T).
+Local AzeroT := (Azero T).
+Local AoppT := (Aopp T).
+Local AeqT := (Aeq T).
+Local AinvT := (Ainv T).
+Local RTT := (RT T).
+Local Th_inv_defT := (Th_inv_def T).
+
+Add Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (Azero T) (Aopp T) 
+  (Aeq T) (RT T).
+
+Add Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
+
+(***************************)
+(*    Lemmas to be used    *)
+(***************************)
+
+Lemma AplusT_sym:(r1,r2:AT)(AplusT r1 r2)==(AplusT r2 r1).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_assoc:(r1,r2,r3:AT)(AplusT (AplusT r1 r2) r3)==
+                                (AplusT r1 (AplusT r2 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_sym:(r1,r2:AT)(AmultT r1 r2)==(AmultT r2 r1).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_assoc:(r1,r2,r3:AT)(AmultT (AmultT r1 r2) r3)==
+                                (AmultT r1 (AmultT r2 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_Ol:(r:AT)(AplusT AzeroT r)==r.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_1l:(r:AT)(AmultT AoneT r)==r.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AplusT_AoppT_r:(r:AT)(AplusT r (AoppT r))==AzeroT.
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma AmultT_AplusT_distr:(r1,r2,r3:AT)(AmultT r1 (AplusT r2 r3))==
+                        (AplusT (AmultT r1 r2) (AmultT r1 r3)).
+Proof.
+  Intros;Ring.
+Save.
+
+Lemma r_AplusT_plus:(r,r1,r2:AT)(AplusT r r1)==(AplusT r r2)->r1==r2.
+Proof.
+  Intros; Transitivity (AplusT (AplusT (AoppT r) r) r1).
+  Ring.
+  Transitivity (AplusT (AplusT (AoppT r) r) r2).
+  Repeat Rewrite -> AplusT_assoc; Rewrite <- H; Reflexivity.
+  Ring.
+Save.
+ 
+Lemma r_AmultT_mult:
+  (r,r1,r2:AT)(AmultT r r1)==(AmultT r r2)->~r==AzeroT->r1==r2.
+Proof.
+  Intros; Transitivity (AmultT (AmultT (AinvT r) r) r1).
+  Rewrite Th_inv_defT;[Symmetry; Apply AmultT_1l;Auto|Auto].
+  Transitivity (AmultT (AmultT (AinvT r) r) r2).
+  Repeat Rewrite AmultT_assoc; Rewrite H; Trivial.
+  Rewrite Th_inv_defT;[Apply AmultT_1l;Auto|Auto].
+Save.
+
+Lemma AmultT_Or:(r:AT) (AmultT r AzeroT)==AzeroT.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AmultT_Ol:(r:AT)(AmultT AzeroT r)==AzeroT.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AmultT_1r:(r:AT)(AmultT r AoneT)==r.
+Proof.
+  Intro; Ring.
+Save.
+ 
+Lemma AinvT_r:(r:AT)~r==AzeroT->(AmultT r (AinvT r))==AoneT.
+Proof.
+  Intros; Rewrite -> AmultT_sym; Apply Th_inv_defT; Auto.
+Save.
+ 
+Lemma without_div_O_contr:
+  (r1,r2:AT)~(AmultT r1 r2)==AzeroT ->~r1==AzeroT/\~r2==AzeroT.
+Proof.
+  Intros r1 r2 H; Split; Red; Intro; Apply H; Rewrite H0; Ring.
+Save.
+
+(************************)
+(*    Interpretation    *)
+(************************)
+
+(**** ExprA --> A ****)
+
+Fixpoint interp_ExprA [lvar:(list (Sprod AT nat));e:ExprA] : AT :=
+  Cases e of
+  | EAzero            => AzeroT
+  | EAone            => AoneT
+  | (EAplus e1 e2) => (AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
+  | (EAmult e1 e2) => (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2))
+  | (EAopp e)      => ((Aopp T) (interp_ExprA lvar e))
+  | (EAinv e)      => ((Ainv T) (interp_ExprA lvar e))
+  | (EAvar n)      => (assoc_2nd AT nat eq_nat_dec lvar n AzeroT)
+  end.
+
+(************************)
+(*    Simplification    *)
+(************************)
+
+(**** Associativity ****)
+
+Definition merge_mult :=
+  Fix merge_mult {merge_mult/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAmult t1 t2) =>
+    Cases t2 of
+    | (EAmult t2 t3) => (EAmult t1 (EAmult t2 (merge_mult t3 e2)))
+    | _ => (EAmult t1 (EAmult t2 e2))
+    end
+  | _ => (EAmult e1 e2)
+  end}.
+
+Fixpoint assoc_mult [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult e1 e3) =>
+    Cases e1 of
+    | (EAmult e1 e2) =>
+      (merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
+        (assoc_mult e3))
+    | _ => (EAmult e1 (assoc_mult e3))
+    end
+  | _ => e
+  end.
+
+Definition merge_plus :=
+  Fix merge_plus {merge_plus/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    Cases t2 of
+    | (EAplus t2 t3) => (EAplus t1 (EAplus t2 (merge_plus t3 e2)))
+    | _ => (EAplus t1 (EAplus t2 e2))
+    end
+  | _ => (EAplus e1 e2)
+  end}.
+
+Fixpoint assoc [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e3) =>
+    Cases e1 of
+    | (EAplus e1 e2) =>
+      (merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3))
+    | _ => (EAplus (assoc_mult e1) (assoc e3))
+    end
+  | _ => (assoc_mult e)
+  end.
+
+Lemma merge_mult_correct1:
+  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (interp_ExprA lvar (merge_mult (EAmult e1 e2) e3))==
+  (interp_ExprA lvar (EAmult e1 (merge_mult e2 e3))).
+Proof.
+Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2.
+Induction e2;Auto;Intros.
+Unfold 1 merge_mult;Fold merge_mult;
+ Unfold 2 interp_ExprA;Fold interp_ExprA;
+ Rewrite (H0 e e3 lvar);
+ Unfold 1 interp_ExprA;Fold interp_ExprA;
+ Unfold 5 interp_ExprA;Fold interp_ExprA;Auto.
+Save.
+
+Lemma merge_mult_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (merge_mult e1 e2))==
+    (interp_ExprA lvar (EAmult e1 e2)).
+Proof.
+Induction e1;Auto;Intros.
+Elim e0;Try (Intros;Simpl;Ring).
+Unfold interp_ExprA in H2;Fold interp_ExprA in H2;
+ Cut (AmultT (interp_ExprA lvar e2) (AmultT (interp_ExprA lvar e4) 
+       (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))))==
+       (AmultT (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4)) 
+       (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
+Intro H3;Rewrite H3;Rewrite <-H2;
+ Rewrite merge_mult_correct1;Simpl;Ring.
+Ring.
+Save.
+
+Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (AmultT (interp_ExprA lvar (assoc_mult e1)) 
+         (interp_ExprA lvar (assoc_mult e2)))==
+  (interp_ExprA lvar (assoc_mult (EAmult e1 e2))).
+Proof.
+Induction e1;Auto;Intros.
+Rewrite <-(H e0 lvar);Simpl;Rewrite merge_mult_correct;Simpl;
+ Rewrite merge_mult_correct;Simpl;Auto.
+Save.
+
+Lemma assoc_mult_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (assoc_mult e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Auto;Intros.
+Elim e0;Intros.
+Intros;Simpl;Ring.
+Simpl;Rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
+ Rewrite (AmultT_1l (interp_ExprA lvar e1)); Apply H0.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite merge_mult_correct;Simpl;Rewrite merge_mult_correct;Simpl;
+ Rewrite AmultT_assoc;Rewrite assoc_mult_correct1;Rewrite H2;Simpl;
+ Rewrite <-assoc_mult_correct1 in H1;
+ Unfold 3 interp_ExprA in H1;Fold interp_ExprA in H1;
+ Rewrite (H0 lvar) in H1;
+ Rewrite (AmultT_sym (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ Rewrite <-AmultT_assoc;Rewrite H1;Rewrite AmultT_assoc;Ring.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Save.
+
+Lemma merge_plus_correct1:
+  (e1,e2,e3:ExprA)(lvar:(list (Sprod AT nat)))
+  (interp_ExprA lvar (merge_plus (EAplus e1 e2) e3))==
+  (interp_ExprA lvar (EAplus e1 (merge_plus e2 e3))).
+Proof.
+Intros e1 e2;Generalize e1;Generalize e2;Clear e1 e2.
+Induction e2;Auto;Intros.
+Unfold 1 merge_plus;Fold merge_plus;
+ Unfold 2 interp_ExprA;Fold interp_ExprA;
+ Rewrite (H0 e e3 lvar);
+ Unfold 1 interp_ExprA;Fold interp_ExprA;
+ Unfold 5 interp_ExprA;Fold interp_ExprA;Auto.
+Save.
+
+Lemma merge_plus_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (merge_plus e1 e2))==
+    (interp_ExprA lvar (EAplus e1 e2)).
+Proof.
+Induction e1;Auto;Intros.
+Elim e0;Try Intros;Try (Simpl;Ring).
+Unfold interp_ExprA in H2;Fold interp_ExprA in H2;
+  Cut (AplusT (interp_ExprA lvar e2) (AplusT (interp_ExprA lvar e4) 
+        (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))))==
+        (AplusT (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4)) 
+       (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
+Intro H3;Rewrite H3;Rewrite <-H2;Rewrite merge_plus_correct1;Simpl;Ring.
+Ring.
+Save.
+
+Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+  (AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))==
+  (interp_ExprA lvar (assoc (EAplus e1 e2))).
+Proof.
+Induction e1;Auto;Intros.
+Rewrite <-(H e0 lvar);Simpl;Rewrite merge_plus_correct;Simpl;
+ Rewrite merge_plus_correct;Simpl;Auto.
+Save.
+
+Lemma assoc_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (assoc e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Auto;Intros.
+Elim e0;Intros.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite merge_plus_correct;Simpl;Rewrite merge_plus_correct;
+ Simpl;Rewrite AplusT_assoc;Rewrite assoc_plus_correct;Rewrite H2;
+ Simpl;Apply (r_AplusT_plus (interp_ExprA lvar (assoc e1))
+   (AplusT (interp_ExprA lvar (assoc e2))
+     (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1)))
+   (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3))
+        (interp_ExprA lvar e1)));Rewrite <-AplusT_assoc; 
+ Rewrite (AplusT_sym (interp_ExprA lvar (assoc e1)) 
+                    (interp_ExprA lvar (assoc e2)));
+ Rewrite assoc_plus_correct;Rewrite H1;Simpl;Rewrite (H0 lvar);
+ Rewrite <-(AplusT_assoc (AplusT (interp_ExprA lvar e2) 
+            (interp_ExprA lvar e1))
+ (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ Rewrite (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1)
+                      (interp_ExprA lvar e3));
+ Rewrite (AplusT_sym (interp_ExprA lvar e1) (interp_ExprA lvar e3));
+ Rewrite <-(AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
+                        (interp_ExprA lvar e1));Apply AplusT_sym.
+Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA;
+ Rewrite assoc_mult_correct;Rewrite (H0 lvar);Simpl;Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Simpl;Rewrite (H0 lvar);Auto.
+Unfold assoc;Fold assoc;Unfold interp_ExprA;Fold interp_ExprA;
+ Rewrite assoc_mult_correct;Simpl;Auto.
+Save.
+
+(**** Distribution *****)
+
+Fixpoint distrib_EAopp [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) => (EAplus (distrib_EAopp e1) (distrib_EAopp e2))
+  | (EAmult e1 e2) => (EAmult (distrib_EAopp e1) (distrib_EAopp e2))
+  | (EAopp e) => (EAmult (EAopp EAone) (distrib_EAopp e))
+  | e => e
+  end.
+
+Definition distrib_mult_right :=
+  Fix distrib_mult_right {distrib_mult_right/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    (EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2))
+  | _ => (EAmult e1 e2)
+  end}.
+
+Definition distrib_mult_left :=
+  Fix distrib_mult_left {distrib_mult_left/1:ExprA->ExprA->ExprA:=
+  [e1,e2:ExprA]
+  Cases e1 of
+  | (EAplus t1 t2) =>
+    (EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2))
+  | _ => (distrib_mult_right e2 e1)
+  end}.
+
+Fixpoint distrib_main [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult e1 e2) => (distrib_mult_left (distrib_main e1) (distrib_main e2))
+  | (EAplus e1 e2) => (EAplus (distrib_main e1) (distrib_main e2))
+  | (EAopp e) => (EAopp (distrib_main e))
+  | _ => e
+  end.
+
+Definition distrib [e:ExprA] : ExprA := (distrib_main (distrib_EAopp e)).
+
+Lemma distrib_mult_right_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+     (interp_ExprA lvar (distrib_mult_right e1 e2))==
+     (AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)).
+Proof.
+Induction e1;Try Intros;Simpl;Auto.
+Rewrite AmultT_sym;Rewrite AmultT_AplusT_distr;
+ Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Ring.
+Save.
+
+Lemma distrib_mult_left_correct:
+  (e1,e2:ExprA)(lvar:(list (Sprod AT nat)))
+     (interp_ExprA lvar (distrib_mult_left e1 e2))==
+     (AmultT (interp_ExprA lvar e1)  (interp_ExprA lvar e2)).
+Proof.
+Induction e1;Try Intros;Simpl.
+Rewrite AmultT_Ol;Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_Or.
+Rewrite distrib_mult_right_correct;Simpl;
+ Apply AmultT_sym. 
+Rewrite AmultT_sym;
+ Rewrite (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
+  (interp_ExprA lvar e0)); 
+ Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e));
+ Rewrite (AmultT_sym (interp_ExprA lvar e2) (interp_ExprA lvar e0));
+ Rewrite (H e2 lvar);Rewrite (H0 e2 lvar);Auto.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
+Save.
+
+Lemma distrib_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (distrib e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl;Auto.
+Simpl;Rewrite <- (H lvar);Rewrite <- (H0 lvar); Unfold distrib;Simpl;
+ Apply distrib_mult_left_correct.
+Simpl;Fold AoppT;Rewrite <- (H lvar);Unfold distrib;Simpl; 
+ Rewrite distrib_mult_right_correct;
+ Simpl;Fold AoppT;Ring.
+Save.
+
+(**** Multiplication by the inverse product ****)
+
+Lemma mult_eq:
+  (e1,e2,a:ExprA)(lvar:(list (Sprod AT nat)))
+    ~((interp_ExprA lvar a)==AzeroT)->
+      (interp_ExprA lvar (EAmult a e1))==(interp_ExprA lvar (EAmult a e2))->
+        (interp_ExprA lvar e1)==(interp_ExprA lvar e2).
+Proof.
+  Simpl;Intros;
+    Apply (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
+      (interp_ExprA lvar e2));Assumption.
+Save.
+
+Fixpoint multiply_aux [a,e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) =>
+    (EAplus (EAmult a e1) (multiply_aux a e2))
+  | _ => (EAmult a e)
+  end.
+
+Definition multiply [e:ExprA] : ExprA :=
+  Cases e of
+  | (EAmult a e1) => (multiply_aux a e1)
+  | _ => e
+  end.
+
+Lemma multiply_aux_correct:
+  (a,e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (multiply_aux a e))==
+    (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction e;Simpl;Intros;Try (Rewrite merge_mult_correct);Auto.
+  Simpl;Rewrite (H0 lvar);Ring.
+Save.
+
+Lemma multiply_correct:
+  (e:ExprA)(lvar:(list (Sprod AT nat)))
+    (interp_ExprA lvar (multiply e))==(interp_ExprA lvar e).
+Proof.
+  Induction e;Simpl;Auto.
+  Intros;Apply multiply_aux_correct.
+Save.
+
+(**** Permutations and simplification ****)
+
+Fixpoint monom_remove [a,m:ExprA] : ExprA :=
+  Cases m of
+  | (EAmult m0 m1) =>
+    (Cases (eqExprA m0 (EAinv a)) of
+     | (left _) => m1
+     | (right _) => (EAmult m0 (monom_remove a m1))
+     end)
+  | _ =>
+    (Cases (eqExprA m (EAinv a)) of
+     | (left _) => EAone
+     | (right _) => (EAmult a m)
+     end)
+  end.
+
+Definition monom_simplif_rem := 
+  Fix monom_simplif_rem {monom_simplif_rem/1:ExprA->ExprA->ExprA:=
+  [a,m:ExprA] 
+  Cases a of
+  | (EAmult a0 a1) => (monom_simplif_rem a1 (monom_remove a0 m))
+  | _ => (monom_remove a m)
+  end}.
+
+Definition monom_simplif [a,m:ExprA] : ExprA :=
+  Cases m of
+  | (EAmult a' m') =>
+    (Cases (eqExprA a a') of
+     | (left _) => (monom_simplif_rem a m')
+     | (right _) => m
+     end)
+  | _ => m
+  end.
+
+Fixpoint inverse_simplif [a,e:ExprA] : ExprA :=
+  Cases e of
+  | (EAplus e1 e2) => (EAplus (monom_simplif a e1) (inverse_simplif a e2))
+  | _ => (monom_simplif a e)
+  end.
+
+Lemma monom_remove_correct:(e,a:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_remove a e))==
+  (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction e; Intros.
+Simpl;Case (eqExprA EAzero (EAinv a));Intros;[Inversion e0|Simpl;Trivial].
+Simpl;Case (eqExprA EAone (EAinv a));Intros;[Inversion e0|Simpl;Trivial].
+Simpl;Case (eqExprA (EAplus e0 e1) (EAinv a));Intros;[Inversion e2|
+ Simpl;Trivial].
+Simpl;Case (eqExprA e0 (EAinv a));Intros.
+Rewrite e2;Simpl;Fold AinvT.
+Rewrite <-(AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
+             (interp_ExprA lvar e1));
+  Rewrite AinvT_r;[Ring|Assumption].
+Simpl;Rewrite H0;Auto; Ring.
+Simpl;Fold AoppT;Case (eqExprA (EAopp e0) (EAinv a));Intros;[Inversion e1|
+ Simpl;Trivial].
+Unfold monom_remove;Case (eqExprA (EAinv e0) (EAinv a));Intros.
+Case (eqExprA e0 a);Intros.
+Rewrite e2;Simpl;Fold AinvT;Rewrite AinvT_r;Auto.
+Inversion e1;Simpl;ElimType False;Auto.
+Simpl;Trivial.
+Unfold monom_remove;Case (eqExprA (EAvar n) (EAinv a));Intros;
+ [Inversion e0|Simpl;Trivial].
+Save.
+
+Lemma monom_simplif_rem_correct:(a,e:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_simplif_rem a e))==
+  (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Proof.
+Induction a;Simpl;Intros; Try Rewrite monom_remove_correct;Auto.
+Elim (without_div_O_contr (interp_ExprA lvar e) 
+                          (interp_ExprA lvar e0) H1);Intros.
+Rewrite (H0 (monom_remove e e1) lvar H3);Rewrite monom_remove_correct;Auto.
+Ring.
+Save.
+
+Lemma monom_simplif_correct:(e,a:ExprA)
+  (lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+  (interp_ExprA lvar (monom_simplif a e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Case (eqExprA a e0);Intros.
+Rewrite <-e2;Apply monom_simplif_rem_correct;Auto. 
+Simpl;Trivial.
+Save.
+
+Lemma inverse_correct:
+  (e,a:ExprA)(lvar:(list (Sprod AT nat)))~((interp_ExprA lvar a)==AzeroT)->
+    (interp_ExprA lvar (inverse_simplif a e))==(interp_ExprA lvar e).
+Proof.
+Induction e;Intros;Auto.
+Simpl;Rewrite (H0 a lvar H1); Rewrite monom_simplif_correct ; Auto.
+Unfold inverse_simplif;Rewrite monom_simplif_correct ; Auto.
+Save.
+
+End Theory_of_fields.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
new file mode 100644
index 0000000000..60edfe07d8
--- /dev/null
+++ b/contrib/field/field.ml4
@@ -0,0 +1,113 @@
+(* field.ml4 *)
+
+(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*)
+
+open Names
+open Proof_type
+open Tacinterp
+open Tacmach
+open Term
+open Util
+open Vernacinterp
+
+(* Interpretation of constr's *)
+let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
+
+(* Construction of constants *)
+let constant dir s =
+  let dir = "Coq"::"field"::dir in
+  let id = id_of_string s in
+  try 
+    Declare.global_reference_in_absolute_module dir id
+  with Not_found ->
+    anomaly ("Field: cannot find "^
+	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+
+(* To deal with the optional arguments *)
+let constr_of_opt a opt =
+  let ac = constr_of a in
+  match opt with
+  | None -> mkApp ((constant ["Field_Compl"] "None"),[|ac|])
+  | Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|])
+
+(* Table of theories *)
+let th_tab = ref ((Hashtbl.create 53) : (constr,constr) Hashtbl.t)
+
+let lookup typ = Hashtbl.find !th_tab typ
+
+let _ = 
+  let init () = th_tab := (Hashtbl.create 53) in
+  let freeze () = !th_tab in
+  let unfreeze fs = th_tab := fs in
+  Summary.declare_summary "field"
+    { Summary.freeze_function   = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function     = init;
+      Summary.survive_section   = false }
+
+let load_addfield _ = ()
+let cache_addfield (_,(typ,th)) = Hashtbl.add !th_tab typ th
+let export_addfield x = Some x
+
+(* Declaration of the Add Field library object *)
+let (in_addfield,out_addfield)=
+  Libobject.declare_object
+    ("ADD_FIELD",
+     { Libobject.load_function = load_addfield;
+       Libobject.open_function = cache_addfield;
+       Libobject.cache_function = cache_addfield;
+       Libobject.export_function = export_addfield })
+
+(* Adds a theory to the table *)
+let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
+  ainv_l =
+  begin
+    (try
+       Ring.add_theory true true a aplus amult aone azero aopp aeq rth
+         Quote.ConstrSet.empty
+     with | UserError("Add Semi Ring",_) -> ());
+    let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
+      [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
+    Lib.add_anonymous_leaf (in_addfield (a,th))
+  end
+
+(* Vernac command declaration *)
+let _ =
+  let rec opt_arg (aminus_o,adiv_o) = function
+    | (VARG_STRING "minus")::(VARG_CONSTR aminus)::l ->
+      (match aminus_o with
+      |	None -> opt_arg ((Some aminus),adiv_o) l
+      |	_ -> anomaly "AddField")
+    | (VARG_STRING "div")::(VARG_CONSTR adiv)::l ->
+      (match adiv_o with
+      |	None -> opt_arg (aminus_o,(Some adiv)) l
+      |	_ -> anomaly "AddField")
+    | _ -> (aminus_o,adiv_o) in
+  vinterp_add "AddField"
+    (function 
+       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
+	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
+	 ::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth)
+         ::(VARG_CONSTR ainv_l)::l ->
+         (fun () ->
+           let (aminus_o,adiv_o) = opt_arg (None,None) l in
+           add_field (constr_of a) (constr_of aplus) (constr_of amult)
+             (constr_of aone) (constr_of azero) (constr_of aopp)
+             (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
+             (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l))
+       | _ -> anomaly "AddField")
+
+(* Guesses the type and calls Field_Gen with the right theory *)
+let field g =
+  let evc = project g
+  and env = pf_env g in
+  let typ = constr_of_Constr (interp_tacarg (evc,env,[],[],Some g,get_debug ())
+    <:tactic<
+      Match Context With
+      | [|-(eq ?1 ? ?)] -> ?1
+      |	[|-(eqT ?1 ? ?)] -> ?1>>) in
+  let th = VArg (Constr (lookup typ)) in
+  (tac_interp [("FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
+
+(* Declaration of Field *)
+let _ = hide_tactic "Field" (function _ -> field)