Légères simplifications code de Field; message d'erreur si pas égalité

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

4 files changed, 51 insertions, 69 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index edf0793176..aa3a991470 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -18,27 +18,24 @@ Fixpoint appT [A:Type][l:(listT A)] : (listT A) -> (listT A) :=
   | (consT a l1) => (consT A a (appT A l1 m))
   end.
 
-Inductive Sprod [A:Type;B:Set] : Type :=
-  Spair : A -> B -> (Sprod 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 (Sprod A B))]
+   [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 (Spair v e) l) =>
+  | (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}.
 
-Inductive prodT [A,B:Type] : Type :=
-  pairT: A->B->(prodT A B).
-
 Definition fstT [A,B:Type;c:(prodT A B)] :=
   Cases c of
   | (pairT a _) => a
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 74869ba3ba..1411c4a543 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -53,10 +53,10 @@ Tactic Definition SeekVar FT trm :=
 
 Recursive Tactic Definition NumberAux lvar cpt :=
   Match lvar With
-  | [(nilT ?1)] -> '(nilT (Sprod ?1 nat))
+  | [(nilT ?1)] -> '(nilT (prodT ?1 nat))
   | [(consT ?1 ?2 ?3)] ->
     Let l2 = (NumberAux ?3 '(S cpt)) In
-    '(consT (Sprod ?1 nat) (Spair ?1 nat ?2 cpt) l2).
+    '(consT (prodT ?1 nat) (pairT ?1 nat ?2 cpt) l2).
 
 Tactic Definition Number lvar := (NumberAux lvar O).
 
@@ -67,7 +67,7 @@ Tactic Definition BuildVarList FT trm :=
 Recursive Tactic Definition Assoc elt lst :=
   Match lst With
   | [(nilT ?)] -> Fail
-  | [(consT (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
+  | [(consT (prodT ? nat) (pairT ? nat ?1 ?2) ?3)] ->
     Match elt= ?1 With
     | [?1= ?1] -> ?2
     | _ -> (Assoc elt ?3).
@@ -144,24 +144,18 @@ Tactic Definition GiveMult trm :=
 (**** Associativity ****)
 
 Tactic Definition ApplyAssoc FT lvar trm :=
-  Cut (interp_ExprA FT lvar (assoc trm))=(interp_ExprA FT lvar trm);
-  [Intro;
-   (Match Context With
-    | [id:(interp_ExprA ?1 ?2 (assoc ?3))= ?4 |- ?] ->
-      Let t=Eval Compute in (assoc ?3) In
-      Change (interp_ExprA ?1 ?2 t)= ?4 in id;Try (Rewrite <- id);Clear id)
-  |Apply assoc_correct].
+  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.
 
 (**** Distribution *****)
 
 Tactic Definition ApplyDistrib FT lvar trm :=
-  Cut (interp_ExprA FT lvar (distrib trm))=(interp_ExprA FT lvar trm);
-  [Intro;
-   (Match Context With
-    | [id:(interp_ExprA ?1 ?2 (distrib ?3))= ?4 |- ?] ->
-      Let t=Eval Compute in (distrib ?3) In
-      Change (interp_ExprA ?1 ?2 t)= ?4 in id;Try (Rewrite <- id);Clear id)
-  |Apply distrib_correct].
+  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.
 
 (**** Multiplication by the inverse product ****)
 
@@ -190,26 +184,19 @@ Tactic Definition Multiply mul :=
           | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2].
 
 Tactic Definition ApplyMultiply FT lvar trm :=
-  Cut (interp_ExprA FT lvar (multiply trm))=(interp_ExprA FT lvar trm);
-  [Intro;
-   (Match Context With
-    | [id:(interp_ExprA ?1 ?2 (multiply ?3))= ?4 |- ?] ->
-      Let t=Eval Compute in (multiply ?3) In
-      Change (interp_ExprA ?1 ?2 t)= ?4 in id;Try (Rewrite <- id);Clear id)
-  |Apply multiply_correct].
+  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.
 
 (**** Permutations and simplification ****)
 
 Tactic Definition ApplyInverse mul FT lvar trm :=
-  Cut (interp_ExprA FT lvar (inverse_simplif mul trm))=
-      (interp_ExprA FT lvar trm);
-  [Intro;
-   (Match Context With
-   | [id:(interp_ExprA ?1 ?2 (inverse_simplif ?3 ?4))= ?5 |- ?] ->
-     Let t=Eval Compute in (inverse_simplif ?3 ?4) In
-      Change (interp_ExprA ?1 ?2 t)= ?5 in id;Try (Rewrite <- id);Clear id)
-  |Apply inverse_correct;Assumption].
-
+  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].
 (**** Inverse test ****)
 
 Tactic Definition StrongFail tac := First [tac|Fail 2].
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 054c13e088..e2710260f9 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -189,7 +189,7 @@ Save.
 
 (**** ExprA --> A ****)
 
-Fixpoint interp_ExprA [lvar:(listT (Sprod AT nat));e:ExprA] : AT :=
+Fixpoint interp_ExprA [lvar:(listT (prodT AT nat));e:ExprA] : AT :=
   Cases e of
   | EAzero         => AzeroT
   | EAone          => AoneT
@@ -252,7 +252,7 @@ Fixpoint assoc [e:ExprA] : ExprA :=
   end.
 
 Lemma merge_mult_correct1:
-  (e1,e2,e3:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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.
@@ -266,7 +266,7 @@ Unfold 1 merge_mult;Fold merge_mult;
 Save.
 
 Lemma merge_mult_correct:
-  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (merge_mult e1 e2))=
     (interp_ExprA lvar (EAmult e1 e2)).
 Proof.
@@ -282,7 +282,7 @@ Intro H3;Rewrite H3;Rewrite <-H2;
 Ring.
 Save.
 
-Lemma assoc_mult_correct1:(e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+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))).
@@ -293,7 +293,7 @@ Rewrite <-(H e0 lvar);Simpl;Rewrite merge_mult_correct;Simpl;
 Save.
 
 Lemma assoc_mult_correct:
