From 177c8fbc523a171e8c8470fa675f9a69ef7f99de Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 8 Mar 2017 08:35:29 +0100
Subject: Adapt proofs to future handling of literal constants in Coq.

This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
---
 flocq/Core/Fcore_ulp.v | 21 ++++-----------------
 1 file changed, 4 insertions(+), 17 deletions(-)

(limited to 'flocq/Core/Fcore_ulp.v')

diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 28d2bc35..3bc0eac3 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -18,6 +18,7 @@ COPYING file for more details.
 *)
 
 (** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
+Require Import Reals Psatz.
 Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
@@ -2002,7 +2003,7 @@ rewrite Hx in Hfx; contradict Hfx; auto with real.
 intros H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le.
 rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption.
 apply Ropp_le_contravar.
@@ -2018,7 +2019,7 @@ case (Rle_or_lt 0 (round beta fexp Zceil x)).
 intros H; destruct H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le_pos; trivial.
 case (Rle_or_lt 0 x); trivial.
 intros H1; contradict H.
@@ -2234,21 +2235,7 @@ apply generic_format_0.
 left; apply Rlt_le_trans with (1:=H).
 rewrite V1,V2; right; field.
 (* *)
-assert (T: (u < (u + succ u) / 2 < succ u)%R).
-split.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-u)%R.
-apply Rle_lt_trans with u;[right; ring|idtac].
-apply Rlt_le_trans with (1:=V).
-right; field.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-succ u)%R.
-apply Rle_lt_trans with u;[right; field|idtac].
-apply Rlt_le_trans with (1:=V).
-right; ring.
-(* *)
+assert (T: (u < (u + succ u) / 2 < succ u)%R) by lra.
 destruct T as (T1,T2).
 apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R...
 apply round_N_pt...
-- 
cgit