moins de reification inutile, noatations standards

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

8 files changed, 101 insertions, 90 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index ef1701c9f..9a0c9090f 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -27,6 +27,7 @@ Require Export Ncring.
 Require Export Ncring_initial.
 Require Export Ncring_tac.
 Require Export Integral_domain.
+Require Import DiscrR.
 
 Declare ML Module "nsatz_plugin".
 
@@ -250,9 +251,10 @@ End nsatz1.
 
 Ltac equality_to_goal H x y:=
   let h := fresh "nH" in
+  (* eliminate trivial  hypotheses, but it takes time!:
     (assert (h:equality x y);
     [solve [cring] | clear H; clear h])
-  || (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
+  || *) (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
 .
 
 Ltac equalities_to_goal :=
@@ -341,31 +343,36 @@ Ltac get_lpol g :=
   end.
 
 Ltac nsatz_generic radicalmax info lparam lvar :=
-match goal with
-  |- ?g => let lb := lterm_goal g in
-(*     idtac "lb"; idtac lb;*)
-     match eval red in (list_reifyl (lterm:=lb)) with
-     | (?fv, ?le) => 
-        let fv := match lvar with
-                     (@nil _) => fv
-                    | _ => lvar
-                  end in
-(*         idtac "variables:";idtac fv;*)
-        let nparam := eval compute in (Z_of_nat (List.length lparam)) in
-        let fv := parametres_en_tete fv lparam in
-(*        idtac "variables:"; idtac fv;
-        idtac "nparam:"; idtac nparam; *)
-        match eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) with
-          | (?fv, ?le) => 
-(*              idtac "variables:";idtac fv; idtac le; idtac lb;*)
-              reify_goal fv le lb;
-                match goal with 
+ let nparam := eval compute in (Z_of_nat (List.length lparam)) in
+ match goal with
+  |- ?g => let lb := lterm_goal g in 
+     match (match lvar with
+              |(@nil _) =>
+                 match lparam with
+                   |(@nil _) =>
+                     let r := eval red in (list_reifyl (lterm:=lb)) in r
+                   |_ =>
+                     match eval red in (list_reifyl (lterm:=lb)) with
+                       |(?fv, ?le) =>
+                         let fv := parametres_en_tete fv lparam in
+                           (* we reify a second time, with the good order
+                              for variables *)
+                         let r := eval red in 
+                                  (list_reifyl (lterm:=lb) (lvar:=fv)) in r
+                     end
+                  end
+              |_ => 
+                let fv := parametres_en_tete lvar lparam in
+                let r := eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) in r
+            end) with
+          |(?fv, ?le) => 
+            reify_goal fv le lb ;
+            match goal with 
                    |- ?g => 
                        let lp := get_lpol g in 
                        let lpol := eval compute in (List.rev lp) in
-(*                       idtac "polynomes:"; idtac lpol;*)
-                       (*simpl;*) intros;
-  (*simpl;*)
+                       intros;
+
   let SplitPolyList kont :=
     match lpol with
     | ?p2::?lp2 => kont p2 lp2
@@ -397,12 +404,15 @@ match goal with
             try trivial;
             try exact integral_domain_one_zero;
             try exact integral_domain_minus_one_zero
+          || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
+                     one, one_notation, multiplication, mul_notation, zero, zero_notation;
+                     discrR || omega]) 
           || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]
 ) 
 )
-end end end end .
+end end end .
 
 Ltac nsatz_default:=
   intros;
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
index 5b566dbb0..e896554ea 100644
--- a/plugins/setoid_ring/Algebra_syntax.v
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -23,27 +23,3 @@ Notation "[ x ]" := (bracket(x)).
 Class Power {A B: Type} := power : A -> B -> A.
 Notation "x ^ y" := (power x y).
 
