diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /test-suite/micromega/rexample.v | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 |