Micromega : bugs fixes - renaming of tactics - documentation

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

7 files changed, 103 insertions, 67 deletions

diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v
index 6951fcd33..8e9c0c6de 100644
--- a/test-suite/micromega/bertot.v
+++ b/test-suite/micromega/bertot.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Micromegatac.
+Require Import Psatz.
 
 Open Scope Z_scope.
 
@@ -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.
-  micromega Z.
+  psatz Z.
 Qed.
 
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index dc78ace5d..23bea439a 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Micromegatac.
+Require Import Psatz.
 Require Import Ring_normalize.
 Open Scope Z_scope.
 Require Import ZMicromega.
@@ -19,7 +19,7 @@ Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
   intros.
-  zfarkas. 
+  lia. 
 Qed.
 
 
@@ -28,14 +28,14 @@ Qed.
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
   intros. 
-  micromega Z. 
+  psatz Z. 
 Qed.
 
 
 Lemma Zdiscr: forall a b c x, 
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 
@@ -43,7 +43,7 @@ Lemma plus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  zfarkas.
+  lia.
 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; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma pol3: forall x y, 0 <= x + y ->  
   x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 
@@ -96,7 +96,7 @@ Proof.
   generalize (H8 _ _ _ (conj H5 H4)).
   generalize (H10 _ _ _ (conj H5 H4)).
   generalize rho_ge.
-  micromega Z.
+  psatz Z.
 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; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_pos_zero: forall x y,
   x > 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_pos_neg: forall x y,
   x > 0 -> y < 0 -> x*y < 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_zer_pos: forall x y,
   x = 0 -> y > 0 -> x*y = 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_zero_zero: forall x y,
   x = 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_zero_neg: forall x y,
   x = 0 -> y < 0 -> x*y = 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_neg_pos: forall x y,
   x < 0 -> y > 0 -> x*y < 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_neg_zero: forall x y,
   x < 0 -> y = 0 -> x*y = 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma sign_neg_neg: forall x y,
   x < 0 -> y < 0 -> x*y > 0.
 Proof.
-  intros; micromega Z.
+  intros; psatz Z.
 Qed.
 
 
@@ -161,26 +161,26 @@ Qed.
 Lemma binomial : forall x y, (x+y)^2 = x^2 + 2*x*y + y^2.
 Proof.
   intros.
-  zfarkas.
+  lia.
 Qed.
 
 Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
 Proof.
   intros.
-  micromega Z.
+  psatz Z.
 Qed.
 
 
 Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
 Proof.
   intros.
-  micromega Z.
+  psatz Z.
 Qed.
 
 
 Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 (* Found in Parrilo's talk *)
@@ -188,10 +188,9 @@ Qed.
 Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
 Proof.
   intros.
-  micromega Z.
+  psatz Z.
 Qed.
 
-
 (* from hol_light/Examples/sos.ml *)
 
 Lemma hol_light1 : forall a1 a2 b1 b2,
@@ -199,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 ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 
 Lemma hol_light2 : forall x a,
         3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
 Proof.
- intros ; micromega Z.
+ intros ; psatz Z.
 Qed.
 
 Lemma hol_light3 : forall b a c x,
   b ^ 2 < 4 * a * c -> (a * x ^2  + b * x + c = 0) -> False.
 Proof.
-intros ; micromega Z.
+intros ; psatz Z.
 Qed.
 
 Lemma hol_light4 : forall a c b x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
 Proof.
-intros ; micromega Z.
+intros ; psatz Z.
 Qed.
 
 Lemma hol_light5 : forall x y,
@@ -228,7 +227,7 @@ Lemma hol_light5 : forall x y,
       x ^ 2 + (y - 1) ^ 2 < 1 \/
       (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
 Proof.
-intros; micromega Z.
+intros; psatz Z.
 Qed.
 
 
@@ -237,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 ; micromega Z.
+intros ; psatz Z.
 Qed.
 
 Lemma hol_light8 : forall x y z,
  x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 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;micromega Z.
+  intros; psatz Z.
 Qed.
 
 Lemma hol_light10 : forall x y,
  x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 Lemma hol_light11 : forall x y,
  x > 1 /\ y > 1 -> x * y > x + y - 1.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 
@@ -274,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 ; micromega Z.
+  unfold e ; intros ; psatz Z.
 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 ;micromega Z.
+  intros ;psatz Z.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -292,20 +291,20 @@ Lemma hol_light16 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x + y <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 Lemma hol_light17 : forall x y,
   0 <= x /\ 0 <= y /\ (x * y = 1)
    -> x * y * (x + y) <= x ^ 2 + y ^ 2.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 Lemma hol_light18 : forall x y,
   0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
 Proof.
-  intros ; micromega Z.
+  intros ; psatz Z.
 Qed.
 
 (* ------------------------------------------------------------------------- *)
@@ -314,13 +313,13 @@ Qed.
 
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
-  intros ; zfarkas.
+  intros ; lia.
 Qed.
 
 Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
 Proof.
   intros.
-  micromega Z.
+  psatz Z.
 Qed.
 
 
@@ -329,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.
-  micromega Z.
+  psatz Z.
 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.
@@ -343,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).
-  micromega Z.
+  psatz Z.
 Qed.
diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v
index ec88b68dd..0298303f5 100644
--- a/test-suite/micromega/heap3_vcgen_25.v
+++ b/test-suite/micromega/heap3_vcgen_25.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Micromegatac.
+Require Import Psatz.
 
 Open Scope Z_scope.
 
@@ -34,5 +34,5 @@ Lemma vcgen_25 : forall
   (H13 : 0 <= 121 * i + 810 * j + -7465 * m + 64350),
   (1 = -2 * i + it).
 Proof.
-  intros ; zfarkas.
+  intros ; lia.
 Qed.
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 42aff5a47..cdecebfcd 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -6,7 +6,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Micromegatac.
+Require Import Psatz.
 Require Import QArith.
 Require Import Ring_normalize.
 
@@ -14,7 +14,7 @@ Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
-  omicron Q.
+  psatzl Q.
 Qed.
 
 (* Other (simple) examples *)
@@ -23,13 +23,13 @@ Open Scope Q_scope.
 Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2).
 Proof.
   intros.
