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