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, 113 insertions, 38 deletions

diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 25e4a09fa0..d70bb809c6 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -12,25 +12,48 @@ Open Scope Z_scope.
 Require Import ZMicromega.
 Require Import VarMap.
 
-(* false in Q : x=1/2 and n=1 *)
-
 Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
   intros.
-  lia.
+  psatz Z 2.
 Qed.
 
 
+
 (* From Laurent Théry *)
 
-Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+  intros.
+  psatz Z 2.
+Qed.
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+  intros.
+  psatz Z 2.
+Qed.
+
+Goal forall (x y : Z), 2*x = 0 -> x * y = 0.
 Proof.
   intros.
   psatz Z 2.
 Qed.
 
 
+Goal forall (x y: Z), - x*x >= 0 -> x * y = 0.
+Proof.
+  intros.
+  psatz Z 4.
+Qed.
+
+Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Proof.
+  intros.
+  psatz Z 2.
+Qed.
+
 Lemma Zdiscr: forall a b c x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
@@ -42,11 +65,9 @@ Lemma plus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  lia.
+  psatz Z 1.
 Qed.
 
-
-
 Lemma mplus_minus : forall x y,
   x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
 Proof.
@@ -95,7 +116,7 @@ Proof.
   generalize (H8 _ _ _ (conj H5 H4)).
   generalize (H10 _ _ _ (conj H5 H4)).
   generalize rho_ge.
-  psatz Z 2.
+  zify; intuition subst ; psatz Z 2.
 Qed.
 
 (* Rule of signs *)
@@ -118,18 +139,12 @@ Proof.
   intros; psatz Z 2.
 Qed.
 
-Lemma sign_zer_pos: forall x y,
+Lemma sign_zero_pos: forall x y,
   x = 0 -> y > 0 -> x*y = 0.
 Proof.
   intros; psatz Z 2.
 Qed.
 
-Lemma sign_zero_zero: forall x y,
-  x = 0 -> y = 0 -> x*y = 0.
-Proof.
-  intros; psatz Z 2.
-Qed.
-
 Lemma sign_zero_neg: forall x y,
   x = 0 -> y < 0 -> x*y = 0.
 Proof.
@@ -157,12 +172,6 @@ Qed.
 
 (* Other (simple) examples *)
 
-Lemma binomial : forall x y, (x+y)^2 = x^2 + 2*x*y + y^2.
-Proof.
-  intros.
-  lia.
-Qed.
-
 Lemma product : forall x y, x >= 0 -> y >= 0 -> x * y >= 0.
 Proof.
   intros.
@@ -170,13 +179,6 @@ Proof.
 Qed.
 
 
-Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
-Proof.
-  intros.
-  psatz Z 2.
-Qed.
-
-
 Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
 Proof.
   intros ; psatz Z 2.
@@ -229,8 +231,6 @@ Proof.
 intros; psatz Z 3.
 Qed.
 
-
-
 Lemma hol_light7 : forall x y z,
  0<= x /\ 0 <= y /\ 0 <= z /\ x + y + z <= 3
   -> x * y + x * z + y * z >= 3 * x * y * z.
@@ -251,6 +251,7 @@ Proof.
   intros; psatz Z 2.
 Qed.
 
+
 Lemma hol_light10 : forall x y,
  x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
 Proof.
@@ -275,6 +276,7 @@ Proof.
   unfold e ; intros ; psatz Z 2.
 Qed.
 
+
 Lemma hol_light14 : forall x y z,
  2 <= x /\ x <= 4 /\ 2 <= y /\ y <= 4 /\ 2 <= z /\ z <= 4
   -> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z).
@@ -300,6 +302,7 @@ Proof.
   intros ; psatz Z 3.
 Qed.
 
+
 Lemma hol_light18 : forall x y,
   0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
 Proof.
@@ -310,18 +313,12 @@ Qed.
 (* Some examples over integers and natural numbers.                          *)
 (* ------------------------------------------------------------------------- *)
 
-Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
-Proof.
-  intros ; lia.
-Qed.
-
 Lemma hol_light22 : forall n, n >= 0 -> n <= n * n.
 Proof.
   intros.
   psatz Z 2.
 Qed.
 
