Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

4 files changed, 944 insertions, 877 deletions

diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index df2a44f3e7..a7cf332a79 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -12,4 +12,4 @@ Require Export Field_Compl.
 Require Export Field_Theory.
 Require Export Field_Tactic.
 
-(* Command declarations are moved to the ML side *)
+(* Command declarations are moved to the ML side *)
\ No newline at end of file
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index aa3a991470..c90fea1ecc 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -8,55 +8,54 @@
 
 (* $Id$ *)
 
-Inductive listT [A:Type] : Type :=
-  nilT : (listT A) | consT : A->(listT A)->(listT A).
-
-Fixpoint appT [A:Type][l:(listT A)] : (listT A) -> (listT A) :=
-  [m:(listT A)]
-  Cases l of
-  | nilT => m 
-  | (consT a l1) => (consT A a (appT A l1 m))
+Inductive listT (A:Type) : Type :=
+  | nilT : listT A
+  | consT : A -> listT A -> listT A.
+
+Fixpoint appT (A:Type) (l m:listT A) {struct l} : listT A :=
+  match l with
+  | nilT => m
+  | consT a l1 => consT A a (appT A l1 m)
   end.
 
-Inductive prodT [A,B:Type] : Type :=
-  pairT: A->B->(prodT A B).
+Inductive prodT (A B:Type) : Type :=
+    pairT : A -> B -> prodT A B.
 
 Definition assoc_2nd :=
