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

1 files changed, 15 insertions, 0 deletions

diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index 952a1b91e7..898a3a1a28 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -36,6 +36,21 @@ trivial.
 intro; apply IH.
 Qed.
 
+
+Theorem make_impl_map :
+  forall (A B: Type) (eval : A -> Prop) (eval' : A*B -> Prop) (l : list (A*B)) r
+         (EVAL : forall x, eval' x <-> eval (fst x)),
+    make_impl eval' l r <-> make_impl eval (List.map fst l) r.
+Proof.
+induction l as [| a l IH]; simpl.
+- tauto.
+- intros.
+  rewrite EVAL.
+  rewrite IH.
+  tauto.
+  auto.
+Qed.
+
 Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop :=
   match l with
     | nil => True