Intégration de micromega ("omicron" pour fourier et sa variante sur Z,

"micromega" et "sos" pour les problèmes non linéaires sous-traités à
csdp); mise en place d'un cache pour pouvoir rejouer les preuves
sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra
affiner cela).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 62 insertions, 0 deletions

diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
new file mode 100644
index 000000000..42aff5a47
--- /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.