-Fix assoc_2nd_rec
-  {assoc_2nd_rec 
-   [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (prodT A B))]
-   : B->A->A:=
-  [key:B;default:A]
-  Cases lst of
-  | nilT => default
-  | (consT (pairT v e) l) =>
-    (Cases (eq_dec e key) of
-    | (left _) => v
-    | (right _) => (assoc_2nd_rec A B eq_dec l key default)
-    end)
-  end}.
-
-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.
+  (fix assoc_2nd_rec (A:Type) (B:Set)
+                     (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
+                     (lst:listT (prodT A B)) {struct lst} : 
+   B -> A -> A :=
+     fun (key:B) (default:A) =>
+       match lst with
+       | nilT => default
+       | consT (pairT 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 fstT (A B:Type) (c:prodT A B) := match c with
+                                            | pairT a _ => a
+                                            end.
+
+Definition sndT (A B:Type) (c:prodT A B) := match c with
+                                            | pairT _ a => a
+                                            end.
 
 Definition mem :=
-Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool :=
-  Cases l of
-  | nilT => false
-  | (consT 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).
+  (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) 
+           (a:A) (l:listT A) {struct l} : bool :=
+     match l with
+     | nilT => false
+     | consT a1 l1 =>
+         match eq_dec a a1 with
+         | 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.
\ No newline at end of file
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index cd382bc393..a5b206fb20 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -8,102 +8,101 @@
 
 (* $Id$ *)
 
-Require Ring.
+Require Import Ring.
 Require Export Field_Compl.
 Require Export Field_Theory.
 
 (**** Interpretation A --> ExprA ****)
 
-Recursive Tactic Definition MemAssoc var lvar :=
-  Match lvar With
-  | [(nilT ?)] -> false
-  | [(consT ? ?1 ?2)] ->
-    (Match ?1=var With
-     | [?1=?1] -> true
-     | _ -> (MemAssoc var ?2)).
-
-Recursive Tactic Definition SeekVarAux FT lvar trm :=
-  Let AT     = Eval Cbv Beta Delta [A] Iota in (A FT)
-  And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT)
-  And AoneT  = Eval Cbv Beta Delta [Aone] Iota in (Aone FT)
-  And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT)
-  And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT)
-  And AoppT  = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT)
-  And AinvT  = Eval Cbv Beta Delta [Ainv] Iota 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)] -> '(consT AT ?1 lvar).
-
-Tactic Definition SeekVar FT trm :=
-  Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) In
-  (SeekVarAux FT '(nilT AT) trm).
-
-Recursive Tactic Definition NumberAux lvar cpt :=
-  Match lvar With
-  | [(nilT ?1)] -> '(nilT (prodT ?1 nat))
-  | [(consT ?1 ?2 ?3)] ->
-    Let l2 = (NumberAux ?3 '(S cpt)) In
-    '(consT (prodT ?1 nat) (pairT ?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).
-V7only [
-(*Used by contrib Maple *)
-Tactic Definition build_var_list := BuildVarList.
-].
-
-Recursive Tactic Definition Assoc elt lst :=
-  Match lst With
-  | [(nilT ?)] -> Fail
-  | [(consT (prodT ? nat) (pairT ? nat ?1 ?2) ?3)] ->
-    Match elt= ?1 With
-    | [?1= ?1] -> ?2
-    | _ -> (Assoc elt ?3).
-
-Recursive Meta Definition interp_A FT lvar trm :=
-  Let AT     = Eval Cbv Beta Delta [A] Iota in (A FT)
-  And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT)
-  And AoneT  = Eval Cbv Beta Delta [Aone] Iota in (Aone FT)
-  And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT)
-  And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT)
-  And AoppT  = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT)
-  And AinvT  = Eval Cbv Beta Delta [Ainv] Iota 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).
+Ltac mem_assoc var lvar :=
+  match constr:lvar with
+  | (nilT _) => constr:false
+  | (consT _ ?X1 ?X2) =>
+      match constr:(X1 = var) with
+      | (?X1 = ?X1) => constr:true
+      | _ => mem_assoc var X2
+      end
+  end.
+
+Ltac seek_var_aux FT lvar trm :=
+  let AT := eval cbv beta iota delta [A] in (A FT)
+  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  match constr:trm with
+  | AzeroT => lvar
+  | AoneT => lvar
+  | (AplusT ?X1 ?X2) =>
+      let l1 := seek_var_aux FT lvar X1 in
+      seek_var_aux FT l1 X2
+  | (AmultT ?X1 ?X2) =>
+      let l1 := seek_var_aux FT lvar X1 in
+      seek_var_aux FT l1 X2
+  | (AoppT ?X1) => seek_var_aux FT lvar X1
+  | (AinvT ?X1) => seek_var_aux FT lvar X1
+  | ?X1 =>
+      let res := mem_assoc X1 lvar in
+      match constr:res with
+      | true => lvar
+      | false => constr:(consT AT X1 lvar)
+      end
+  end.
+
+Ltac seek_var FT trm :=
+  let AT := eval cbv beta iota delta [A] in (A FT) in
+  seek_var_aux FT (nilT AT) trm.
+
+Ltac number_aux lvar cpt :=
+  match constr:lvar with
+  | (nilT ?X1) => constr:(nilT (prodT X1 nat))
+  | (consT ?X1 ?X2 ?X3) =>
+      let l2 := number_aux X3 (S cpt) in
+      constr:(consT (prodT X1 nat) (pairT X1 nat X2 cpt) l2)
+  end.
+
+Ltac number lvar := number_aux lvar 0.
+
+Ltac build_varlist FT trm := let lvar := seek_var FT trm in
+                             number lvar.
+
+Ltac assoc elt lst :=
+  match constr:lst with
+  | (nilT _) => fail
+  | (consT (prodT _ nat) (pairT _ nat ?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 := eval cbv beta iota delta [A] in (A FT)
+  with AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (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    *)
@@ -111,166 +110,190 @@ Recursive Meta Definition interp_A FT lvar trm :=
 
 (**** Generation of the multiplier ****)
 
-Recursive Tactic Definition Remove e l :=
-  Match l With
-  | [(nilT ?)] -> l
-  | [(consT ?1 e ?2)] -> ?2
-  | [(consT ?1 ?2 ?3)] ->
-    Let nl = (Remove e ?3) In
-    '(consT ?1 ?2 nl).
-
-Recursive Tactic Definition Union l1 l2 :=
-  Match l1 With
-  | [(nilT ?)] -> l2
-  | [(consT ?1 ?2 ?3)] ->
-    Let nl2 = (Remove ?2 l2) In
-    Let nl = (Union ?3 nl2) In
-    '(consT ?1 ?2 nl).
-
-Recursive Tactic Definition RawGiveMult trm :=
-  Match trm With
-  | [(EAinv ?1)] -> '(consT ExprA ?1 (nilT 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 (appT ExprA l1 l2)
-  | _ -> '(nilT ExprA).
-
-Tactic Definition GiveMult trm :=
-  Let ltrm = (RawGiveMult trm) In
-  '(mult_of_list ltrm).
+Ltac remove e l :=
+  match constr:l with
+  | (nilT _) => l
+  | (consT ?X1 e ?X2) => constr:X2
+  | (consT ?X1 ?X2 ?X3) => let nl := remove e X3 in
+                           constr:(consT X1 X2 nl)
+  end.
+
+Ltac union l1 l2 :=
+  match constr:l1 with
+  | (nilT _) => l2
+  | (consT ?X1 ?X2 ?X3) =>
+      let nl2 := remove X2 l2 in
+      let nl := union X3 nl2 in
+      constr:(consT X1 X2 nl)
+  end.
+
+Ltac raw_give_mult trm :=
+  match constr:trm with
+  | (EAinv ?X1) => constr:(consT ExprA X1 (nilT ExprA))
+  | (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 (appT ExprA l1 l2)
+  | _ => constr:(nilT ExprA)
+  end.
+
+Ltac give_mult trm :=
+  let ltrm := raw_give_mult trm in
+  constr:(mult_of_list ltrm).
 
 (**** Associativity ****)
 
-Tactic Definition ApplyAssoc FT lvar trm :=
-  Let t=Eval Compute in (assoc trm) In
-  Match t=trm With
-  | [ ?1=?1 ] -> Idtac
-  | _ -> Rewrite <- (assoc_correct FT trm); Change (assoc trm) with t.
+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 *****)
 
-Tactic Definition ApplyDistrib FT lvar trm :=
-  Let t=Eval Compute in (distrib trm) In
-  Match t=trm With
-  | [ ?1=?1 ] -> Idtac
-  | _ -> Rewrite <- (distrib_correct FT trm); Change (distrib trm) with t.
+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 ****)
 
-Tactic Definition GrepMult :=
-  Match Context With
-    | [ id: ~(interp_ExprA ? ? ?)= ? |- ?] -> id.
-
-Tactic Definition WeakReduce :=
-  Match Context With
-  | [|-[(interp_ExprA ?1 ?2 ?)]] ->
-    Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list ?1 ?2 A
-                    Azero Aone Aplus Amult Aopp Ainv] Zeta Iota.
-
-Tactic Definition Multiply mul :=
-  Match Context With
-  | [|-(interp_ExprA ?1 ?2 ?3)=(interp_ExprA ?1 ?2 ?4)] ->
-    Let AzeroT = Eval Cbv Beta Delta [Azero ?1] Iota 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)
-    |WeakReduce;
-     Let AoneT  = Eval Cbv Beta Delta [Aone ?1] Iota in (Aone ?1)
-     And AmultT = Eval Cbv Beta Delta [Amult ?1] Iota in (Amult ?1) In
-     Try (Match Context With
-          | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2].
-
-Tactic Definition ApplyMultiply FT lvar trm :=
-  Let t=Eval Compute in (multiply trm) In
-  Match t=trm With
-  | [ ?1=?1 ] -> Idtac
-  | _ -> Rewrite <- (multiply_correct FT trm); Change (multiply trm) with t.
+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 ?X1 ?X2 ?X3 = interp_ExprA ?X1 ?X2 ?X4) =>
+      let AzeroT := eval cbv beta iota delta [Azero X1] in (Azero X1) in
+      (cut (interp_ExprA X1 X2 mul <> AzeroT);
+        [ intro; let id := grep_mult in
+                 apply (mult_eq X1 X3 X4 mul X2 id)
+        | weak_reduce;
+           let AoneT := eval cbv beta iota delta [Aone X1] in (Aone X1)
+           with AmultT := eval cbv beta iota delta [Amult X1] in (Amult X1) in
+           (try
+             match goal with
+             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r X1)
+             end; clear X1 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 ****)
 
-Tactic Definition ApplyInverse mul FT lvar trm :=
-  Let t=Eval Compute in (inverse_simplif mul trm) In
-  Match t=trm With
-  | [ ?1=?1 ] -> Idtac
-  | _ -> Rewrite <- (inverse_correct FT trm mul);
-         [Change (inverse_simplif mul trm) with t|Assumption].
+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 ****)
 
