From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- test-suite/micromega/bertot.v | 4 +- test-suite/micromega/example.v | 85 +++++++++++++++++------------------ test-suite/micromega/heap3_vcgen_25.v | 4 +- test-suite/micromega/qexample.v | 27 ++++++++--- test-suite/micromega/rexample.v | 27 ++++++++--- test-suite/micromega/square.v | 14 +++--- test-suite/micromega/zomicron.v | 10 ++--- 7 files changed, 102 insertions(+), 69 deletions(-) (limited to 'test-suite/micromega') diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v index 6951fcd3..bcf222f9 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 3. Qed. diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index dc78ace5..751fe91e 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 2. 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 4. 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 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; micromega Z. + intros; psatz Z 4. Qed. @@ -96,7 +96,7 @@ Proof. generalize (H8 _ _ _ (conj H5 H4)). generalize (H10 _ _ _ (conj H5 H4)). generalize rho_ge. - micromega 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; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_pos_zero: forall x y, x > 0 -> y = 0 -> x*y = 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_pos_neg: forall x y, x > 0 -> y < 0 -> x*y < 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_zer_pos: forall x y, x = 0 -> y > 0 -> x*y = 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_zero_zero: forall x y, x = 0 -> y = 0 -> x*y = 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_zero_neg: forall x y, x = 0 -> y < 0 -> x*y = 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_neg_pos: forall x y, x < 0 -> y > 0 -> x*y < 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_neg_zero: forall x y, x < 0 -> y = 0 -> x*y = 0. Proof. - intros; micromega Z. + intros; psatz Z 2. Qed. Lemma sign_neg_neg: forall x y, x < 0 -> y < 0 -> x*y > 0. Proof. - intros; micromega Z. + intros; psatz Z 2. 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 2. Qed. Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0. Proof. intros. - micromega Z. + psatz Z 2. Qed. Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 -> False. Proof. - intros ; micromega Z. + intros ; psatz Z 2. 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 2. 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 4. Qed. Lemma hol_light2 : forall x a, 3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0. Proof. - intros ; micromega 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 ; micromega 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 ; micromega Z. +intros ; psatz Z 4. 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 3. 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 3. 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 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;micromega Z. + intros; psatz Z 2. Qed. Lemma hol_light10 : forall x y, x >= 1 /\ y >= 1 -> x * y >= x + y - 1. Proof. - intros ; micromega Z. + intros ; psatz Z 2. Qed. Lemma hol_light11 : forall x y, x > 1 /\ y > 1 -> x * y > x + y - 1. Proof. - intros ; micromega Z. + intros ; psatz Z 2. 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 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 ;micromega Z. + intros ;psatz Z 2. 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 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 ; micromega 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 ; micromega Z. + intros ; psatz Z 4. 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 2. Qed. @@ -329,12 +328,12 @@ 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 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 Z. + intros ; psatz Z. Qed. @@ -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 8. Qed. diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v index ec88b68d..0298303f 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 42aff5a4..1fa250e0 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,22 +14,25 @@ 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 *) 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 +61,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 ; psatz Q. +Qed. + + + diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 5132dc4e..d7386a4e 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -6,17 +6,17 @@ (* *) (************************************************************************) -Require Import Micromegatac. +Require Import Psatz. Require Import Reals. 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. - 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,20 @@ 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 ; psatz R. +Qed. + +Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). +intros; split_Rabs; psatzl R. +Qed. \ No newline at end of file diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 30c72e8c..b78bba25 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 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' ; micromega 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; 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 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. @@ -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 b13654d6..2b40f6c9 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. -- cgit v1.2.3