-  (e:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (assoc_mult e))=(interp_ExprA lvar e).
 Proof.
 Induction e;Auto;Intros.
@@ -315,7 +315,7 @@ Simpl;Rewrite (H0 lvar);Auto.
 Save.
 
 Lemma merge_plus_correct1:
-  (e1,e2,e3:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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.
@@ -329,7 +329,7 @@ Unfold 1 merge_plus;Fold merge_plus;
 Save.
 
 Lemma merge_plus_correct:
-  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e1,e2:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (merge_plus e1 e2))=
     (interp_ExprA lvar (EAplus e1 e2)).
 Proof.
@@ -344,7 +344,7 @@ Intro H3;Rewrite H3;Rewrite <-H2;Rewrite merge_plus_correct1;Simpl;Ring.
 Ring.
 Save.
 
-Lemma assoc_plus_correct:(e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+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.
@@ -354,7 +354,7 @@ Rewrite <-(H e0 lvar);Simpl;Rewrite merge_plus_correct;Simpl;
 Save.
 
 Lemma assoc_correct:
-  (e:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (assoc e))=(interp_ExprA lvar e).
 Proof.
 Induction e;Auto;Intros.
@@ -406,14 +406,13 @@ Definition distrib_mult_right :=
   | _ => (EAmult e1 e2)
   end}.
 
-Definition distrib_mult_left :=
-  Fix distrib_mult_left {distrib_mult_left/1:ExprA->ExprA->ExprA:=
-  [e1,e2:ExprA]
+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)
-  end}.
+  end.
 
 Fixpoint distrib_main [e:ExprA] : ExprA :=
   Cases e of
@@ -426,7 +425,7 @@ Fixpoint distrib_main [e:ExprA] : ExprA :=
 Definition distrib [e:ExprA] : ExprA := (distrib_main (distrib_EAopp e)).
 
 Lemma distrib_mult_right_correct:
-  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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.
@@ -436,7 +435,7 @@ Rewrite AmultT_sym;Rewrite AmultT_AplusT_distr;
 Save.
 
 Lemma distrib_mult_left_correct:
-  (e1,e2:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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.
@@ -457,7 +456,7 @@ Rewrite distrib_mult_right_correct;Simpl;Apply AmultT_sym.
 Save.
 
 Lemma distrib_correct:
-  (e:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (distrib e))=(interp_ExprA lvar e).
 Proof.
 Induction e;Intros;Auto.
@@ -472,7 +471,7 @@ Save.
 (**** Multiplication by the inverse product ****)
 
 Lemma mult_eq:
-  (e1,e2,a:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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).
@@ -496,7 +495,7 @@ Definition multiply [e:ExprA] : ExprA :=
   end.
 
 Lemma multiply_aux_correct:
-  (a,e:ExprA)(lvar:(listT (Sprod AT nat)))
+  (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.
@@ -505,7 +504,7 @@ Induction e;Simpl;Intros;Try (Rewrite merge_mult_correct);Auto.
 Save.
 
 Lemma multiply_correct:
-  (e:ExprA)(lvar:(listT (Sprod AT nat)))
+  (e:ExprA)(lvar:(listT (prodT AT nat)))
     (interp_ExprA lvar (multiply e))=(interp_ExprA lvar e).
 Proof.
   Induction e;Simpl;Auto.
@@ -553,7 +552,7 @@ Fixpoint inverse_simplif [a,e:ExprA] : ExprA :=
   end.
 
 Lemma monom_remove_correct:(e,a:ExprA)
-  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)=AzeroT)->
+  (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.
@@ -580,7 +579,7 @@ Unfold monom_remove;Case (eqExprA (EAvar n) (EAinv a));Intros;
 Save.
 
 Lemma monom_simplif_rem_correct:(a,e:ExprA)
-  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)=AzeroT)->
+  (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.
@@ -592,7 +591,7 @@ Ring.
 Save.
 
 Lemma monom_simplif_correct:(e,a:ExprA)
-  (lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)=AzeroT)->
+  (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.
@@ -602,7 +601,7 @@ Simpl;Trivial.
 Save.
 
 Lemma inverse_correct:
-  (e,a:ExprA)(lvar:(listT (Sprod AT nat)))~((interp_ExprA lvar a)=AzeroT)->
+  (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.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index c1ba413f05..0c908e1ad8 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -140,14 +140,13 @@ END
 let field g =
   Library.check_required_library ["Coq";"field";"Field"];
   let ist = { lfun=[]; lmatch=[]; debug=get_debug () } in
-  let typ = constr_of_VConstr (pf_env g) (val_interp ist g
-    <:tactic< Match Context With [|- (eq ?1 ? ?)] -> ?1>>) in
+  let typ = 
+    match Hipattern.match_with_equation (pf_concl g) with
+      | Some (eq,t::args) when eq = Coqlib.build_coq_eq_data.Coqlib.eq () -> t
+      | _ -> error "The statement is not built from Leibniz' equality" in
   let th = VConstr (lookup typ) in
   (tac_interp [(id_of_string "FT",th)] [] (get_debug ())
-    <:tactic<
-      Match Context With
-      | [|- (eq ?1 ?2 ?3)] -> Field_Gen FT
-      | _ -> Fail 1 "Field: not an equality">>) g
+    <:tactic< Match Context With [|-(eq ?1 ?2 ?3)] -> Field_Gen FT>>) g
 
 (* Verifies that all the terms have the same type and gives the right theory *)
 let guess_theory env evc = function