-Tactic Definition StrongFail tac := First [tac|Fail 2].
-
-Recursive Tactic Definition InverseTestAux FT trm :=
-  Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT)
-  And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT)
-  And AoppT  = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT)
-  And AinvT  = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In
-  Match trm With
-  | [(AinvT ?)] -> Fail 1
-  | [(AoppT ?1)] -> StrongFail ((InverseTestAux FT ?1);Idtac)
-  | [(AplusT ?1 ?2)] ->
-    StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
-  | [(AmultT ?1 ?2)] ->
-    StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
-  | _ -> Idtac.
-
-Tactic Definition InverseTest FT :=
-  Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In
-  Match Context With
-  | [|- ?1=?2] -> (InverseTestAux FT '(AplusT ?1 ?2)).
+Ltac strong_fail tac := first [ tac | fail 2 ].
+
+Ltac inverse_test_aux FT trm :=
+  let AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (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 := eval cbv beta iota delta [Aplus] in (Aplus FT) in
+  match goal with
+  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
+  end.
 
 (**** Field itself ****)
 
-Tactic Definition ApplySimplif sfun :=
-  (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 Reduce FT :=
-  Let AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT)
-  And AoneT  = Eval Cbv Beta Delta [Aone] Iota in (Aone FT)
-  And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT)
-  And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT)
-  And AoppT  = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT)
-  And AinvT  = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In
-  Cbv Beta Delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] Zeta Iota
-  Orelse Compute.
-
-Recursive Tactic Definition Field_Gen_Aux FT :=
-  Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In
-  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 [ft:=FT][vm:=lvar](interp_ExprA ft vm trm1)=(interp_ExprA ft vm trm2);
-    [Compute;Auto
-    |Intros ft vm;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
-     (Multiply mul);[(ApplySimplif ApplyMultiply);
-       (ApplySimplif (ApplyInverse mul));
-       (Let id = GrepMult In Clear id);WeakReduce;Clear ft vm;
-       First [(InverseTest FT);Ring|(Field_Gen_Aux FT)]|Idtac]].
-
-Tactic Definition Field_Gen FT :=
-  Unfolds FT;((InverseTest FT);Ring) Orelse (Field_Gen_Aux FT).
-V7only [Tactic Definition field_gen := Field_Gen.].
+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 eval cbv beta iota delta [Aminus] in (Aminus FT) with
+  | (Some _ ?X1) => unfold X1 in |- *
+  | _ => idtac
+  end;
+   match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+   | (Some _ ?X1) => unfold X1 in |- *
+   | _ => idtac
+   end.
+
+Ltac reduce FT :=
+  let AzeroT := eval cbv beta iota delta [Azero] in (Azero FT)
+  with AoneT := eval cbv beta iota delta [Aone] in (Aone FT)
+  with AplusT := eval cbv beta iota delta [Aplus] in (Aplus FT)
+  with AmultT := eval cbv beta iota delta [Amult] in (Amult FT)
+  with AoppT := eval cbv beta iota delta [Aopp] in (Aopp FT)
+  with AinvT := eval cbv beta iota delta [Ainv] in (Ainv FT) in
+  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] in |- * ||
+     compute in |- *).
+
+Ltac field_gen_aux FT :=
+  let AplusT := eval cbv beta iota delta [Aplus] in (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; ring | field_gen_aux FT ]
+           | idtac ] ])
+  end.
+
+Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
 
 (*****************************)
 (*    Term Simplification    *)