-  omicron Q.
+  psatzl Q.
 Qed.
 
 
 Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m.
 Proof.
-  intros ; omicron Q.
+  intros ; psatzl Q.
 Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
@@ -58,5 +58,19 @@ Lemma vcgen_25 : forall
   (( 1# 1) == (-2 # 1) * i + it).
 Proof.
   intros.
-  omicron Q.
+  psatzl Q.
 Qed.
+
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+Proof.
+  intros.
+  psatz Q 2.
+Qed.
+
+Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 # 1) *x^2*y^2) >= 0.
+Proof.
+  intros ; sos Q.
+Qed.
+
+
+
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 5132dc4ef..5738ebbff 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -6,7 +6,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Micromegatac.
+Require Import Psatz.
 Require Import Reals.
 Require Import Ring_normalize.
 
@@ -16,7 +16,7 @@ Lemma plus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  omicron R.
+  psatzl R.
 Qed.
 
 (* Other (simple) examples *)
@@ -24,13 +24,13 @@ Qed.
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
 Proof.
   intros.
-  omicron R.
+  psatzl R.
 Qed.
 
 
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
-  intros ; omicron R.
+  intros ; psatzl R.
 Qed.
 
 
@@ -58,5 +58,26 @@ Lemma vcgen_25 : forall
   (( 1 ) = (-2  ) * i + it).
 Proof.
   intros.
-  omicron R.
+  psatzl R.
+Qed.
+
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+Proof.
+  intros.
+  psatz R 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.
+Proof.
+  intros ; sos R.
+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.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 30c72e8c1..5594afbb9 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -6,12 +6,12 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import ZArith Zwf Micromegatac QArith.
+Require Import ZArith Zwf Psatz QArith.
 Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; micromega Z.
+ intros ; case (Zabs_dec x) ; intros ; psatz Z.
 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' ; micromega Z).
+  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z).
 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; micromega Z).
-assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by micromega Z.
+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.
 apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
 Qed.
 
@@ -44,7 +44,9 @@ Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z.
 Proof.
   intros.
   destruct x.
-  cbv beta  iota zeta delta - [Pmult].
+  simpl.
+  unfold Zpower_pos.
+  simpl.
   rewrite Pmult_1_r.
   reflexivity.
 Qed.
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index b13654d69..2b40f6c93 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -1,27 +1,27 @@
 Require Import ZArith.
-Require Import Micromegatac.
+Require Import Psatz.
 Open Scope Z_scope.
 
 Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
 Proof.
   intros.
-  omicron Z.
+  lia.
 Qed.
 
 Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False.
 Proof.
   intros.
-  omicron Z.
+  lia.
 Qed.
 
 Lemma two_x_y_z_eq_1 : forall x y z, 2 * x + 2 * y + 2 * z= 1 -> False.
 Proof.
   intros.
-  omicron Z.
+  lia.
 Qed.
 
 Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> 7 * x - 9 * y = 4 -> -10 <= 7 * x - 9 * y <= 4 -> False.
 Proof.
   intros ; intuition auto.
-  omicron Z.
+  lia.
 Qed.