diff options
| author | Frédéric Besson | 2019-03-08 09:56:49 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-04-01 12:08:45 +0200 |
| commit | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (patch) | |
| tree | 2f09d223261f45a527b36231a4f74c803ccf8fa6 /theories/Reals/Rbasic_fun.v | |
| parent | 4c3f4d105a32cc7661ae714fe4e25619e32bc84c (diff) | |
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
Diffstat (limited to 'theories/Reals/Rbasic_fun.v')
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 5 |
1 files changed, 3 insertions, 2 deletions
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. |