From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/micromega/qexample.v | 62 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 test-suite/micromega/qexample.v (limited to 'test-suite/micromega/qexample.v') diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v new file mode 100644 index 00000000..42aff5a4 --- /dev/null +++ b/test-suite/micromega/qexample.v @@ -0,0 +1,62 @@ +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* *) +(************************************************************************) + +Require Import Micromegatac. +Require Import QArith. +Require Import Ring_normalize. + +Lemma plus_minus : forall x y, + 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. +Proof. + intros. + omicron 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. +Qed. + + +Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m. +Proof. + intros ; omicron Q. +Qed. +Open Scope Z_scope. +Open Scope Q_scope. + +Lemma vcgen_25 : forall + (n : Q) + (m : Q) + (jt : Q) + (j : Q) + (it : Q) + (i : Q) + (H0 : 1 * it + (-2 # 1) * i + (-1 # 1) == 0) + (H : 1 * jt + (-2 # 1) * j + (-1 # 1) == 0) + (H1 : 1 * n + (-10 # 1) = 0) + (H2 : 0 <= (-4028 # 1) * i + (6222 # 1) * j + (705 # 1) * m + (-16674 # 1)) + (H3 : 0 <= (-418 # 1) * i + (651 # 1) * j + (94 # 1) * m + (-1866 # 1)) + (H4 : 0 <= (-209 # 1) * i + (302 # 1) * j + (47 # 1) * m + (-839 # 1)) + (H5 : 0 <= (-1 # 1) * i + 1 * j + (-1 # 1)) + (H6 : 0 <= (-1 # 1) * j + 1 * m + (0 # 1)) + (H7 : 0 <= (1 # 1) * j + (5 # 1) * m + (-27 # 1)) + (H8 : 0 <= (2 # 1) * j + (-1 # 1) * m + (2 # 1)) + (H9 : 0 <= (7 # 1) * j + (10 # 1) * m + (-74 # 1)) + (H10 : 0 <= (18 # 1) * j + (-139 # 1) * m + (1188 # 1)) + (H11 : 0 <= 1 * i + (0 # 1)) + (H13 : 0 <= (121 # 1) * i + (810 # 1) * j + (-7465 # 1) * m + (64350 # 1)), + (( 1# 1) == (-2 # 1) * i + it). +Proof. + intros. + omicron Q. +Qed. -- cgit v1.2.3