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/qexample.v | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'test-suite/micromega/qexample.v')
-rw-r--r-- | test-suite/micromega/qexample.v | 27 |
1 files changed, 22 insertions, 5 deletions
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. + + + |