-
-Notation "\/ x y z ,  P" := (forall x y z, P)
-   (at level 200, x ident, y ident, z ident).
-Notation "\/ x y ,  P" := (forall x y, P)
-   (at level 200, x ident, y ident).
-Notation "\/ x , P" := (forall x, P)(at level 200, x ident).
-
-Notation "\/ x y z : T ,  P" := (forall x y z : T, P)
-   (at level 200, x ident, y ident, z ident).
-Notation "\/ x y  : T ,  P" := (forall x y : T, P)
-   (at level 200, x ident, y ident).
-Notation "\/ x  : T , P" := (forall x : T, P)(at level 200, x ident).
-
-Notation "\ x y z , P" := (fun x y z => P)
-   (at level 200, x ident, y ident, z ident).
-Notation "\ x y ,  P" := (fun x y => P)
-   (at level 200, x ident, y ident).
-Notation "\ x , P" := (fun x => P)(at level 200, x ident).
-
-Notation "\ x y z : T , P" := (fun x y z : T => P)
-   (at level 200, x ident, y ident, z ident).
-Notation "\ x y : T ,  P" := (fun x y : T => P)
-   (at level 200, x ident, y ident).
-Notation "\ x : T , P" := (fun x : T => P)(at level 200, x ident).
diff --git a/plugins/setoid_ring/Ncring.v b/plugins/setoid_ring/Ncring.v
index 5b6987d01..9a30fa47e 100644
--- a/plugins/setoid_ring/Ncring.v
+++ b/plugins/setoid_ring/Ncring.v
@@ -40,16 +40,16 @@ Class Ring `{Ro:Ring_ops}:={
  ring_mult_comp: Proper (_==_ ==> _==_ ==>_==_) _*_;
  ring_sub_comp: Proper (_==_ ==> _==_ ==>_==_) _-_;
  ring_opp_comp: Proper (_==_==>_==_) -_;
- ring_add_0_l    : \/x, 0 + x == x;
- ring_add_comm   : \/x y, x + y == y + x;
- ring_add_assoc  : \/x y z, x + (y + z) == (x + y) + z;
- ring_mul_1_l    : \/x, 1 * x == x;
- ring_mul_1_r    : \/x, x * 1 == x;
- ring_mul_assoc  : \/x y z, x * (y * z) == (x * y) * z;
- ring_distr_l    : \/x y z, (x + y) * z == x * z + y * z;
- ring_distr_r    : \/x y z, z * ( x + y) == z * x + z * y;
- ring_sub_def    : \/x y, x - y == x + -y;
- ring_opp_def    : \/x, x + -x == 0
+ ring_add_0_l    : forall x, 0 + x == x;
+ ring_add_comm   : forall x y, x + y == y + x;
+ ring_add_assoc  : forall x y z, x + (y + z) == (x + y) + z;
+ ring_mul_1_l    : forall x, 1 * x == x;
+ ring_mul_1_r    : forall x, x * 1 == x;
+ ring_mul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
+ ring_distr_l    : forall x y z, (x + y) * z == x * z + y * z;
+ ring_distr_r    : forall x y z, z * ( x + y) == z * x + z * y;
+ ring_sub_def    : forall x y, x - y == x + -y;
+ ring_opp_def    : forall x, x + -x == 0
 }.
 (* inutile! je sais plus pourquoi j'ai mis ca...
 Instance ring_Ring_ops(R:Type)`{Ring R}
@@ -94,11 +94,11 @@ Instance power_ring {R:Type}`{Ring R} : Power:=
 Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}`{Rh:Bracket C R}:= {
     ring_morphism0    : [0] == 0;
     ring_morphism1    : [1] == 1;
-    ring_morphism_add : \/x y, [x + y] == [x] + [y];
-    ring_morphism_sub : \/x y, [x - y] == [x] - [y];
-    ring_morphism_mul : \/x y, [x * y] == [x] * [y];
-    ring_morphism_opp : \/ x, [-x] == -[x];
-    ring_morphism_eq  : \/x y, x == y -> [x] == [y]}.
+    ring_morphism_add : forall x y, [x + y] == [x] + [y];
+    ring_morphism_sub : forall x y, [x - y] == [x] - [y];
+    ring_morphism_mul : forall x y, [x * y] == [x] * [y];
+    ring_morphism_opp : forall  x, [-x] == -[x];
+    ring_morphism_eq  : forall x y, x == y -> [x] == [y]}.
 
 Section Ring.
 
