diff options
Diffstat (limited to 'flocq/Core/Fcore_ulp.v')
| -rw-r--r-- | flocq/Core/Fcore_ulp.v | 21 |
1 files changed, 4 insertions, 17 deletions
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... |