-
 Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
   ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
                 -> (x1 + y1 = x2 + y2).
@@ -336,11 +333,89 @@ Proof.
   psatz Z 1.
 Qed.
 
-
-
 Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2)  >= 0.
 Proof.
   intros.
   generalize (motzkin' x y).
   psatz Z 8.
 Qed.
+
+(** Other tests *)
+
+Goal forall x y z n,
+    y >= z /\ y = n \/ ~ y >= z /\ z = n ->
+    x >= y /\
+    (x >= z /\ (x >= n /\ x = x \/ ~ x >= n /\ x = n) \/
+               ~ x >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)) \/
+    ~ x >= y /\
+    (y >= z /\ (x >= n /\ y = x \/ ~ x >= n /\ y = n) \/
+               ~ y >= z /\ (x >= n /\ z = x \/ ~ x >= n /\ z = n)).
+Proof.
+  intros.
+  psatz Z 2.
+Qed.
+
+(** Incompeteness: require manual case split *)
+Goal forall (z0 z z1 z2 z3 z5 :Z)
+(H8 : 0 <= z2)
+(H5 : z5 > 0)
+(H0 : z0 > 0)
+(H9 : z2 < z0)
+(H1 : z0 * z5 > 0)
+(H10 : 0 <= z1 * z0 + z0 * z5 - 1 - z0 * z5 * z)
+(H11 : z1 * z0 + z0 * z5 - 1 - z0 * z5 * z < z0 * z5)
+(H6 : 0 <= z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3)
+(H7 : z0 * z1 + z2 - z0 + 1 + z0 * z5 - 1 - z0 * z5 * z3 < z0 * z5)
+(C : z > z3), False.
+Proof.
+  intros.
+  assert (z1 - z5 * z3 - 1 < 0) by psatz Z 3.
+  psatz Z 3.
+Qed.
+
+Goal forall
+    (d sz x n : Z)
+    (GE : sz * x - sz * d >=1 )
+    (R  : sz + d * sz - sz * x >= 1),
+    False.
+Proof.
+  intros.
+  assert (x - d >= 1) by psatz Z 3.
+  psatz Z 3.
+Qed.
+
+
+Goal forall x6 x8 x9 x10 x11 x12 x13 x14,
+    x6  >= 0 ->
+    -x6 + x8 + x9 + -x10  >= 1 ->
+    x8  >= 0 ->
+    x11  >= 0 ->
+    -x11 + x12 + x13 + -x14  >= 1 ->
+    x6 + -4*x8 + -2*x9 + 3*x10 + x11 + -4*x12 + -2*x13 + 3*x14  >= -5 ->
+    x10  >= 0 ->
+    x14  >= 0 ->
+    x12  >= 0 ->
+    x8 + -x10 + x12 + -x14  >= 1 ->
+ False.
+Proof.
+  intros.
+  psatz Z 1.
+Qed.
+
+Goal forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12,
+x2 + -1*x4 >= 0 ->
+-2*x2 + x4 >= -1 ->
+x1 + x3 + x4 + -1*x7 + -1*x11 >= 1 ->
+-1*x2 + x8 + x10 >= 0 ->
+-2*x3 + -2*x4 + x5 + 2*x6 + x9 >= -1 ->
+-2*x1 + 3*x3 + x4 + -1*x7 + -1*x11 >= 0 ->
+-2*x1 + x3 + x4 + -1*x8 + -1*x10 + 2*x12 >= 0 ->
+-2*x2 + x3 + x4 + -1*x7 + -1*x11 + 2*x12 >= 0 ->
+-2*x2 + x3 + 3*x4 + -1*x8 + -1*x10 >= 0 ->
+2*x2 + -1*x3 + -1*x4 + x5 + 2*x6 + -2*x8 + x9 + -2*x10 >= 0 ->
+x1 + -2*x3 + x7 + x11 + -2*x12 >= 0 ->
+ False.
+Proof.
+  intros.
+  psatz Z 1.
+Qed.