Several improvements and fixes of Lia

- Improved reification for Micromega (support for #8764)

- Fixes #9268: Do not take universes into account in lia reification

  Improve #9291 by threading the evar_map during reification.
  Universes are unified.

- Remove (potentially cyclic) dependency over lra for Rle_abs

- Towards a complete simplex-based lia

  fixes  #9615

Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal  for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.

For scalability, nia is currently NOT performing this pre-processing.

- Lia is using the FSet library

  manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
  to work around a "leaked" hint breaking compatibility of eauto

5 files changed, 123 insertions, 3 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b85258505b..e0324b0232 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
index 8de631aa6a..485c24f0c9 100644
--- a/test-suite/micromega/example_nia.v
+++ b/test-suite/micromega/example_nia.v
@@ -435,6 +435,12 @@ Goal forall
     (R  : sz + d * sz - sz * x >= 1),
     False.
 Proof.
+  (* Manual proof.
+     assert (H : sz >= 2) by GE + R.
+     assert (GEd : x - d >= 1 by GE / H
+     assert (Rd  : 1 + d - x >= 1 by R / H)
+     1 >= 2 by GEd + Rd
+   *)
   intros.
   assert (x - d >= 1) by nia.
   nia.
diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v
new file mode 100644
index 0000000000..02b98b562f
--- /dev/null
+++ b/test-suite/micromega/rsyntax.v
@@ -0,0 +1,75 @@
+Require Import ZArith.
+Require Import Lra.
+Require Import Reals.
+
+Goal (1 / (1 - 1) = 0)%R.
+  Fail lra. (* division by zero *)
+Abort.
+
+Goal (0 / (1 - 1) = 0)%R.
+  lra. (* 0 * x = 0 *)
+Qed.
+
+Goal (10 ^ 2 = 100)%R.
+  lra. (* pow is reified as a constant *)
+Qed.
+
+Goal (2 / (1/2) ^ 2 = 8)%R.
+  lra. (* pow is reified as a constant *)
+Qed.
+
+
+Goal ( IZR (Z.sqrt 4) = 2)%R.
+Proof.
+  Fail lra.
+Abort.
+
+Require Import DeclConstant.
+
+Instance Dsqrt : DeclaredConstant Z.sqrt := {}.
+
+Goal ( IZR (Z.sqrt 4) = 2)%R.
+Proof.
+  lra.
+Qed.
+
+Require Import QArith.
+Require Import Qreals.
+
+Goal (Q2R (1 # 2) = 1/2)%R.
+Proof.
+  lra.
+Qed.
+
+Goal ( 1 ^ (2 + 2) = 1)%R.
+Proof.
+  Fail lra.
+Abort.
+
+Instance Dplus : DeclaredConstant Init.Nat.add := {}.
+
+Goal ( 1 ^ (2 + 2) = 1)%R.
+Proof.
+  lra.
+Qed.
+
+Require Import Lia.
+
+Goal ( 1 ^ (2 + 2) = 1)%Z.
+Proof.
+  Fail lia.
+  reflexivity.
+Qed.
+
+Instance DZplus : DeclaredConstant Z.add := {}.
+
+Goal ( 1 ^ (2 + 2) = 1)%Z.
+Proof.
+  lia.
+Qed.
+
+
+Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R.
+Proof.
+  lra.
+Qed.
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 239bc69360..55691f553c 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -82,11 +82,48 @@ Proof.
   lia.
 Qed.
 
+Section S.
+  Variables x y: Z.
+  Variables XGe : x >= 0.
+  Variables YGt : y > 0.
+  Variables YLt : y < 0.
+
+  Goal False.
+  Proof using - XGe.
+    lia.
+  Qed.
+
+  Goal False.
+  Proof using YGt YLt x y.
+    lia.
+  Qed.
+
+  End S.
+
 (*  Bug 5073 *)
 Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
 Proof.
   lia.
 Qed.
 
+Lemma ex_pos : forall x, exists z t, x = z - t /\ z >= 0 /\ t >= 0.
+Proof.
+  intros.
+  destruct (dec_Zge x 0).
+  exists x, 0.
+  lia.
+  exists 0, (-x).
+  lia.
+Qed.
 
-
+Goal forall
+    (b q r : Z)
+    (H : b * q + r <= 0)
+    (H5 : - b < r)
+    (H6 : r <= 0)
+    (H2 : 0 <= b),
+  b = 0 -> False.
+Proof.
+  intros b q r.
+  lia.
+Qed.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 36992e4dda..7429a521b3 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -7,6 +7,8 @@ Require Import QMicromega.
 Require Import RMicromega.
 
 Recursive Extraction
-   List.map simpl_cone (*map_cone  indexes*)
-   denorm Qpower vm_add
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ
+           List.map simpl_cone (*map_cone  indexes*)
+           denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.