Refactoring of Micromega code using a Simplex linear solver

- Simplex based linear prover
  Unset Simplex to get Fourier elimination
  For lia and nia, do not enumerate but generate cutting planes.
- Better non-linear support
  Factorisation of the non-linear pre-processing
  Careful handling of equation x=e, x is only eliminated if x is used linearly
- More opaque interfaces
  (Linear solvers Simplex and Mfourier are independent)
- Set Dump Arith "file" so that lia,nia calls generate Coq goals
  in filexxx.v. Used to collect benchmarks and regressions.
- Rationalise the test-suite
  example.v only tests psatz Z
  example_nia.v only tests lia, nia
  In both files, the tests are in essence the same.
  In particular, if a test is solved by psatz but not by nia,
  we finish the goal by an explicit Abort.
  There are additional tests in example_nia.v which require specific
  integer reasoning out of scope of psatz.

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index bd52270100..52dc9ed2e0 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -72,6 +72,14 @@ Proof.
   psatz R 3.
 Qed.
 
+Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+Proof.
+  intros.
+  nra.
+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 2.
@@ -86,3 +94,24 @@ Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
 Proof.
   lra.
 Qed.
+
+(* From L. Théry *)
+
+Goal forall (x y : R), x = 0 -> x * y = 0.
+Proof.
+  intros.
+  nra.
+Qed.
+
+Goal forall (x y : R), 2*x = 0 -> x * y = 0.
+Proof.
+  intros.
+  nra.
+Qed.
+
+
+Goal forall (x y: R), - x*x >= 0 -> x * y = 0.
+Proof.
+  intros.
+  nra.
+Qed.