diff options
Diffstat (limited to 'test-suite/micromega/example.v')
-rw-r--r-- | test-suite/micromega/example.v | 72 |
1 files changed, 36 insertions, 36 deletions
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. |