@@ -106,7 +106,7 @@ Context {R:Type}`{Rr:Ring R}.
 
 (* Powers *)
 
- Lemma pow_pos_comm : \/ x j,  x * pow_pos x j == pow_pos x j * x.
+ Lemma pow_pos_comm : forall  x j,  x * pow_pos x j == pow_pos x j * x.
 induction j; simpl. rewrite <- ring_mul_assoc.
 rewrite <- ring_mul_assoc. 
 rewrite <- IHj. rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
@@ -116,7 +116,7 @@ rewrite ring_mul_assoc. rewrite IHj.
 rewrite <- ring_mul_assoc. rewrite IHj. reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Psucc : \/ x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Lemma pow_pos_Psucc : forall  x j, pow_pos x (Psucc j) == x * pow_pos x j.
  Proof.
   induction j; simpl. 
   rewrite IHj. 
@@ -127,7 +127,7 @@ rewrite <- ring_mul_assoc. reflexivity.
 reflexivity. reflexivity.
 Qed.
 
- Lemma pow_pos_Pplus : \/ x i j,
+ Lemma pow_pos_Pplus : forall  x i j,
    pow_pos x (i + j) == pow_pos x i * pow_pos x j.
  Proof.
   intro x;induction i;intros.
@@ -145,7 +145,7 @@ Qed.
 
  Definition id_phi_N (x:N) : N := x.
 
- Lemma pow_N_pow_N : \/ x n, pow_N x (id_phi_N n) == pow_N x n.
+ Lemma pow_N_pow_N : forall  x n, pow_N x (id_phi_N n) == pow_N x n.
  Proof.
   intros; reflexivity.
  Qed.
@@ -159,7 +159,7 @@ Qed.
  Qed.
 *)
  (** rings are almost rings*)
- Lemma ring_mul_0_l : \/ x, 0 * x == 0.
+ Lemma ring_mul_0_l : forall  x, 0 * x == 0.
  Proof.
   intro x. setoid_replace (0*x) with ((0+1)*x + -x). 
   rewrite ring_add_0_l. rewrite ring_mul_1_l .
@@ -169,7 +169,7 @@ Qed.
   rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_mul_0_r : \/ x, x * 0 == 0.
+ Lemma ring_mul_0_r : forall  x, x * 0 == 0.
  Proof.
   intro x; setoid_replace (x*0)  with (x*(0+1) + -x).
   rewrite ring_add_0_l ; rewrite ring_mul_1_r .
@@ -180,7 +180,7 @@ Qed.
   rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_opp_mul_l : \/x y, -(x * y) == -x * y.
+ Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
  Proof.
   intros x y;rewrite <- (ring_add_0_l (- x * y)).
   rewrite ring_add_comm .
@@ -191,7 +191,7 @@ Qed.
   rewrite ring_mul_0_l;rewrite ring_add_0_l ;reflexivity.
  Qed.
 
-Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
+Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y.
  Proof.
   intros x y;rewrite <- (ring_add_0_l (x * - y)).
   rewrite ring_add_comm .
@@ -202,7 +202,7 @@ Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
   rewrite ring_mul_0_r;rewrite ring_add_0_l ;reflexivity.
  Qed.
 
- Lemma ring_opp_add : \/x y, -(x + y) == -x + -y.
+ Lemma ring_opp_add : forall x y, -(x + y) == -x + -y.
  Proof.
   intros x y;rewrite <- (ring_add_0_l  (-(x+y))).
   rewrite <- (ring_opp_def  x).
@@ -221,7 +221,7 @@ Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
   rewrite ring_add_comm; reflexivity.
  Qed.
 
- Lemma ring_opp_opp : \/ x, - -x == x.
+ Lemma ring_opp_opp : forall  x, - -x == x.
  Proof.
   intros x; rewrite <- (ring_add_0_l (- -x)).
   rewrite <- (ring_opp_def x).
@@ -230,7 +230,7 @@ Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
  Qed.
 
  Lemma ring_sub_ext :
-      \/ x1 x2, x1 == x2 -> \/ y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+      forall  x1 x2, x1 == x2 -> forall  y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
  Proof.
   intros.
   setoid_replace (x1 - y1)  with (x1 + -y1).
@@ -250,17 +250,17 @@ Lemma ring_opp_mul_r : \/x y, -(x * y) == x * -y.
      | reflexivity
      ].
 
- Lemma ring_add_0_r : \/ x, (x + 0) == x.
+ Lemma ring_add_0_r : forall  x, (x + 0) == x.
  Proof. intros; mrewrite. Qed.
 
  
- Lemma ring_add_assoc1 : \/x y z, (x + y) + z == (y + z) + x.
+ Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
  Proof.
   intros;rewrite <- (ring_add_assoc x).
   rewrite (ring_add_comm x);reflexivity.
  Qed.
 
- Lemma ring_add_assoc2 : \/x y z, (y + x) + z == (y + z) + x.
+ Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
  Proof.
   intros; repeat rewrite <- ring_add_assoc.
    rewrite (ring_add_comm x); reflexivity.
diff --git a/plugins/setoid_ring/Cring_Q.v b/plugins/setoid_ring/Rings_Q.v
index ca8439aa6..fd7654713 100644
--- a/plugins/setoid_ring/Cring_Q.v
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -1,4 +1,5 @@
 Require Export Cring.
+Require Export Integral_domain.
 
 (* Rational numbers *)
 Require Import QArith.
@@ -20,3 +21,10 @@ Defined.
 
 Instance Qcri: (Cring (Rr:=Qri)).
 red. exact Qmult_comm. Defined.
+
+Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
+unfold Qeq. simpl. auto with *. Qed.
+
+Instance Qdi : (Integral_domain (Rcr:=Qcri)). 
+constructor. 
+exact Qmult_integral. exact Q_one_zero. Defined.
diff --git a/plugins/setoid_ring/Cring_R.v b/plugins/setoid_ring/Rings_R.v
index b548aa7aa..fd219c235 100644
--- a/plugins/setoid_ring/Cring_R.v
+++ b/plugins/setoid_ring/Rings_R.v
@@ -1,4 +1,5 @@
 Require Export Cring.
+Require Export Integral_domain.
 
 (* Real numbers *)
 Require Import Reals.
@@ -23,3 +24,11 @@ Defined.
 
 Instance Rcri: (Cring (Rr:=Rri)).
 red. exact Rmult_comm. Defined.
+
+Lemma R_one_zero: 1%R <> 0%R.
+discrR.
+Qed.
+
+Instance Rdi : (Integral_domain (Rcr:=Rcri)). 
+constructor. 
+exact Rmult_integral. exact R_one_zero. Defined.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
new file mode 100644
index 000000000..889048653
--- /dev/null
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -0,0 +1,14 @@
+Require Export Cring.
+Require Export Integral_domain.
+Require Export Ncring_initial.
+
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Zmult_comm. Defined.
+
+Lemma Z_one_zero: 1%Z <> 0%Z.
+omega. 
+Qed.
+
+Instance Zdi : (Integral_domain (Rcr:=Zcri)). 
+constructor. 
+exact Zmult_integral. exact Z_one_zero. Defined.
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 4297e3a8b..580df9b55 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -19,6 +19,7 @@ Ncring.vo
 Ncring_polynom.vo
 Ncring_initial.vo
 Ncring_tac.vo
-Cring_R.vo
-Cring_Q.vo
+Rings_Z.vo
+Rings_R.vo
+Rings_Q.vo
 Integral_domain.vo
\ No newline at end of file
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 22143de13..d316e4a09 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,3 +1,4 @@
+(* compile en user    3m39.915s sur cachalot *)
 Require Import Nsatz.
 
 (* Example with a generic domain *)
@@ -214,10 +215,6 @@ Ltac geo_begin:=
   geo_split_hyps;
   scnf; proof_pol_disj.
 
-Ltac geo_end:=
-  simpl; unfold R2, addition, add_notation, multiplication, mul_notation, one, one_notation, zero, zero_notation, equality, eq_notation;
-  discrR.
-
 (* Examples *)
 
 Lemma medians: forall A B C A1 B1 C1 H:point,
@@ -300,7 +297,6 @@ Time nsatz with radicalmax :=1%N strategy:=1%Z
   variables:= (@nil R).
 (*Finished transaction in 13. secs (10.102464u,0.s)
 *)
-geo_end. 
 Qed.
 
 Lemma Pappus: forall A B C A1 B1 C1 P Q S:point,
@@ -370,7 +366,7 @@ Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point,
   \/ collinear A B C.
 Proof. geo_begin. 
 idtac "threepoints".
-Time nsatz. geo_end.  
+Time nsatz. 
 (*Finished transaction in 7. secs (6.282045u,0.s)
 *) Qed.
 
@@ -394,7 +390,7 @@ Proof. geo_begin.
 idtac "Feuerbach".
 Time nsatz. 
 (*Finished transaction in 21. secs (19.021109u,0.s)*)
-geo_end. Qed.
+Qed.
 
 
 
@@ -414,13 +410,10 @@ Proof. geo_begin.
 idtac "Euler_circle 3 goals".
 Time nsatz. 
 (*Finished transaction in 13. secs (11.208296u,0.124981s)*)
-geo_end. 
 Time nsatz.  
 (*Finished transaction in 10. secs (8.846655u,0.s)*) 
-geo_end. 
 Time nsatz. 
 (*Finished transaction in 11. secs (9.186603u,0.s)*)
-geo_end. 
 Qed.
 
 
@@ -489,7 +482,7 @@ Proof. geo_begin.
 idtac "bissectrices".
 Time nsatz.
 (*Finished transaction in 2. secs (1.937705u,0.s)*)
-geo_end. Qed.
+Qed.
 
 Lemma bisections: forall A B C A1 B1 C1 H:point,
   middle B C A1 ->  orthogonal H A1 B C ->