From 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 8 Mar 2019 09:56:49 +0100
Subject: 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
---
 theories/Reals/Rbasic_fun.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'theories/Reals/Rbasic_fun.v')

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 59e0148625..e17f02bb6e 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -15,7 +15,6 @@
 
 Require Import Rbase.
 Require Import R_Ifp.
-Require Import Lra.
 Local Open Scope R_scope.
 
 Implicit Type r : R.
@@ -357,7 +356,9 @@ Qed.
 
 Lemma Rle_abs : forall x:R, x <= Rabs x.
 Proof.
-  intro; unfold Rabs; case (Rcase_abs x); intros; lra.
+  intro; unfold Rabs; case (Rcase_abs x); intros;auto with real.
+  apply Rminus_le; rewrite <- Rplus_0_r;
+    unfold Rminus; rewrite Ropp_involutive; auto with real.
 Qed.
 
 Definition RRle_abs := Rle_abs.
-- 
cgit v1.2.3