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.

5 files changed, 928 insertions, 43 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.
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
new file mode 100644
index 0000000000..8de631aa6a
--- /dev/null
+++ b/test-suite/micromega/example_nia.v
@@ -0,0 +1,503 @@
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import ZArith.
+Require Import Psatz.
+Open Scope Z_scope.
+Require Import ZMicromega.
+Require Import VarMap.
+
+(* false in Q : x=1/2 and n=1 *)
+
+Lemma int_not_rat : forall x, 2 * x = 1 -> False.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
+Lemma not_so_easy : forall x n : Z,
+  2*x + 1 <= 2 *n -> x <= n-1.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall a1 da na b1 db nb,
+    a1 * da = na ->
+    b1 * db = nb  ->
+    a1 * b1 *  da * db = na * nb.
+Proof.
+  intros.
+  nia.
+Qed.
+
+(* From Laurent Théry *)
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+Goal forall (x y : Z), x = 0 -> x * y = 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+Goal forall (x y : Z), 2*x = 0 -> x * y = 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Goal forall (x y: Z), - x*x >= 0 -> x * y = 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Lemma Zdiscr: forall a b c x,
+  a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
+Proof.
+  intros.
+  Fail nia. (* Incompletness *)
+Abort.
+
+
+Lemma plus_minus : forall x y,
+  0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
+Lemma mplus_minus : forall x y,
+  x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma pol3: forall x y, 0 <= x + y ->
+  x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+
+(* Motivating example from: Expressiveness + Automation + Soundness:
+   Towards COmbining SMT Solvers and Interactive Proof Assistants *)
+Parameter rho : Z.
+Parameter rho_ge : rho >= 0.
+Parameter correct : Z -> Z -> Prop.
+
+
+Definition rbound1 (C:Z -> Z -> Z) : Prop :=
+  forall p s t, correct p t /\ s <= t -> C p t - C p s <= (1-rho)*(t-s).
+
+Definition rbound2 (C:Z -> Z -> Z) : Prop :=
+  forall p s t, correct p t /\ s <= t ->  (1-rho)*(t-s) <= C p t - C p s.
+
+
+Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
+  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  ->
+  Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s).
+Proof.
+  intros.
+  generalize (Z.abs_eq (C p t - D q t)).
+  generalize (Z.abs_neq (C p t - D q t)).
+  generalize (Z.abs_eq (C p s -D q s)).
+  generalize (Z.abs_neq (C p s - D q s)).
+  unfold rbound2 in H.
+  unfold rbound1 in H.
+  intuition.
+  generalize (H6 _ _ _ (conj H H4)).
+  generalize (H7 _ _ _ (conj H H4)).
+  generalize (H8 _ _ _ (conj H H4)).
+  generalize (H10 _ _ _ (conj H H4)).
+  generalize (H6 _ _ _ (conj H5 H4)).
+  generalize (H7 _ _ _ (conj H5 H4)).
+  generalize (H8 _ _ _ (conj H5 H4)).
+  generalize (H10 _ _ _ (conj H5 H4)).
+  generalize rho_ge.
+  nia.
+Qed.
+
+(* Rule of signs *)
+
+Lemma sign_pos_pos: forall x y,
+  x > 0 -> y > 0 -> x*y > 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_pos_zero: forall x y,
+  x > 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_pos_neg: forall x y,
+  x > 0 -> y < 0 -> x*y < 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_zero_pos: forall x y,
+  x = 0 -> y > 0 -> x*y = 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_zero_zero: forall x y,
+  x = 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_zero_neg: forall x y,
+  x = 0 -> y < 0 -> x*y = 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_neg_pos: forall x y,
+  x < 0 -> y > 0 -> x*y < 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_neg_zero: forall x y,
+  x < 0 -> y = 0 -> x*y = 0.
+Proof.
+  intros; nia.
+Qed.
+
+Lemma sign_neg_neg: forall x y,
+  x < 0 -> y < 0 -> x*y > 0.
+Proof.
+  intros; nia.
+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.
+  nia.
+Qed.
+
+
+Lemma product_strict : forall x y, x > 0 -> y > 0 -> x * y > 0.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Lemma pow_2_pos : forall x, x ^ 2 + 1 = 0 ->  False.
+Proof.
+  intros. nia.
+Qed.
+
+(* Found in Parrilo's talk *)
+(* BUG?: certificate with **very** big coefficients *)
+Lemma parrilo_ex : forall x y, x - y^2 + 3 >= 0 -> y + x^2 + 2 = 0 -> False.
+Proof.
+  intros.
+  nia.
+Qed.
+
+(* from hol_light/Examples/sos.ml *)
+
+Lemma hol_light1 : forall a1 a2 b1 b2,
+  a1 >= 0 -> a2 >= 0 ->
+   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) ->
+   (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+Lemma hol_light2 : forall x a,
+        3 * x + 7 * a < 4 -> 3 < 2 * x -> a < 0.
+Proof.
+ intros; nia.
+Qed.
+
+Lemma hol_light3 : forall b a c x,
+  b ^ 2 < 4 * a * c -> (a * x ^2  + b * x + c = 0) -> False.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+
+Lemma hol_light4 : forall a c b x,
+  a * x ^ 2 + b * x + c = 0 -> b ^ 2 >= 4 * a * c.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+Lemma hol_light5 : forall x y,
+    0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1
+     -> x ^ 2 + y ^ 2 < 1 \/
+      (x - 1) ^ 2 + y ^ 2 < 1 \/
+      x ^ 2 + (y - 1) ^ 2 < 1 \/
+      (x - 1) ^ 2 + (y - 1) ^ 2 < 1.
+Proof.
+intros; nia.
+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.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+Lemma hol_light8 : forall x y z,
+ x ^ 2 + y ^ 2 + z ^ 2 = 1 -> (x + y + z) ^ 2 <= 3.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+Lemma hol_light9 : forall w x y z,
+ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
+  -> (w + x + y + z) ^ 2 <= 4.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+
+Lemma hol_light10 : forall x y,
+ x >= 1 /\ y >= 1 -> x * y >= x + y - 1.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Lemma hol_light11 : forall x y,
+ x > 1 /\ y > 1 -> x * y > x + y - 1.
+Proof.
+  intros ; nia.
+Qed.
+
+Lemma hol_light12: forall x y z,
+  2 <= x /\ x <= 125841 / 50000 /\
+  2 <= y /\ y <= 125841 / 50000 /\
+  2 <= z /\ z <= 125841 / 50000
+   -> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= 0.
+Proof.
+  intros x y z ; set (e:= (125841 / 50000)).
+  compute in e.
+  unfold e ; intros ; nia.
+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).
+Proof.
+  intros ; nia.
+Qed.
+
+
+(* ------------------------------------------------------------------------- *)
+(* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
+(* ------------------------------------------------------------------------- *)
+
+Lemma hol_light16 : forall x y,
+  0 <= x /\ 0 <= y /\ (x * y = 1)
+   -> x + y <= x ^ 2 + y ^ 2.
+Proof.
+  intros ; nia.
+Qed.
+
+Lemma hol_light17 : forall x y,
+  0 <= x /\ 0 <= y /\ (x * y = 1)
+   -> x * y * (x + y) <= x ^ 2 + y ^ 2.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+
+Lemma hol_light18 : forall x y,
+  0 <= x /\ 0 <= y -> x * y * (x + y) ^ 2 <= (x ^ 2 + y ^ 2) ^ 2.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+(* ------------------------------------------------------------------------- *)
+(* 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.
+  nia.
+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).
+Proof.
+  intros.
+  nia.
+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.
+  Fail nia.
+Abort.
+
+
+Lemma motzkin : forall x y, (x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2)  >= 0.
+Proof.
+  intros.
+  Fail generalize (motzkin' x y).
+  Fail nia.
+Abort.
+
+(** 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.
+  lia.
+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 nia.
+  nia.
+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 nia.
+  nia.
+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.
+  lia.
+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.
+  lia.
+Qed.
+
+(** Needs some cutting plane *)
+Goal
+  forall (m : Z)
+         (M : Z)
+         (x : Z)
+         (i : Z)
+         (e1 : Z)
+         (e2 : Z)
+         (e5 : Z)
+         (e6 : Z)
+         (H2 : e5 >=  M)
+         (H11 :  i <  m)
+         (H5 : 0 <=  i)
+         (H15 :  m < 4294967296)
+         (H7 : 0 <=  x)
+         (H26 : e5 < 4294967296)
+         (H21 :  x +  i = 4294967296 * e6 + e5)
+         (H9 :  x +  m = 4294967296 * e2 + e1)
+         (H12 :  x < e1)
+         (H13 : e1 <  M),
+    False.
+Proof.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v
new file mode 100644
index 0000000000..ec39209230
--- /dev/null
+++ b/test-suite/micromega/non_lin_ci.v
@@ -0,0 +1,278 @@
+Require Import ZArith.
+Require Import Lia Psatz.
+Open Scope Z_scope.
+
+
+
+
+(* From fiat-crypto Generalized.v *)
+
+
+Goal forall (x1 : Z) (x2 : Z) (x3 : Z) (x4 : Z) (x5 : Z) (x6 : Z) (x7 : Z) (x8 : Z) (x9 : Z) (x10 : Z) (x11 : Z) (x12 : Z) (x13 : Z) (x14 : Z) (x15 : Z) (x16 : Z) (x17 : Z) (x18 : Z)
+(H0 : -1 + -x1^2 + x3*x5 + x1^2*x2 + -x2*x3*x4 >= 0)
+(H1 : -1 + x4 >= 0)
+(H2 : -1 + x6 >= 0)
+(H3 : -1 + -x4 + x1 >= 0)
+(H4 : x3 + -x7 = 0)
+(H5 : x8 >= 0)
+(H6 : -1 + x4 >= 0)
+(H7 : x9 >= 0)
+(H8 : -x8 + x10 >= 0)
+(H9 : -1 + x1^2 + -x9 >= 0)
+(H10 : x4 + -x11 >= 0)
+(H11 : -x3 + x1*x12 + -x12*x13 >= 0)
+(H12 : -1 + -x9 + x1*x4 >= 0)
+(H13 : -1 + x4 + -x13 >= 0)
+(H14 : x13 >= 0)
+(H15 : -1 + x5 >= 0)
+(H16 : -1 + x1 + -x2 >= 0)
+(H17 : x1^2 + -x13 + -x3*x4 = 0)
+(H18 : -1 + x12 + -x14 >= 0)
+(H19 : x14 >= 0)
+(H20 : x1 + -x14 + -x5*x12 = 0)
+(H21 : -1 + x4 + -x15 >= 0)
+(H22 : x15 >= 0)
+(H23 : x9 + -x15 + -x2*x4 = 0)
+(H24 : -x9 + x16 + x4*x17 = 0)
+(H25 : x17 + -x18 = 0)
+, False
+.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+Goal
+  forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13
+  __x14 __x15 __x16 : Z)
+         (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2)
+         (H7 : 0 <= __x8)
+         (H12 : 0 <= __x14)
+         (H0 : __x8 = __x15 * __x11 + __x9)
+         (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16)
+         (H17 : __x16 <= 0)
+         (H15 : 0 <= __x9)
+         (H18 : __x9 < __x15)
+         (H16 : 0 <= __x12)
+         (H19 : __x12 < (__x10 * __x15 + __x14) * __x10)
+  , False.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+
+(* From fiat-crypto Toplevel1.v *)
+
+
+Goal forall
+    (x1 x2 x3 x4 x5 x7 : Z)
+    (H0 : x1 + x2 - x3 = 0) (* substitute x1, nothing happens *)
+    (H1 : 2 * x2 - x4 - 1 >= 0)
+    (H2 : - x2 + x4 >= 0)
+    (H3 : 2 * x2 - x5 - 1 >= 0)
+    (H5 : x2 - 4 >= 0)
+    (H7 : - x2 * x7 + x4 * x5 >= 0)
+    (H6 : x2 * x7 + x2 - x4 * x5 - 1 >= 0)
+    (H9 : x7 - x2 ^ 2 >= 0), (* x2^2 is *visibly* positive *)
+  False.
+Proof.
+  intros.
+  nia.
+Qed.
+
+Goal forall
+    (x1 x2 x3 x4 x5 x7 : Z)
+    (H0 : x2 + x1 - x3 = 0) (* substitute x2= x3 -x1 ... *)
+    (H1 : 2 * x2 - x4 - 1 >= 0)
+    (H2 : - x2 + x4 >= 0)
+    (H3 : 2 * x2 - x5 - 1 >= 0)
+    (H5 : x2 - 4 >= 0)
+    (H7 : - x2 * x7 + x4 * x5 >= 0)
+    (H6 : x2 * x7 + x2 - x4 * x5 - 1 >= 0)
+    (H9 : x7 - x2 ^ 2 >= 0), (* (x3 - x1)^2 is not visibly positive *)
+  False.
+Proof.
+  intros.
+  nia.
+Qed.
+
+(* From bedrock2 FlatToRisc.v *)
+
+(* Variant of the following - omega fails (bad linearisation?)*)
+Goal forall
+    (PXLEN XLEN r : Z)
+    (q q0 r0 a : Z)
+    (H3 : 4 * a = 4 * PXLEN * q0 + (4 * q + r))
+    (H6 : 0 <= 4 * q + r)
+    (H7 : 4 * q + r < 4 * PXLEN)
+    (H8 : r <= 3)
+    (H4 : r >= 1),
+  False.
+Proof.
+  intros.
+  Time lia.
+Qed.
+
+Goal forall
+    (PXLEN XLEN r : Z)
+    (q q0 r0 a : Z)
+    (H3 : 4 * a = 4 * PXLEN * q0 + (4 * q + r))
+    (H6 : 0 <= 4 * q + r)
+    (H7 : 4 * q + r < 4 * PXLEN)
+    (H8 : r <= 3)
+    (H4 : r >= 1),
+  False.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+
+(** Very slow *)
+Goal forall
+    (XLEN r : Z)
+    (H : 4 < 2 ^ XLEN)
+    (H0 : 8 <= XLEN)
+    (q q0 r0 a : Z)
+    (H3 : 4 * a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+    (H5 : r0 = 4 * q + r)
+    (H6 : 0 <= r0)
+    (H7 : r0 < 4 * 2 ^ (XLEN - 2))
+    (H2 : 0 <= r)
+    (H8 : r < 4)
+    (H4 : r > 0)
+    (H9 : 0 < 2 ^ (XLEN - 2)),
+    False.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+Goal forall
+    (XLEN r : Z)
+    (R : r > 0 \/ r < 0)
+    (H : 4 < 2 ^ XLEN)
+    (H0 : 8 <= XLEN)
+    (H1 : ~ (0 <= XLEN - 2) \/ 0 < 2 ^ (XLEN - 2))
+     (q  q0 r0 a : Z)
+    (H2 : 0 <= r0 < 4 * 2 ^ (XLEN - 2))
+    (H3 : 4 *  a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+    (H4 : 0 <= r < 4)
+    (H5 : r0 = 4 * q + r),
+    False.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+Goal forall
+    (XLEN r : Z)
+    (R : r > 0 \/ r < 0)
+    (H : 4 < 2 ^ XLEN)
+    (H0 : 8 <= XLEN)
+    (H1 : ~ (0 <= XLEN - 2) \/ 0 < 2 ^ (XLEN - 2))
+     (q  q0 r0 a : Z)
+    (H2 : 0 <= r0 < 4 * 2 ^ (XLEN - 2))
+    (H3 : 4 *  a = 4 * 2 ^ (XLEN - 2) * q0 + r0)
+    (H4 : 0 <= r < 4)
+    (H5 : r0 = 4 * q + r),
+    False.
+Proof.
+  intros.
+  intuition idtac.
+  Time   all:nia.
+Qed.
+
+
+
+Goal forall
+    (XLEN a q q0 z : Z)
+    (HR : 4 * a - 4 * z * q0 - 4 * q > 0)
+    (H0 : 8 <= XLEN)
+    (H1 : 0 < z)
+    (H : 0 <= 4 * a - 4 * z * q0 - 4 * q)
+    (H3 : 4 * a - 4 * z * q0 - 4 * q < 4)
+    (H4 : 4 * a - 4 * z * q0 < 4 * z),
+  False.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+
+
+(* From fiat-crypto Modulo.v *)
+
+Goal forall  (b : Z)
+             (H : 0 <> b)
+             (c  r q1 q2 r2 : Z)
+             (H2 : r2 < c)
+             (q0 : Z)
+             (H7 : r < b)
+             (H5 : 0 <= r)
+             (H6 : r < b)
+             (H12 : 0 < c)
+             (H13 : 0 <> c)
+             (H0 : 0 <> c * b)
+             (H1 : 0 <= r2)
+             (H14 : 0 <= q0)
+             (H9 : c * q1 + q0 = c * q2 + r2)
+             (H4 : 0 <= b * q0 + - r)
+             (H10 : b * q0 + - r < c * b),
+  q1 = q2.
+Proof.
+  intros.
+  Fail nia.
+Abort.
+
+
+(* From Sozeau's plugin Equations *)
+
+
+Goal forall x p2 p1 m,
+    x <> 0%Z  ->
+    (Z.abs (x *  p2 ) > Z.abs (Z.abs p1 + Z.abs m))%Z ->
+    (Z.abs (x * (p1 + x * p2 )) > Z.abs m)%Z.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+
+Goal forall z z0 z1 m
+            (Heqz0 : z0 = ((1 + z) * z1)%Z)
+            (H0 : (0 <= m)%Z)
+            (H3 : z = m)
+            (H1 : (0 <= z0)%Z)
+            (H4 : z1 = z0)
+            (H2 : (z1 > 0)%Z),
+  (z1 > z)%Z.
+Proof.
+  intros.
+  Time nia.
+Qed.
+
+
+
+
+(* Known issues.
+
+  - Found proof may violate  Proof using ...
+    There may be a compliant proof but lia has no way to know.
+    Proofs could be optimised to minimise the number of hypotheses,
+    but this seems to costly.
+Section S.
+  Variable z z0 z1 z2 : Z.
+  Variable H2 : 0 <= z2.
+  Variable H3 : z2 < z1.
+  Variable H4 : 0 <= z0.
+  Variable H5 : z0 < z1.
+  Variable H6 : z = - z2.
+
+  Goal -z1 -z2  >= 0 -> False.
+  Proof using  H2 H3  H6.
+    intros.
+    lia.
+  Qed.
+*)
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.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index d163dfbcd2..7266b662fa 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -11,21 +11,21 @@ Open Scope Z_scope.
 
 Lemma Zabs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
- intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
+ intros ; case (Zabs_dec x) ; intros ; nia.
 Qed.
 Hint Resolve Z.abs_nonneg Zabs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
-intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
+  intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
 assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
          /\ Z.abs p^2 = p^2) by auto.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
-  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
+  (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
 intros n IHn p [Hn [Hp Heq]].
-assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; psatz Z 2).
-assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by psatz Z 2.
+assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; nia).
+assert (Hdecr : 0 < 2*p-n /\ 0 <= n-p /\ (2*p-n)^2=2*(n-p)^2) by nia.
 apply (IHn (2*p-n) Hzwf (n-p) Hdecr).
 Qed.