Improved robustness of micromega parser. Proof search of Micromega test-suites is now bounded -- ensure termination

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

5 files changed, 46 insertions, 49 deletions

diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
index 8e9c0c6de..bcf222f92 100644
--- a/test-suite/micromega/bertot.v
+++ b/test-suite/micromega/bertot.v
@@ -17,6 +17,6 @@ Goal (forall x y n,
   (x < n /\ x <= n /\ 2 * y = x * (x+1) -> x + 1 <= n /\ 2 *(x+1+y) = (x+1)*(x+2))).
 Proof.
   intros.
-  psatz Z.
+  psatz Z 3.
 Qed.
 
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 23bea439a..905b9a938 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -28,14 +28,14 @@ Qed.
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
   intros. 
-  psatz Z. 
+  psatz Z 2. 
 Qed.
 
 
 Lemma Zdiscr: forall a b c x, 
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 
@@ -51,13 +51,13 @@ Qed.
 Lemma mplus_minus : forall x y, 
   x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma pol3: forall x y, 0 <= x + y ->  
   x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 4.
 Qed.
 
 
@@ -96,7 +96,7 @@ Proof.
   generalize (H8 _ _ _ (conj H5 H4)).
   generalize (H10 _ _ _ (conj H5 H4)).
   generalize rho_ge.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 (* Rule of signs *)
@@ -104,55 +104,55 @@ Qed.
 Lemma sign_pos_pos: forall x y,
   x > 0 -> y > 0 -> x*y > 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_pos_zero: forall x y,
   x > 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_pos_neg: forall x y,
   x > 0 -> y < 0 -> x*y < 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zer_pos: forall x y,
   x = 0 -> y > 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zero_zero: forall x y,
   x = 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_zero_neg: forall x y,
   x = 0 -> y < 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_pos: forall x y,
   x < 0 -> y > 0 -> x*y < 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_zero: forall x y,
   x < 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma sign_neg_neg: forall x y,
   x < 0 -> y < 0 -> x*y > 0.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 
@@ -167,20 +167,20 @@ Qed.
 Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
 Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
 Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 (* Found in Parrilo's talk *)
@@ -188,7 +188,7 @@ Qed.
 Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 (* from hol_light/Examples/sos.ml *)
@@ -198,26 +198,26 @@ Lemma hol_light1 : forall a1 a2 b1 b2,
    (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> 
    (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 
 Lemma hol_light2 : forall x a,
         3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
 Proof.
- intros ; psatz Z.
+ intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light3 : forall b a c x,
   b ^ 2 < 4 * a * c -> (a * x ^2  + b * x + c = 0) -> False.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 4.
 Qed.
 
 Lemma hol_light4 : forall a c b x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 4.
 Qed.
 
 Lemma hol_light5 : forall x y,
@@ -227,7 +227,7 @@ Lemma hol_light5 : forall x y,
       x ^ 2 + (y - 1) ^ 2 < 1 \/
       (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
 Proof.
-intros; psatz Z.
+intros; psatz Z 3.
 Qed.
 
 
@@ -236,32 +236,32 @@ Lemma hol_light7 : forall x y z,
  0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
   -> x * y + x * z + y * z >= 3 * x * y * z.
 Proof.
-intros ; psatz Z.
+intros ; psatz Z 3.
 Qed.
 
 Lemma hol_light8 : forall x y z,
  x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light9 : forall w x y z,
  w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
   -> (w + x + y + z) ^ 2 <= 4.
 Proof.
-  intros; psatz Z.
+  intros; psatz Z 2.
 Qed.
 
 Lemma hol_light10 : forall x y,
  x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light11 : forall x y,
  x > 1 /\ y > 1 -> x * y > x + y - 1.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 
@@ -273,14 +273,14 @@ Lemma hol_light12: forall x y z,
 Proof.
   intros x y z ; set (e:= (125841 / 50000)).
   compute in e.
-  unfold e ; intros ; psatz Z.
+  unfold e ; intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light14 : forall x y z,
  2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
   -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
 Proof.
-  intros ;psatz Z.
+  intros ;psatz Z 2.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -291,20 +291,20 @@ Lemma hol_light16 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x + y <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 2.
 Qed.
 
 Lemma hol_light17 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x * y * (x + y) <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 3.
 Qed.
 
 Lemma hol_light18 : forall x y,
   0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
 Proof.
-  intros ; psatz Z.
+  intros ; psatz Z 4.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -319,7 +319,7 @@ Qed.
 Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 
@@ -328,7 +328,7 @@ Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0
                 -> (x1 + y1 = x2 + y2).
 Proof.
   intros.
-  psatz Z.
+  psatz Z 2.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
@@ -342,5 +342,5 @@ Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2)  >= 0.
 Proof.
   intros.
   generalize (motzkin' x y).
-  psatz Z.
+  psatz Z 8.
 Qed.
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index cdecebfcd..8a349a1d9 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -17,6 +17,9 @@ Proof.
   psatzl Q.
 Qed.
 
+
+
+
 (* Other (simple) examples *)
 Open Scope Q_scope.
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 5738ebbff..1de1955db 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -12,7 +12,7 @@ Require Import Ring_normalize.
 
 Open Scope R_scope.
 
-Lemma plus_minus : forall x y, 
+Lemma yplus_minus : forall x y, 
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -74,10 +74,4 @@ Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
 intros; split_Rabs; psatzl R.
-Qed.
- 
-Lemma l2 :
- forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
-intros.
-split_Rabs; psatzl R.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 5594afbb9..b78bba25c 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,7 +11,7 @@ Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; psatz Z.
+ intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
 Qed.
 Hint Resolve Zabs_pos Zabs_square.
 
@@ -21,11 +21,11 @@ intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
 assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
          /\ Zabs p^2 = p^2) by auto.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by 
-  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z).
+  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
 intros n IHn p [Hn [Hp Heq]].
-assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z).
-assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z.
+assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z 2).
+assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z 2.
 apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
 Qed.