Imported Upstream snapshot 8.3~beta0+13298

7 files changed, 1334 insertions, 0 deletions

diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v
new file mode 100644
index 00000000..efa53b4e
--- /dev/null
+++ b/plugins/field/LegacyField.v
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Require Export LegacyField_Compl.
+Require Export LegacyField_Theory.
+Require Export LegacyField_Tactic.
+Declare ML Module "field_plugin".
+
+(* Command declarations are moved to the ML side *)
diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
new file mode 100644
index 00000000..d4a39296
--- /dev/null
+++ b/plugins/field/LegacyField_Compl.v
@@ -0,0 +1,38 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Require Import List.
+
+Definition assoc_2nd :=
+  (fix assoc_2nd_rec (A:Type) (B:Set)
+                     (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
+                     (lst:list (prod A B)) {struct lst} :
+   B -> A -> A :=
+     fun (key:B) (default:A) =>
+       match lst with
+       | nil => default
+       | (v,e) :: l =>
+           match eq_dec e key with
+           | left _ => v
+           | right _ => assoc_2nd_rec A B eq_dec l key default
+           end
+       end).
+
+Definition mem :=
+  (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2})
+           (a:A) (l:list A) {struct l} : bool :=
+     match l with
+     | nil => false
+     | a1 :: l1 =>
+         match eq_dec a a1 with
+         | left _ => true
+         | right _ => mem A eq_dec a l1
+         end
+     end).
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
new file mode 100644
index 00000000..5c1f228a
--- /dev/null
+++ b/plugins/field/LegacyField_Tactic.v
@@ -0,0 +1,433 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Require Import List.
+Require Import LegacyRing.
+Require Export LegacyField_Compl.
+Require Export LegacyField_Theory.
+
+(**** Interpretation A --> ExprA ****)
+
+Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
+
+Ltac body_of s := eval cbv beta iota delta [s] in s.
+
+Ltac mem_assoc var lvar :=
+  match constr:lvar with
+  | nil => constr:false
+  | ?X1 :: ?X2 =>
+      match constr:(X1 = var) with
+      | (?X1 = ?X1) => constr:true
+      | _ => mem_assoc var X2
+      end
+  end.
+
+Ltac number lvar :=
+  let rec number_aux lvar cpt :=
+    match constr:lvar with
+    | (@nil ?X1) => constr:(@nil (prod X1 nat))
+    | ?X2 :: ?X3 =>
+        let l2 := number_aux X3 (S cpt) in
+        constr:((X2,cpt) :: l2)
+    end
+  in number_aux lvar 0.
+
+Ltac build_varlist FT trm :=
+  let rec seek_var lvar trm :=
+    let AT := get_component A FT
+    with AzeroT := get_component Azero FT
+    with AoneT := get_component Aone FT
+    with AplusT := get_component Aplus FT
+    with AmultT := get_component Amult FT
+    with AoppT := get_component Aopp FT
+    with AinvT := get_component Ainv FT in
+    match constr:trm with
+    | AzeroT => lvar
+    | AoneT => lvar
+    | (AplusT ?X1 ?X2) =>
+        let l1 := seek_var lvar X1 in
+        seek_var l1 X2
+    | (AmultT ?X1 ?X2) =>
+        let l1 := seek_var lvar X1 in
+        seek_var l1 X2
+    | (AoppT ?X1) => seek_var lvar X1
+    | (AinvT ?X1) => seek_var lvar X1
+    | ?X1 =>
+        let res := mem_assoc X1 lvar in
+        match constr:res with
+        | true => lvar
+        | false => constr:(X1 :: lvar)
+        end
+    end in
+  let AT := get_component A FT in
+  let lvar := seek_var (@nil AT) trm in
+  number lvar.
+
+Ltac assoc elt lst :=
+  match constr:lst with
+  | nil => fail
+  | (?X1,?X2) :: ?X3 =>
+      match constr:(elt = X1) with
+      | (?X1 = ?X1) => constr:X2
+      | _ => assoc elt X3
+      end
+  end.
+
+Ltac interp_A FT lvar trm :=
+  let AT := get_component A FT
+  with AzeroT := get_component Azero FT
+  with AoneT := get_component Aone FT
+  with AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
+  match constr:trm with
+  | AzeroT => constr:EAzero
+  | AoneT => constr:EAone
+  | (AplusT ?X1 ?X2) =>
+      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
+      constr:(EAplus e1 e2)
+  | (AmultT ?X1 ?X2) =>
+      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
+      constr:(EAmult e1 e2)
+  | (AoppT ?X1) =>
+      let e := interp_A FT lvar X1 in
+      constr:(EAopp e)
+  | (AinvT ?X1) => let e := interp_A FT lvar X1 in
+                   constr:(EAinv e)
+  | ?X1 => let idx := assoc X1 lvar in
+           constr:(EAvar idx)
+  end.
+
+(************************)
+(*    Simplification    *)
+(************************)
+
+(**** Generation of the multiplier ****)
+
+Ltac remove e l :=
+  match constr:l with
+  | nil => l
+  | e :: ?X2 => constr:X2
+  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
+  end.
+
+Ltac union l1 l2 :=
+  match constr:l1 with
+  | nil => l2
+  | ?X2 :: ?X3 =>
+      let nl2 := remove X2 l2 in
+      let nl := union X3 nl2 in
+      constr:(X2 :: nl)
+  end.
+
+Ltac raw_give_mult trm :=
+  match constr:trm with
+  | (EAinv ?X1) => constr:(X1 :: nil)
+  | (EAopp ?X1) => raw_give_mult X1
+  | (EAplus ?X1 ?X2) =>
+      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
+      union l1 l2
+  | (EAmult ?X1 ?X2) =>
+      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
+      eval compute in (app l1 l2)
+  | _ => constr:(@nil ExprA)
+  end.
+
+Ltac give_mult trm :=
+  let ltrm := raw_give_mult trm in
+  constr:(mult_of_list ltrm).
+
+(**** Associativity ****)
+
+Ltac apply_assoc FT lvar trm :=
+  let t := eval compute in (assoc trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (assoc_correct FT trm); change (assoc trm) with t in |- *
+  end.
+
+(**** Distribution *****)
+
+Ltac apply_distrib FT lvar trm :=
+  let t := eval compute in (distrib trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (distrib_correct FT trm);
+       change (distrib trm) with t in |- *
+  end.
+
+(**** Multiplication by the inverse product ****)
+
+Ltac grep_mult := match goal with
+                  | id:(interp_ExprA _ _ _ <> _) |- _ => id
+                  end.
+
+Ltac weak_reduce :=
+  match goal with
+  |  |- context [(interp_ExprA ?X1 ?X2 _)] =>
+      cbv beta iota zeta
+       delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
+             Aone Aplus Amult Aopp Ainv] in |- *
+  end.
+
+Ltac multiply mul :=
+  match goal with
+  |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
+      let AzeroT := get_component Azero FT in
+      cut (interp_ExprA FT X2 mul <> AzeroT);
+       [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
+       | weak_reduce;
+          (let AoneT := get_component Aone ltac:(body_of FT)
+           with AmultT := get_component Amult ltac:(body_of FT) in
+           try
+             match goal with
+             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
+             end; clear FT X2) ]
+  end.
+
+Ltac apply_multiply FT lvar trm :=
+  let t := eval compute in (multiply trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (multiply_correct FT trm);
+       change (multiply trm) with t in |- *
+  end.
+
+(**** Permutations and simplification ****)
+
+Ltac apply_inverse mul FT lvar trm :=
+  let t := eval compute in (inverse_simplif mul trm) in
+  match constr:(t = trm) with
+  | (?X1 = ?X1) => idtac
+  | _ =>
+      rewrite <- (inverse_correct FT trm mul);
+       [ change (inverse_simplif mul trm) with t in |- * | assumption ]
+  end.
+(**** Inverse test ****)
+
+Ltac strong_fail tac := first [ tac | fail 2 ].
+
+Ltac inverse_test_aux FT trm :=
+  let AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
+  match constr:trm with
+  | (AinvT _) => fail 1
+  | (AoppT ?X1) =>
+      strong_fail ltac:(inverse_test_aux FT X1; idtac)
+  | (AplusT ?X1 ?X2) =>
+      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
+  | (AmultT ?X1 ?X2) =>
+      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
+  | _ => idtac
+  end.
+
+Ltac inverse_test FT :=
+  let AplusT := get_component Aplus FT in
+  match goal with
+  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
+  end.
+
+(**** Field itself ****)
+
+Ltac apply_simplif sfun :=
+  match goal with
+  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) =>
+  sfun X1 X2 X3
+  end;
+   match goal with
+   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) =>
+   sfun X1 X2 X3
+   end.
+
+Ltac unfolds FT :=
+  match get_component Aminus FT with
+  | Some ?X1 => unfold X1 in |- *
+  | _ => idtac
+  end;
+  match get_component Adiv FT with
+  | Some ?X1 => unfold X1 in |- *
+  | _ => idtac
+  end.
+
+Ltac reduce FT :=
+  let AzeroT := get_component Azero FT
+  with AoneT := get_component Aone FT
+  with AplusT := get_component Aplus FT
+  with AmultT := get_component Amult FT
+  with AoppT := get_component Aopp FT
+  with AinvT := get_component Ainv FT in
+  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
+     compute in |- *).
+
+Ltac field_gen_aux FT :=
+  let AplusT := get_component Aplus FT in
+  match goal with
+  |  |- (?X1 = ?X2) =>
+      let lvar := build_varlist FT (AplusT X1 X2) in
+      let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
+      let mul := give_mult (EAplus trm1 trm2) in
+      cut
+        (let ft := FT in
+         let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
+        [ compute in |- *; auto
+        | intros ft vm; apply_simplif apply_distrib;
+           apply_simplif apply_assoc; multiply mul;
+           [ apply_simplif apply_multiply;
+              apply_simplif ltac:(apply_inverse mul);
+              (let id := grep_mult in
+               clear id; weak_reduce; clear ft vm; first
+              [ inverse_test FT; legacy ring | field_gen_aux FT ])
+           | idtac ] ]
+  end.
+
+Ltac field_gen FT :=
+  unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
+
+(*****************************)
+(*    Term Simplification    *)
+(*****************************)
+
+(**** Minus and division expansions ****)
+
+Ltac init_exp FT trm :=
+  let e :=
+   (match get_component Aminus FT with
+    | Some ?X1 => eval cbv beta delta [X1] in trm
+    | _ => trm
+    end) in
+  match get_component Adiv FT with
+  | Some ?X1 => eval cbv beta delta [X1] in e
+  | _ => e
+  end.
+
+(**** Inverses simplification ****)
+
+Ltac simpl_inv trm :=
+  match constr:trm with
+  | (EAplus ?X1 ?X2) =>
+      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
+      constr:(EAplus e1 e2)
+  | (EAmult ?X1 ?X2) =>
+      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
+      constr:(EAmult e1 e2)
+  | (EAopp ?X1) => let e := simpl_inv X1 in
+                   constr:(EAopp e)
+  | (EAinv ?X1) => SimplInvAux X1
+  | ?X1 => constr:X1
+  end
+ with SimplInvAux trm :=
+  match constr:trm with
+  | (EAinv ?X1) => simpl_inv X1
+  | (EAmult ?X1 ?X2) =>
+      let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
+      constr:(EAmult e1 e2)
+  | ?X1 => let e := simpl_inv X1 in
+           constr:(EAinv e)
+  end.
+
+(**** Monom simplification ****)
+
+Ltac map_tactic fcn lst :=
+  match constr:lst with
+  | nil => lst
+  | ?X2 :: ?X3 =>
+      let r := fcn X2 with t := map_tactic fcn X3 in
+      constr:(r :: t)
+  end.
+
+Ltac build_monom_aux lst trm :=
+  match constr:lst with
+  | nil => eval compute in (assoc trm)
+  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
+  end.
+
+Ltac build_monom lnum lden :=
+  let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
+  let ltot := eval compute in (app lnum ildn) in
+  let trm := build_monom_aux ltot EAone in
+  match constr:trm with
+  | (EAmult _ ?X1) => constr:X1
+  | ?X1 => constr:X1
+  end.
+
+Ltac simpl_monom_aux lnum lden trm :=
+  match constr:trm with
+  | (EAmult (EAinv ?X1) ?X2) =>
+      let mma := mem_assoc X1 lnum in
+      match constr:mma with
+      | true =>
+          let newlnum := remove X1 lnum in
+          simpl_monom_aux newlnum lden X2
+      | false => simpl_monom_aux lnum (X1 :: lden) X2
+      end
+  | (EAmult ?X1 ?X2) =>
+      let mma := mem_assoc X1 lden in
+      match constr:mma with
+      | true =>
+          let newlden := remove X1 lden in
+          simpl_monom_aux lnum newlden X2
+      | false => simpl_monom_aux (X1 :: lnum) lden X2
+      end
+  | (EAinv ?X1) =>
+      let mma := mem_assoc X1 lnum in
+      match constr:mma with
+      | true =>
+          let newlnum := remove X1 lnum in
+          build_monom newlnum lden
+      | false => build_monom lnum (X1 :: lden)
+      end
+  | ?X1 =>
+      let mma := mem_assoc X1 lden in
+      match constr:mma with
+      | true =>
+          let newlden := remove X1 lden in
+          build_monom lnum newlden
+      | false => build_monom (X1 :: lnum) lden
+      end
+  end.
+
+Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
+
+Ltac simpl_all_monomials trm :=
+  match constr:trm with
+  | (EAplus ?X1 ?X2) =>
+      let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
+      constr:(EAplus e1 e2)
+  | ?X1 => simpl_monom X1
+  end.
+
+(**** Associativity and distribution ****)
+
+Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
+
+(**** The tactic Field_Term ****)
+
+Ltac eval_weak_reduce trm :=
+  eval
+   cbv beta iota zeta
+    delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
+          Amult Aopp Ainv] in trm.
+
+Ltac field_term FT exp :=
+  let newexp := init_exp FT exp in
+  let lvar := build_varlist FT newexp in
+  let trm := interp_A FT lvar newexp in
+  let tma := eval compute in (assoc trm) in
+  let tsmp :=
+   simpl_all_monomials
+    ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
+  let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
+  (replace exp with trep; [ legacy ring trep | field_gen FT ]).
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
new file mode 100644
index 00000000..cc8b043f
--- /dev/null
+++ b/plugins/field/LegacyField_Theory.v
@@ -0,0 +1,650 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Require Import List.
+Require Import Peano_dec.
+Require Import LegacyRing.
+Require Import LegacyField_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 -> A -> A);
+   Adiv : option (A -> A -> A);
+   RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
+   Th_inv_def : forall 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 : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}.
+Proof.
+  double induction e1 e2; try intros;
+   try (left; reflexivity) || (try (right; discriminate)).
+  elim (H1 e0); intro y; elim (H2 e); intro y0;
+   try
+    (left; rewrite y; rewrite y0; auto) ||
+      (right; red in |- *; intro; inversion H3; auto).
+  elim (H1 e0); intro y; elim (H2 e); intro y0;
+   try
+    (left; rewrite y; rewrite y0; auto) ||
+      (right; red in |- *; intro; inversion H3; auto).
+  elim (H0 e); intro y.
+  left; rewrite y; auto.
+  right; red in |- *; intro; inversion H1; auto.
+  elim (H0 e); intro y.
+  left; rewrite y; auto.
+  right; red in |- *; intro; inversion H1; auto.
+  elim (eq_nat_dec n n0); intro y.
+  left; rewrite y; auto.
+  right; red in |- *; intro; inversion H; auto.
+Defined.
+
+Definition eq_nat_dec := Eval compute in eq_nat_dec.
+Definition eqExprA := Eval compute in eqExprA_O.
+
+(**** Generation of the multiplier ****)
+
+Fixpoint mult_of_list (e:list ExprA) : ExprA :=
+  match e with
+  | nil => EAone
+  | e1 :: l1 => EAmult e1 (mult_of_list l1)
+  end.
+
+Section Theory_of_fields.
+
+Variable T : Field_Theory.
+
+Let AT := A T.
+Let AplusT := Aplus T.
+Let AmultT := Amult T.
+Let AoneT := Aone T.
+Let AzeroT := Azero T.
+Let AoppT := Aopp T.
+Let AeqT := Aeq T.
+Let AinvT := Ainv T.
+Let RTT := RT T.
+Let Th_inv_defT := Th_inv_def T.
+
+Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
+ Azero T) (Aopp T) (Aeq T) (RT T).
+
+Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
+
+(***************************)
+(*    Lemmas to be used    *)
+(***************************)
+
+Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AplusT_assoc :
+ forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AmultT_assoc :
+ forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma AmultT_AplusT_distr :
+ forall r1 r2 r3:AT,
+   AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
+Proof.
+  intros; legacy ring.
+Qed.
+
+Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.
+Proof.
+  intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
+  legacy ring.
+  transitivity (AplusT (AplusT (AoppT r) r) r2).
+  repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
+  legacy ring.
+Qed.
+
+Lemma r_AmultT_mult :
+ forall 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  in |- *; 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 ].
+Qed.
+
+Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
+Proof.
+  intro; legacy ring.
+Qed.
+
+Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
+Proof.
+  intro; legacy ring.
+Qed.
+
+Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
+Proof.
+  intro; legacy ring.
+Qed.
+
+Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
+Proof.
+  intros; rewrite AmultT_comm; apply Th_inv_defT; auto.
+Qed.
+
+Lemma Rmult_neq_0_reg :
+ forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
+Proof.
+  intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; legacy ring.
+Qed.
+
+(************************)
+(*    Interpretation    *)
+(************************)
+
+(**** ExprA --> A ****)
+
+Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
+ AT :=
+  match e with
+  | 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 (e1:ExprA) : ExprA -> ExprA :=
+     fun e2:ExprA =>
+       match e1 with
+       | EAmult t1 t2 =>
+           match t2 with
+           | 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 :=
+  match e with
+  | EAmult e1 e3 =>
+      match e1 with
+      | 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 (e1:ExprA) : ExprA -> ExprA :=
+     fun e2:ExprA =>
+       match e1 with
+       | EAplus t1 t2 =>
+           match t2 with
+           | 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 :=
+  match e with
+  | EAplus e1 e3 =>
+      match e1 with
+      | 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 :
+ forall (e1 e2 e3:ExprA) (lvar:list (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.
+simple induction e2; auto; intros.
+unfold merge_mult at 1 in |- *; fold merge_mult in |- *;
+ unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *;
+ rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *;
+ fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *;
+ fold interp_ExprA in |- *; auto.
+Qed.
+
+Lemma merge_mult_correct :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
+Proof.
+simple induction e1; auto; intros.
+elim e0; try (intros; simpl in |- *; legacy 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 in |- *; legacy ring.
+legacy ring.
+Qed.
+
+Lemma assoc_mult_correct1 :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   AmultT (interp_ExprA lvar (assoc_mult e1))
+     (interp_ExprA lvar (assoc_mult e2)) =
+   interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
+Proof.
+simple induction e1; auto; intros.
+rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_mult_correct;
+ simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
+ auto.
+Qed.
+
+Lemma assoc_mult_correct :
+ forall (e:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
+Proof.
+simple induction e; auto; intros.
+elim e0; intros.
+intros; simpl in |- *; legacy ring.
+simpl in |- *; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
+ rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite merge_mult_correct; simpl in |- *;
+ rewrite merge_mult_correct; simpl in |- *; rewrite AmultT_assoc;
+ rewrite assoc_mult_correct1; rewrite H2; simpl in |- *;
+ rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1;
+ fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
+ rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc;
+ legacy ring.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+Qed.
+
+Lemma merge_plus_correct1 :
+ forall (e1 e2 e3:ExprA) (lvar:list (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.
+simple induction e2; auto; intros.
+unfold merge_plus at 1 in |- *; fold merge_plus in |- *;
+ unfold interp_ExprA at 2 in |- *; fold interp_ExprA in |- *;
+ rewrite (H0 e e3 lvar); unfold interp_ExprA at 1 in |- *;
+ fold interp_ExprA in |- *; unfold interp_ExprA at 5 in |- *;
+ fold interp_ExprA in |- *; auto.
+Qed.
+
+Lemma merge_plus_correct :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
+Proof.
+simple induction e1; auto; intros.
+elim e0; try intros; try (simpl in |- *; legacy 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 in |- *; legacy ring.
+legacy ring.
+Qed.
+
+Lemma assoc_plus_correct :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
+   interp_ExprA lvar (assoc (EAplus e1 e2)).
+Proof.
+simple induction e1; auto; intros.
+rewrite <- (H e0 lvar); simpl in |- *; rewrite merge_plus_correct;
+ simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
+ auto.
+Qed.
+
+Lemma assoc_correct :
+ forall (e:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
+Proof.
+simple induction e; auto; intros.
+elim e0; intros.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite merge_plus_correct; simpl in |- *;
+ rewrite merge_plus_correct; simpl in |- *; rewrite AplusT_assoc;
+ rewrite assoc_plus_correct; rewrite H2; simpl in |- *;
+ 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_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
+  ; rewrite assoc_plus_correct; rewrite H1; simpl in |- *;
+ 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_comm (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_comm.
+unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
+ fold interp_ExprA in |- *; rewrite assoc_mult_correct;
+ rewrite (H0 lvar); simpl in |- *; auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+simpl in |- *; rewrite (H0 lvar); auto.
+unfold assoc in |- *; fold assoc in |- *; unfold interp_ExprA in |- *;
+ fold interp_ExprA in |- *; rewrite assoc_mult_correct;
+ simpl in |- *; auto.
+Qed.
+
+(**** Distribution *****)
+
+Fixpoint distrib_EAopp (e:ExprA) : ExprA :=
+  match e with
+  | 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 (e1:ExprA) : ExprA -> ExprA :=
+     fun e2:ExprA =>
+       match e1 with
+       | EAplus t1 t2 =>
+           EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)
+       | _ => EAmult e1 e2
+       end).
+
+Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA :=
+  match e1 with
+  | 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 :=
+  match e with
+  | 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 :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (distrib_mult_right e1 e2) =
+   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
+Proof.
+simple induction e1; try intros; simpl in |- *; auto.
+rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
+ rewrite (H0 e2 lvar); legacy ring.
+Qed.
+
+Lemma distrib_mult_left_correct :
+ forall (e1 e2:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (distrib_mult_left e1 e2) =
+   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
+Proof.
+simple induction e1; try intros; simpl in |- *.
+rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl in |- *;
+ apply AmultT_Or.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+rewrite AmultT_comm;
+ rewrite
+  (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
+     (interp_ExprA lvar e0));
+ rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e));
+ rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0));
+ rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_comm.
+Qed.
+
+Lemma distrib_correct :
+ forall (e:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
+Proof.
+simple induction e; intros; auto.
+simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar);
+ unfold distrib in |- *; simpl in |- *; auto.
+simpl in |- *; rewrite <- (H lvar); rewrite <- (H0 lvar);
+ unfold distrib in |- *; simpl in |- *; apply distrib_mult_left_correct.
+simpl in |- *; fold AoppT in |- *; rewrite <- (H lvar);
+ unfold distrib in |- *; simpl in |- *; rewrite distrib_mult_right_correct;
+ simpl in |- *; fold AoppT in |- *; legacy ring.
+Qed.
+
+(**** Multiplication by the inverse product ****)
+
+Lemma mult_eq :
+ forall (e1 e2 a:ExprA) (lvar:list (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 in |- *; intros;
+   apply
+    (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
+       (interp_ExprA lvar e2)); assumption.
+Qed.
+
+Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA :=
+  match e with
+  | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2)
+  | _ => EAmult a e
+  end.
+
+Definition multiply (e:ExprA) : ExprA :=
+  match e with
+  | EAmult a e1 => multiply_aux a e1
+  | _ => e
+  end.
+
+Lemma multiply_aux_correct :
+ forall (a e:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (multiply_aux a e) =
+   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
+Proof.
+simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
+ auto.
+  simpl in |- *; rewrite (H0 lvar); legacy ring.
+Qed.
+
+Lemma multiply_correct :
+ forall (e:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
+Proof.
+  simple induction e; simpl in |- *; auto.
+  intros; apply multiply_aux_correct.
+Qed.
+
+(**** Permutations and simplification ****)
+
+Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA :=
+  match m with
+  | EAmult m0 m1 =>
+      match eqExprA m0 (EAinv a) with
+      | left _ => m1
+      | right _ => EAmult m0 (monom_remove a m1)
+      end
+  | _ =>
+      match eqExprA m (EAinv a) with
+      | left _ => EAone
+      | right _ => EAmult a m
+      end
+  end.
+
+Definition monom_simplif_rem :=
+  (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA :=
+     fun m:ExprA =>
+       match a with
+       | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m)
+       | _ => monom_remove a m
+       end).
+
+Definition monom_simplif (a m:ExprA) : ExprA :=
+  match m with
+  | EAmult a' m' =>
+      match eqExprA a a' with
+      | left _ => monom_simplif_rem a m'
+      | right _ => m
+      end
+  | _ => m
+  end.
+
+Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
+  match e with
+  | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2)
+  | _ => monom_simplif a e
+  end.
+
+Lemma monom_remove_correct :
+ forall (e a:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar a <> AzeroT ->
+   interp_ExprA lvar (monom_remove a e) =
+   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
+Proof.
+simple induction e; intros.
+simpl in |- *; case (eqExprA EAzero (EAinv a)); intros;
+ [ inversion e0 | simpl in |- *; trivial ].
+simpl in |- *; case (eqExprA EAone (EAinv a)); intros;
+ [ inversion e0 | simpl in |- *; trivial ].
+simpl in |- *; case (eqExprA (EAplus e0 e1) (EAinv a)); intros;
+ [ inversion e2 | simpl in |- *; trivial ].
+simpl in |- *; case (eqExprA e0 (EAinv a)); intros.
+rewrite e2; simpl in |- *; fold AinvT in |- *.
+rewrite <-
+ (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
+    (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ].
+simpl in |- *; rewrite H0; auto; legacy ring.
+simpl in |- *; fold AoppT in |- *; case (eqExprA (EAopp e0) (EAinv a));
+ intros; [ inversion e1 | simpl in |- *; trivial ].
+unfold monom_remove in |- *; case (eqExprA (EAinv e0) (EAinv a)); intros.
+case (eqExprA e0 a); intros.
+rewrite e2; simpl in |- *; fold AinvT in |- *; rewrite AinvT_r; auto.
+inversion e1; simpl in |- *; exfalso; auto.
+simpl in |- *; trivial.
+unfold monom_remove in |- *; case (eqExprA (EAvar n) (EAinv a)); intros;
+ [ inversion e0 | simpl in |- *; trivial ].
+Qed.
+
+Lemma monom_simplif_rem_correct :
+ forall (a e:ExprA) (lvar:list (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.
+simple induction a; simpl in |- *; intros; try rewrite monom_remove_correct;
+ auto.
+elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1);
+ intros.
+rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto.
+legacy ring.
+Qed.
+
+Lemma monom_simplif_correct :
+ forall (e a:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar a <> AzeroT ->
+   interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
+Proof.
+simple induction e; intros; auto.
+simpl in |- *; case (eqExprA a e0); intros.
+rewrite <- e2; apply monom_simplif_rem_correct; auto.
+simpl in |- *; trivial.
+Qed.
+
+Lemma inverse_correct :
+ forall (e a:ExprA) (lvar:list (AT * nat)),
+   interp_ExprA lvar a <> AzeroT ->
+   interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
+Proof.
+simple induction e; intros; auto.
+simpl in |- *; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
+unfold inverse_simplif in |- *; rewrite monom_simplif_correct; auto.
+Qed.
+
+End Theory_of_fields.
+
+(* Compatibility *)
+Notation AplusT_sym := AplusT_comm (only parsing).
+Notation AmultT_sym := AmultT_comm (only parsing).
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
new file mode 100644
index 00000000..238b4c1e
--- /dev/null
+++ b/plugins/field/field.ml4
@@ -0,0 +1,191 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Names
+open Pp
+open Proof_type
+open Tacinterp
+open Tacmach
+open Term
+open Typing
+open Util
+open Vernacinterp
+open Vernacexpr
+open Tacexpr
+open Mod_subst
+open Coqlib
+
+(* Interpretation of constr's *)
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
+
+(* Construction of constants *)
+let constant dir s = gen_constant "Field" ("field"::dir) s
+let init_constant s = gen_constant_in_modules "Field" init_modules s
+
+(* To deal with the optional arguments *)
+let constr_of_opt a opt =
+  let ac = constr_of a in
+  let ac3 = mkArrow ac (mkArrow ac ac) in
+  match opt with
+  | None -> mkApp (init_constant "None",[|ac3|])
+  | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
+
+(* Table of theories *)
+let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
+
+let lookup env typ =
+  try Gmap.find typ !th_tab
+  with Not_found ->
+    errorlabstrm "field"
+      (str "No field is declared for type" ++ spc() ++
+      Printer.pr_lconstr_env env typ)
+
+let _ =
+  let init () = th_tab := Gmap.empty 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 }
+
+let load_addfield _ = ()
+let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab
+let subst_addfield (subst,(typ,th as obj)) =
+  let typ' = subst_mps subst typ in
+  let th' = subst_mps subst th in
+    if typ' == typ && th' == th then obj else
+      (typ',th')
+
+(* Declaration of the Add Field library object *)
+let (in_addfield,out_addfield)=
+  Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
+       Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
+       Libobject.cache_function = cache_addfield;
+       Libobject.subst_function = subst_addfield;
+       Libobject.classify_function = (fun a -> Libobject.Substitute a)}
+
+(* 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 false a None None None aplus amult aone azero
+        (Some aopp) aeq rth Quote.ConstrSet.empty
+     with | UserError("Add Semi Ring",_) -> ());
+    let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
+      [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
+    begin
+      let _ = type_of (Global.env ()) Evd.empty th in ();
+      Lib.add_anonymous_leaf (in_addfield (a,th))
+    end
+  end
+
+(* Vernac command declaration *)
+open Extend
+open Pcoq
+open Genarg
+
+VERNAC ARGUMENT EXTEND divarg
+| [ "div" ":=" constr(adiv) ] -> [ adiv ]
+END
+
+VERNAC ARGUMENT EXTEND minusarg
+| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
+END
+
+(*
+(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
+VERNAC ARGUMENT EXTEND minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+*)
+
+(* For the translator, otherwise the code above is OK *)
+open Ppconstr
+let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
+  if omin=None && odiv=None then mt() else
+    spc() ++ str "with" ++
+    pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
+    pr_opt (fun c -> str "div := " ++ _prc c) odiv
+(*
+let () =
+  Pptactic.declare_extra_genarg_pprule true
+    (rawwit_minus_div_arg,pp_minus_div_arg)
+    (globwit_minus_div_arg,pp_minus_div_arg)
+    (wit_minus_div_arg,pp_minus_div_arg)
+*)
+ARGUMENT EXTEND minus_div_arg
+  TYPED AS constr_opt * constr_opt
+  PRINTED BY pp_minus_div_arg
+| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
+| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
+| [ ] -> [ None, None ]
+END
+
+VERNAC COMMAND EXTEND Field
+  [ "Add" "Legacy" "Field"
+      constr(a) constr(aplus) constr(amult) constr(aone)
+      constr(azero) constr(aopp) constr(aeq)
+      constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
+    -> [ let (aminus_o, adiv_o) = md 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) ]
+END
+
+(* Guesses the type and calls field_gen with the right theory *)
+let field g =
+  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
+  let typ =
+    try match Hipattern.match_with_equation (pf_concl g) with
+      | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
+      | _ -> raise Exit
+    with Hipattern.NoEquationFound | Exit ->
+      error "The statement is not built from Leibniz' equality" in
+  let th = VConstr ([],lookup (pf_env g) typ) in
+  (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
+    <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
+
+(* Verifies that all the terms have the same type and gives the right theory *)
+let guess_theory env evc = function
+  | c::tl ->
+    let t = type_of env evc c in
+    if List.exists (fun c1 ->
+      not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then
+      errorlabstrm "Field:" (str" All the terms must have the same type")
+    else
+      lookup env t
+  | [] -> anomaly "Field: must have a non-empty constr list here"
+
+(* Guesses the type and calls Field_Term with the right theory *)
+let field_term l g =
+  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
+  let env = (pf_env g)
+  and evc = (project g) in
+  let th = valueIn (VConstr ([],guess_theory env evc l))
+  and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
+  (List.fold_right
+    (fun c a ->
+     let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
+     Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
+
+(* Declaration of Field *)
+
+TACTIC EXTEND legacy_field
+| [ "legacy" "field" ] -> [ field ]
+| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
+END
diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib
new file mode 100644
index 00000000..3c3e87af
--- /dev/null
+++ b/plugins/field/field_plugin.mllib
@@ -0,0 +1,2 @@
+Field
+Field_plugin_mod
diff --git a/plugins/field/vo.itarget b/plugins/field/vo.itarget
new file mode 100644
index 00000000..22b56f33
--- /dev/null
+++ b/plugins/field/vo.itarget
@@ -0,0 +1,4 @@
+LegacyField_Compl.vo
+LegacyField_Tactic.vo
+LegacyField_Theory.vo
+LegacyField.vo