@@ -278,120 +301,132 @@ V7only [Tactic Definition field_gen := Field_Gen.].
 
 (**** Minus and division expansions ****)
 
-Meta Definition InitExp FT trm :=
-  Let e =
-    (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With
-     | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm
-     | _ -> trm) In
-  Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
-  | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e
-  | _ -> e.
-V7only [
-(*Used by contrib Maple *)
-Tactic Definition init_exp := InitExp.
-].
+Ltac init_exp FT trm :=
+  let e :=
+   (match eval cbv beta iota delta [Aminus] in (Aminus FT) with
+    | (Some _ ?X1) => eval cbv beta delta [X1] in trm
+    | _ => trm
+    end) in
+  match eval cbv beta iota delta [Adiv] in (Adiv FT) with
+  | (Some _ ?X1) => eval cbv beta delta [X1] in e
+  | _ => e
+  end.
 
 (**** Inverses simplification ****)
 
-Recursive Meta Definition SimplInv trm:=
-  Match trm With
-  | [(EAplus ?1 ?2)] ->
-    Let e1 = (SimplInv ?1)
-    And e2 = (SimplInv ?2) In
-    '(EAplus e1 e2)
-  | [(EAmult ?1 ?2)] ->
-    Let e1 = (SimplInv ?1)
-    And e2 = (SimplInv ?2) In
-    '(EAmult e1 e2)
-  | [(EAopp ?1)] -> Let e = (SimplInv ?1) In '(EAopp e)
-  | [(EAinv ?1)] -> (SimplInvAux ?1)
-  | [?1] -> ?1
-And SimplInvAux trm :=
-  Match trm With
-  | [(EAinv ?1)] -> (SimplInv ?1)
-  | [(EAmult ?1 ?2)] ->
-    Let e1 = (SimplInv '(EAinv ?1))
-    And e2 = (SimplInv '(EAinv ?2)) In
-    '(EAmult e1 e2)
-  | [?1] -> Let e = (SimplInv ?1) In '(EAinv e).
+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 ****)
 
-Recursive Meta Definition Map fcn lst :=
-  Match lst With
-  | [(nilT ?)] -> lst
-  | [(consT ?1 ?2 ?3)] ->
-    Let r = (fcn ?2)
-    And t = (Map fcn ?3) In
-    '(consT ?1 r t).
-
-Recursive Meta Definition BuildMonomAux lst trm :=
-  Match lst With
-  | [(nilT ?)] -> Eval Compute in (assoc trm)
-  | [(consT ? ?1 ?2)] -> BuildMonomAux ?2 '(EAmult trm ?1).
-
-Recursive Meta Definition BuildMonom lnum lden :=
-  Let ildn = (Map (Fun e -> '(EAinv e)) lden) In
-  Let ltot = Eval Compute in (appT ExprA lnum ildn) In
-  Let trm = (BuildMonomAux ltot EAone) In
-  Match trm With
-  | [(EAmult ? ?1)] -> ?1
-  | [?1] -> ?1.
-
-Recursive Meta Definition SimplMonomAux lnum lden trm :=
-  Match trm With
-  | [(EAmult (EAinv ?1) ?2)] ->
-    Let mma = (MemAssoc ?1 lnum) In
-    (Match mma With
-     | [true] ->
-       Let newlnum = (Remove ?1 lnum) In SimplMonomAux newlnum lden ?2
-     | [false] -> SimplMonomAux lnum '(consT ExprA ?1 lden) ?2)
-  | [(EAmult ?1 ?2)] ->
-    Let mma = (MemAssoc ?1 lden) In
-    (Match mma With
-     | [true] ->
-       Let newlden = (Remove ?1 lden) In SimplMonomAux lnum newlden ?2
-     | [false] -> SimplMonomAux '(consT ExprA ?1 lnum) lden ?2)
-  | [(EAinv ?1)] ->
-    Let mma = (MemAssoc ?1 lnum) In
-    (Match mma With
-     | [true] ->
-       Let newlnum = (Remove ?1 lnum) In BuildMonom newlnum lden
-     | [false] -> BuildMonom lnum '(consT ExprA ?1 lden))
-  | [?1] ->
-    Let mma = (MemAssoc ?1 lden) In
-    (Match mma With
-     | [true] ->
-       Let newlden = (Remove ?1 lden) In BuildMonom lnum newlden
-     | [false] -> BuildMonom '(consT ExprA ?1 lnum) lden).
-
-Meta Definition SimplMonom trm :=
-  SimplMonomAux '(nilT ExprA) '(nilT ExprA) trm.
-
-Recursive Meta Definition SimplAllMonoms trm :=
-  Match trm With
-  | [(EAplus ?1 ?2)] ->
-    Let e1 = (SimplMonom ?1)
-    And e2 = (SimplAllMonoms ?2) In
-    '(EAplus e1 e2)
-  | [?1] -> SimplMonom ?1.
+Ltac map_tactic fcn lst :=
+  match constr:lst with
+  | (nilT _) => lst
+  | (consT ?X1 ?X2 ?X3) =>
+      let r := fcn X2 with t := map_tactic fcn X3 in
+      constr:(consT X1 r t)
+  end.
+
+Ltac build_monom_aux lst trm :=
+  match constr:lst with
+  | (nilT _) => eval compute in (assoc trm)
+  | (consT _ ?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 (appT ExprA 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 (consT ExprA 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 (consT ExprA 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 (consT ExprA 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 (consT ExprA X1 lnum) lden
+      end
+  end.
+
+Ltac simpl_monom trm := simpl_monom_aux (nilT ExprA) (nilT 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 ****)
 
-Meta Definition AssocDistrib trm := Eval Compute in (assoc (distrib trm)).
+Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
 
 (**** The tactic Field_Term ****)
 
-Tactic Definition EvalWeakReduce trm :=
-  Eval Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero
-                       Aone Aplus Amult Aopp Ainv] Zeta Iota in trm.
-
-Tactic Definition Field_Term FT exp :=
-  Let newexp = (InitExp FT exp) In
-  Let lvar = (BuildVarList FT newexp) In
-  Let trm = (interp_A FT lvar newexp) In
-  Let tma = Eval Compute in (assoc trm) In
-  Let tsmp = (SimplAllMonoms (AssocDistrib (SimplAllMonoms
-                (SimplInv tma)))) In
-  Let trep = (EvalWeakReduce '(interp_ExprA FT lvar tsmp)) In
-  Replace exp with trep;[Ring trep|Field_Gen FT].
+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; [ ring trep | field_gen FT ]).
\ No newline at end of file
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index e2710260f9..35f1125e41 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -8,86 +8,87 @@
 
 (* $Id$ *)
 
-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
-}.
+Require Import Peano_dec.
+Require Import Ring.
+Require Import 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 : 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.
+  | 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 e1 e2;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. 
+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 Peano_dec.eq_nat_dec.
-Definition eqExprA := Eval Compute in eqExprA_O.
+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:(listT ExprA)]: ExprA :=
-  Cases e of
+Fixpoint mult_of_list (e:listT ExprA) : ExprA :=
+  match e with
   | nilT => EAone
-  | (consT e1 l1) => (EAmult e1 (mult_of_list l1))
+  | consT 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).
+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 Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (Azero T) (Aopp T) 
-  (Aeq T) (RT 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.
 
@@ -95,93 +96,94 @@ 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).
+Lemma AplusT_sym : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AplusT_assoc:(r1,r2,r3:AT)(AplusT (AplusT r1 r2) r3)=
-                                (AplusT r1 (AplusT r2 r3)).
+Lemma AplusT_assoc :
+ forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AmultT_sym:(r1,r2:AT)(AmultT r1 r2)=(AmultT r2 r1).
+Lemma AmultT_sym : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AmultT_assoc:(r1,r2,r3:AT)(AmultT (AmultT r1 r2) r3)=
-                                (AmultT r1 (AmultT r2 r3)).
+Lemma AmultT_assoc :
+ forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AplusT_Ol:(r:AT)(AplusT AzeroT r)=r.
+Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AmultT_1l:(r:AT)(AmultT AoneT r)=r.
+Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AplusT_AoppT_r:(r:AT)(AplusT r (AoppT r))=AzeroT.
+Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma AmultT_AplusT_distr:(r1,r2,r3:AT)(AmultT r1 (AplusT r2 r3))=
-                        (AplusT (AmultT r1 r2) (AmultT r1 r3)).
+Lemma AmultT_AplusT_distr :
+ forall r1 r2 r3:AT,
+   AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
 Proof.
-  Intros;Ring.
-Save.
+  intros; ring.
+Qed.
 
-Lemma r_AplusT_plus:(r,r1,r2:AT)(AplusT r r1)=(AplusT r r2)->r1=r2.
+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).
-  Ring.
-  Transitivity (AplusT (AplusT (AoppT r) r) r2).
-  Repeat Rewrite -> AplusT_assoc; Rewrite <- H; Reflexivity.
-  Ring.
-Save.
+  intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
+  ring.
+  transitivity (AplusT (AplusT (AoppT r) r) r2).
+  repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
+  ring.
+Qed.
  
-Lemma r_AmultT_mult:
-  (r,r1,r2:AT)(AmultT r r1)=(AmultT r r2)->~r=AzeroT->r1=r2.
+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; 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.
+  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:(r:AT) (AmultT r AzeroT)=AzeroT.
+Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
 Proof.
-  Intro; Ring.
-Save.
+  intro; ring.
+Qed.
  
-Lemma AmultT_Ol:(r:AT)(AmultT AzeroT r)=AzeroT.
+Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
 Proof.
-  Intro; Ring.
-Save.
+  intro; ring.
+Qed.
  
-Lemma AmultT_1r:(r:AT)(AmultT r AoneT)=r.
+Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
 Proof.
-  Intro; Ring.
-Save.
+  intro; ring.
+Qed.
  
-Lemma AinvT_r:(r:AT)~r=AzeroT->(AmultT r (AinvT r))=AoneT.
+Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
 Proof.
-  Intros; Rewrite -> AmultT_sym; Apply Th_inv_defT; Auto.
-Save.
+  intros; rewrite AmultT_sym; apply Th_inv_defT; auto.
+Qed.
  
-Lemma without_div_O_contr:
-  (r1,r2:AT)~(AmultT r1 r2)=AzeroT ->~r1=AzeroT/\~r2=AzeroT.
+Lemma Rmult_neq_0_reg :
+ forall 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.
+  intros r1 r2 H; split; red in |- *; intro; apply H; rewrite H0; ring.
+Qed.
 
 (************************)
 (*    Interpretation    *)
@@ -189,15 +191,16 @@ Save.
 
 (**** ExprA --> A ****)
 
-Fixpoint interp_ExprA [lvar:(listT (prodT 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)
+Fixpoint interp_ExprA (lvar:listT (prodT 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.
 
 (************************)
@@ -207,406 +210,436 @@ Fixpoint interp_ExprA [lvar:(listT (prodT AT nat));e:ExprA] : AT :=
 (**** Associativity ****)
 
 Definition merge_mult :=
-  Fix merge_mult {merge_mult [e1:ExprA] : ExprA -> ExprA :=
-  [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
+  (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 {merge_plus [e1:ExprA]:ExprA->ExprA:=
-  [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)
+  (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:
-  (e1,e2,e3:ExprA)(lvar:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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.
+Lemma merge_mult_correct1 :
+ forall (e1 e2 e3:ExprA) (lvar:listT (prodT 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:listT (prodT 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 |- *; 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 |- *; ring.
+ring.
+Qed.
+
+Lemma assoc_mult_correct1 :
+ forall (e1 e2:ExprA) (lvar:listT (prodT 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:listT (prodT AT nat)),
+   interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
+Proof.
+simple induction e; auto; intros.
+elim e0; intros.
+intros; simpl in |- *; 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_sym (interp_ExprA lvar e3) (interp_ExprA lvar e1));
+ rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc; 
+ 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:listT (prodT 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:listT (prodT 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 |- *; 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 |- *; ring.
+ring.
+Qed.
+
+Lemma assoc_plus_correct :
+ forall (e1 e2:ExprA) (lvar:listT (prodT 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:listT (prodT 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_sym (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_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 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 :=
-  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))
+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 {distrib_mult_right [e1:ExprA]:ExprA->ExprA:=
-  [e2:ExprA]Cases e1 of
-  | (EAplus t1 t2) =>
-    (EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2))
-  | _ => (EAmult e1 e2)
-  end}.
-
-Fixpoint distrib_mult_left [e1:ExprA] : ExprA->ExprA :=
-  [e2:ExprA]
-  Cases e1 of
-  | (EAplus t1 t2) =>
-    (EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2))
-  | _ => (distrib_mult_right e2 e1)
+  (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 :=
-  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))
+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:
-  (e1,e2:ExprA)(lvar:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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.
+Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
+
+Lemma distrib_mult_right_correct :
+ forall (e1 e2:ExprA) (lvar:listT (prodT 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_sym; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
+ rewrite (H0 e2 lvar); ring.
+Qed.
+
+Lemma distrib_mult_left_correct :
+ forall (e1 e2:ExprA) (lvar:listT (prodT 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_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 in |- *; apply AmultT_sym.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
+rewrite distrib_mult_right_correct; simpl in |- *; apply AmultT_sym.
+Qed.
+
+Lemma distrib_correct :
+ forall (e:ExprA) (lvar:listT (prodT 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 |- *; ring.
+Qed.
 
 (**** Multiplication by the inverse product ****)
 
-Lemma mult_eq:
-  (e1,e2,a:ExprA)(lvar:(listT (prodT 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)
+Lemma mult_eq :
+ forall (e1 e2 a:ExprA) (lvar:listT (prodT 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 :=
-  Cases e of
-  | (EAmult a e1) => (multiply_aux a e1)
+Definition multiply (e:ExprA) : ExprA :=
+  match e with
+  | EAmult a e1 => multiply_aux a e1
   | _ => e
   end.
 
-Lemma multiply_aux_correct:
-  (a,e:ExprA)(lvar:(listT (prodT AT nat)))
-    (interp_ExprA lvar (multiply_aux a e))=
-    (AmultT (interp_ExprA lvar a) (interp_ExprA lvar e)).
+Lemma multiply_aux_correct :
+ forall (a e:ExprA) (lvar:listT (prodT 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.
+simple induction e; simpl in |- *; intros; try rewrite merge_mult_correct;
+ auto.
+  simpl in |- *; rewrite (H0 lvar); ring.
+Qed.
 
-Lemma multiply_correct:
-  (e:ExprA)(lvar:(listT (prodT AT nat)))
-    (interp_ExprA lvar (multiply e))=(interp_ExprA lvar e).
+Lemma multiply_correct :
+ forall (e:ExprA) (lvar:listT (prodT AT nat)),
+   interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
 Proof.
-  Induction e;Simpl;Auto.
-  Intros;Apply multiply_aux_correct.
-Save.
+  simple induction e; simpl in |- *; auto.
+  intros; apply multiply_aux_correct.
+Qed.
 
 (**** 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)
+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
   | _ =>
-    (Cases (eqExprA m (EAinv a)) of
-     | (left _) => EAone
-     | (right _) => (EAmult a m)
-     end)
+      match eqExprA m (EAinv a) with
+      | 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)
+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] : ExprA :=
-  Cases e of
-  | (EAplus e1 e2) => (EAplus (monom_simplif a e1) (inverse_simplif a e2))
-  | _ => (monom_simplif a e)
+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:(e,a:ExprA)
-  (lvar:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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:(listT (prodT 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.
+Lemma monom_remove_correct :
+ forall (e a:ExprA) (lvar:listT (prodT 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; [ ring | assumption ].
+simpl in |- *; rewrite H0; auto; 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 |- *; elimtype False; 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:listT (prodT 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.
+ring.
+Qed.
+
+Lemma monom_simplif_correct :
+ forall (e a:ExprA) (lvar:listT (prodT 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:listT (prodT 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.
\ No newline at end of file