From 4ee0544a157090ddd087b36109d292cd174bae7c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 2 Aug 2013 08:05:18 +0000 Subject: Merge of Flocq version 2.2.0. More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- flocq/Core/Fcore.v | 4 +- flocq/Core/Fcore_FIX.v | 4 +- flocq/Core/Fcore_FLT.v | 4 +- flocq/Core/Fcore_FLX.v | 4 +- flocq/Core/Fcore_FTZ.v | 4 +- flocq/Core/Fcore_Raux.v | 16 ++- flocq/Core/Fcore_Zaux.v | 4 +- flocq/Core/Fcore_defs.v | 4 +- flocq/Core/Fcore_digits.v | 4 +- flocq/Core/Fcore_float_prop.v | 4 +- flocq/Core/Fcore_generic_fmt.v | 103 ++++++++++++++- flocq/Core/Fcore_rnd.v | 4 +- flocq/Core/Fcore_rnd_ne.v | 23 +++- flocq/Core/Fcore_ulp.v | 278 ++++++++++++++++++++++++++++++++++++++++- 14 files changed, 432 insertions(+), 28 deletions(-) (limited to 'flocq/Core') diff --git a/flocq/Core/Fcore.v b/flocq/Core/Fcore.v index 23ebb39..2a5a5f0 100644 --- a/flocq/Core/Fcore.v +++ b/flocq/Core/Fcore.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v index f185ddf..a3b8d4d 100644 --- a/flocq/Core/Fcore_FIX.v +++ b/flocq/Core/Fcore_FIX.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v index 4ad4797..c057b6c 100644 --- a/flocq/Core/Fcore_FLT.v +++ b/flocq/Core/Fcore_FLT.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_FLX.v b/flocq/Core/Fcore_FLX.v index 62ecb6f..800540f 100644 --- a/flocq/Core/Fcore_FLX.v +++ b/flocq/Core/Fcore_FLX.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v index 5356c11..5f3e533 100644 --- a/flocq/Core/Fcore_FTZ.v +++ b/flocq/Core/Fcore_FTZ.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index 748e36e..d811019 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public @@ -121,6 +121,18 @@ rewrite <- 3!(Rmult_comm r). apply Rmult_minus_distr_l. Qed. +Lemma Rmult_neq_reg_r: forall r1 r2 r3:R, (r2 * r1 <> r3 * r1)%R -> r2 <> r3. +intros r1 r2 r3 H1 H2. +apply H1; rewrite H2; ring. +Qed. + +Lemma Rmult_neq_compat_r: forall r1 r2 r3:R, (r1 <> 0)%R -> (r2 <> r3)%R + -> (r2 *r1 <> r3*r1)%R. +intros r1 r2 r3 H H1 H2. +now apply H1, Rmult_eq_reg_r with r1. +Qed. + + Theorem Rmult_min_distr_r : forall r r1 r2 : R, (0 <= r)%R -> diff --git a/flocq/Core/Fcore_Zaux.v b/flocq/Core/Fcore_Zaux.v index af0d837..7ba28ca 100644 --- a/flocq/Core/Fcore_Zaux.v +++ b/flocq/Core/Fcore_Zaux.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2011 Sylvie Boldo +Copyright (C) 2011-2013 Sylvie Boldo #
# -Copyright (C) 2011 Guillaume Melquiond +Copyright (C) 2011-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_defs.v b/flocq/Core/Fcore_defs.v index fda3a85..ad8cf4f 100644 --- a/flocq/Core/Fcore_defs.v +++ b/flocq/Core/Fcore_defs.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index 2ae076e..02c7a0e 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2011 Sylvie Boldo +Copyright (C) 2011-2013 Sylvie Boldo #
# -Copyright (C) 2011 Guillaume Melquiond +Copyright (C) 2011-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v index 746f7a6..e1535bc 100644 --- a/flocq/Core/Fcore_float_prop.v +++ b/flocq/Core/Fcore_float_prop.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v index b1db47c..b04cf3d 100644 --- a/flocq/Core/Fcore_generic_fmt.v +++ b/flocq/Core/Fcore_generic_fmt.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public @@ -165,6 +165,22 @@ now rewrite Ztrunc_Z2R. now apply Zle_left. Qed. +Lemma generic_format_F2R': forall (x:R) (f:float beta), + F2R f = x -> ((x <> 0)%R -> + (canonic_exp x <= Fexp f)%Z) -> + generic_format x. +Proof. +intros x f H1 H2. +rewrite <- H1; destruct f as (m,e). +apply generic_format_F2R. +simpl in *; intros H3. +rewrite H1; apply H2. +intros Y; apply H3. +apply F2R_eq_0_reg with beta e. +now rewrite H1. +Qed. + + Theorem canonic_opp : forall m e, canonic (Float beta m e) -> @@ -175,6 +191,26 @@ unfold canonic. now rewrite F2R_Zopp, canonic_exp_opp. Qed. +Theorem canonic_abs : + forall m e, + canonic (Float beta m e) -> + canonic (Float beta (Zabs m) e). +Proof. +intros m e H. +unfold canonic. +now rewrite F2R_Zabs, canonic_exp_abs. +Qed. + +Theorem canonic_0: canonic (Float beta 0 (fexp (ln_beta beta 0%R))). +Proof. +unfold canonic; simpl; unfold canonic_exp. +replace (F2R {| Fnum := 0; Fexp := fexp (ln_beta beta 0) |}) with 0%R. +reflexivity. +unfold F2R; simpl; ring. +Qed. + + + Theorem canonic_unicity : forall f1 f2, canonic f1 -> @@ -756,6 +792,24 @@ refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). now apply mantissa_small_pos. Qed. + +Theorem exp_small_round_0_pos : + forall x ex, + (bpow (ex - 1) <= x < bpow ex)%R -> + round x =R0 -> (ex <= fexp ex)%Z . +Proof. +intros x ex H H1. +case (Zle_or_lt ex (fexp ex)); trivial; intros V. +contradict H1. +apply Rgt_not_eq. +apply Rlt_le_trans with (bpow (ex-1)). +apply bpow_gt_0. +apply (round_bounded_large_pos); assumption. +Qed. + + + + Theorem generic_format_round_pos : forall x, (0 < x)%R -> @@ -1014,6 +1068,24 @@ intros rnd' Hr x. apply round_bounded_large_pos... Qed. +Theorem exp_small_round_0 : + forall rnd {Hr : Valid_rnd rnd} x ex, + (bpow (ex - 1) <= Rabs x < bpow ex)%R -> + round rnd x =R0 -> (ex <= fexp ex)%Z . +Proof. +intros rnd Hr x ex H1 H2. +generalize Rabs_R0. +rewrite <- H2 at 1. +apply (round_abs_abs' (fun t rt => forall (ex : Z), +(bpow (ex - 1) <= t < bpow ex)%R -> +rt = 0%R -> (ex <= fexp ex)%Z)); trivial. +clear; intros rnd Hr x Hx. +now apply exp_small_round_0_pos. +Qed. + + + + Section monotone_abs. Variable rnd : R -> Z. @@ -1283,6 +1355,33 @@ rewrite <- mantissa_DN_small_pos with (1 := Hx) (2 := He). now rewrite <- canonic_exp_fexp_pos with (1 := Hx). Qed. + +Theorem round_DN_UP_lt : + forall x, ~ generic_format x -> + (round Zfloor x < x < round Zceil x)%R. +Proof with auto with typeclass_instances. +intros x Fx. +assert (Hx:(round Zfloor x <= x <= round Zceil x)%R). +split. +apply round_DN_pt. +apply round_UP_pt. +split. + destruct Hx as [Hx _]. + apply Rnot_le_lt; intro Hle. + assert (x = round Zfloor x) by now apply Rle_antisym. + rewrite H in Fx. + contradict Fx. + apply generic_format_round... +destruct Hx as [_ Hx]. +apply Rnot_le_lt; intro Hle. +assert (x = round Zceil x) by now apply Rle_antisym. +rewrite H in Fx. +contradict Fx. +apply generic_format_round... +Qed. + + + Theorem round_UP_small_pos : forall x ex, (bpow (ex - 1) <= x < bpow ex)%R -> diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v index 6b4d807..94c9420 100644 --- a/flocq/Core/Fcore_rnd.v +++ b/flocq/Core/Fcore_rnd.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 0b0776e..6829c0c 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public @@ -499,6 +499,25 @@ rewrite Zeven_plus. now rewrite eqb_sym. Qed. +Lemma round_NE_abs: + forall x : R, + round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x). +Proof with auto with typeclass_instances. +intros x. +apply sym_eq. +unfold Rabs at 2. +destruct (Rcase_abs x) as [Hx|Hx]. +rewrite round_NE_opp. +apply Rabs_left1. +rewrite <- (round_0 beta fexp ZnearestE). +apply round_le... +now apply Rlt_le. +apply Rabs_pos_eq. +rewrite <- (round_0 beta fexp ZnearestE). +apply round_le... +now apply Rge_le. +Qed. + Theorem round_NE_pt : forall x, Rnd_NE_pt x (round beta fexp ZnearestE x). diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v index 492fac6..07ef3ec 100644 --- a/flocq/Core/Fcore_ulp.v +++ b/flocq/Core/Fcore_ulp.v @@ -2,9 +2,9 @@ This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ -Copyright (C) 2010-2011 Sylvie Boldo +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public @@ -1139,4 +1139,278 @@ apply le_pred_lt_aux ; try easy. now split. Qed. + +Theorem pred_succ : forall { monotone_exp : Monotone_exp fexp }, + forall x, F x -> (0 < x)%R -> pred (x + ulp x)=x. +Proof. +intros L x Fx Hx. +assert (x <= pred (x + ulp x))%R. +apply le_pred_lt. +assumption. +now apply generic_format_succ. +replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. +apply bpow_gt_0. +apply Rplus_lt_reg_r with (-x)%R; ring_simplify. +apply bpow_gt_0. +apply Rle_antisym; trivial. +apply Rplus_le_reg_r with (ulp (pred (x + ulp x))). +rewrite pred_plus_ulp. +apply Rplus_le_compat_l. +now apply ulp_le. +replace 0%R with (0+0)%R by ring; apply Rplus_lt_compat; try apply Hx. +apply bpow_gt_0. +now apply generic_format_succ. +apply Rgt_not_eq. +now apply Rlt_le_trans with x. +Qed. + + +Theorem lt_UP_le_DN : + forall x y, F y -> + (y < round beta fexp Zceil x -> y <= round beta fexp Zfloor x)%R. +Proof with auto with typeclass_instances. +intros x y Fy Hlt. +apply round_DN_pt... +apply Rnot_lt_le. +contradict Hlt. +apply RIneq.Rle_not_lt. +apply round_UP_pt... +now apply Rlt_le. +Qed. + +Theorem pred_UP_le_DN : + forall x, (0 < round beta fexp Zceil x)%R -> + (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R. +Proof with auto with typeclass_instances. +intros x Pxu. +destruct (generic_format_EM beta fexp x) as [Fx|Fx]. +rewrite !round_generic... +now apply Rlt_le; apply pred_lt_id. +assert (let u := round beta fexp Zceil x in pred u < u)%R as Hup. + now apply pred_lt_id. +apply lt_UP_le_DN... +apply generic_format_pred... +now apply round_UP_pt. +Qed. + +Theorem pred_UP_eq_DN : + forall x, (0 < round beta fexp Zceil x)%R -> ~ F x -> + (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R. +Proof with auto with typeclass_instances. +intros x Px Fx. +apply Rle_antisym. +now apply pred_UP_le_DN. +apply le_pred_lt; try apply generic_format_round... +pose proof round_DN_UP_lt _ _ _ Fx as HE. +now apply Rlt_trans with (1 := proj1 HE) (2 := proj2 HE). +Qed. + + + + + +(** Properties of rounding to nearest and ulp *) + +Theorem rnd_N_le_half_an_ulp: forall choice u v, + F u -> (0 < u)%R -> (v < u + (ulp u)/2)%R + -> (round beta fexp (Znearest choice) v <= u)%R. +Proof with auto with typeclass_instances. +intros choice u v Fu Hu H. +(* . *) +assert (0 < ulp u / 2)%R. +unfold Rdiv; apply Rmult_lt_0_compat. +unfold ulp; apply bpow_gt_0. +auto with real. +(* . *) +assert (ulp u / 2 < ulp u)%R. +apply Rlt_le_trans with (ulp u *1)%R;[idtac|right; ring]. +unfold Rdiv; apply Rmult_lt_compat_l. +apply bpow_gt_0. +apply Rmult_lt_reg_l with 2%R. +auto with real. +apply Rle_lt_trans with 1%R. +right; field. +rewrite Rmult_1_r; auto with real. +(* *) +apply Rnd_N_pt_monotone with F v (u + ulp u / 2)%R... +apply round_N_pt... +apply Rnd_DN_pt_N with (u+ulp u)%R. +pattern u at 3; replace u with (round beta fexp Zfloor (u + ulp u / 2)). +apply round_DN_pt... +apply round_DN_succ; try assumption. +split; try left; assumption. +replace (u+ulp u)%R with (round beta fexp Zceil (u + ulp u / 2)). +apply round_UP_pt... +apply round_UP_succ; try assumption... +split; try left; assumption. +right; field. +Qed. + + +Theorem rnd_N_ge_half_an_ulp_pred: forall choice u v, + F u -> (0 < pred u)%R -> (u - (ulp (pred u))/2 < v)%R + -> (u <= round beta fexp (Znearest choice) v)%R. +Proof with auto with typeclass_instances. +intros choice u v Fu Hu H. +(* . *) +assert (0 < u)%R. +apply Rlt_trans with (1:= Hu). +apply pred_lt_id. +assert (0 < ulp (pred u) / 2)%R. +unfold Rdiv; apply Rmult_lt_0_compat. +unfold ulp; apply bpow_gt_0. +auto with real. +assert (ulp (pred u) / 2 < ulp (pred u))%R. +apply Rlt_le_trans with (ulp (pred u) *1)%R;[idtac|right; ring]. +unfold Rdiv; apply Rmult_lt_compat_l. +apply bpow_gt_0. +apply Rmult_lt_reg_l with 2%R. +auto with real. +apply Rle_lt_trans with 1%R. +right; field. +rewrite Rmult_1_r; auto with real. +(* *) +apply Rnd_N_pt_monotone with F (u - ulp (pred u) / 2)%R v... +2: apply round_N_pt... +apply Rnd_UP_pt_N with (pred u). +pattern (pred u) at 2; replace (pred u) with (round beta fexp Zfloor (u - ulp (pred u) / 2)). +apply round_DN_pt... +replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. +apply round_DN_succ; try assumption. +apply generic_format_pred; assumption. +split; [left|idtac]; assumption. +pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. +field. +now apply Rgt_not_eq. +pattern u at 3; replace u with (round beta fexp Zceil (u - ulp (pred u) / 2)). +apply round_UP_pt... +replace (u - ulp (pred u) / 2)%R with (pred u + ulp (pred u) / 2)%R. +apply trans_eq with (pred u +ulp(pred u))%R. +apply round_UP_succ; try assumption... +apply generic_format_pred; assumption. +split; [idtac|left]; assumption. +apply pred_plus_ulp; try assumption. +now apply Rgt_not_eq. +pattern u at 3; rewrite <- (pred_plus_ulp u); try assumption. +field. +now apply Rgt_not_eq. +pattern u at 4; rewrite <- (pred_plus_ulp u); try assumption. +right; field. +now apply Rgt_not_eq. +Qed. + + +Theorem rnd_N_ge_half_an_ulp: forall choice u v, + F u -> (0 < u)%R -> (u <> bpow (ln_beta beta u - 1))%R + -> (u - (ulp u)/2 < v)%R + -> (u <= round beta fexp (Znearest choice) v)%R. +Proof with auto with typeclass_instances. +intros choice u v Fu Hupos Hu H. +(* *) +assert (bpow (ln_beta beta u-1) <= pred u)%R. +apply le_pred_lt; try assumption. +apply generic_format_bpow. +assert (canonic_exp beta fexp u < ln_beta beta u)%Z. +apply ln_beta_generic_gt; try assumption. +now apply Rgt_not_eq. +unfold canonic_exp in H0. +ring_simplify (ln_beta beta u - 1 + 1)%Z. +omega. +destruct ln_beta as (e,He); simpl in *. +assert (bpow (e - 1) <= Rabs u)%R. +apply He. +now apply Rgt_not_eq. +rewrite Rabs_right in H0. +case H0; auto. +intros T; contradict T. +now apply sym_not_eq. +apply Rle_ge; now left. +assert (Hu2:(ulp (pred u) = ulp u)). +unfold ulp, canonic_exp. +apply f_equal; apply f_equal. +apply ln_beta_unique. +rewrite Rabs_right. +split. +assumption. +apply Rlt_trans with (1:=pred_lt_id _). +destruct ln_beta as (e,He); simpl in *. +rewrite Rabs_right in He. +apply He. +now apply Rgt_not_eq. +apply Rle_ge; now left. +apply Rle_ge, pred_ge_0; assumption. +apply rnd_N_ge_half_an_ulp_pred; try assumption. +apply Rlt_le_trans with (2:=H0). +apply bpow_gt_0. +rewrite Hu2; assumption. +Qed. + + +Lemma round_N_DN_betw: forall choice x d u, + Rnd_DN_pt (generic_format beta fexp) x d -> + Rnd_UP_pt (generic_format beta fexp) x u -> + (d<=x<(d+u)/2)%R -> + round beta fexp (Znearest choice) x = d. +Proof with auto with typeclass_instances. +intros choice x d u Hd Hu H. +apply Rnd_N_pt_unicity with (generic_format beta fexp) x d u; try assumption. +intros Y. +absurd (x < (d+u)/2)%R; try apply H. +apply Rle_not_lt; right. +apply Rplus_eq_reg_r with (-x)%R. +apply trans_eq with (- (x-d)/2 + (u-x)/2)%R. +field. +rewrite Y; field. +apply round_N_pt... +apply Rnd_DN_UP_pt_N with d u... +apply Hd. +right; apply trans_eq with (-(d-x))%R;[idtac|ring]. +apply Rabs_left1. +apply Rplus_le_reg_l with x; ring_simplify. +apply H. +rewrite Rabs_left1. +apply Rplus_le_reg_l with (d+x)%R. +apply Rmult_le_reg_l with (/2)%R. +auto with real. +apply Rle_trans with x. +right; field. +apply Rle_trans with ((d+u)/2)%R. +now left. +right; field. +apply Rplus_le_reg_l with x; ring_simplify. +apply H. +Qed. + + +Lemma round_N_UP_betw: forall choice x d u, + Rnd_DN_pt (generic_format beta fexp) x d -> + Rnd_UP_pt (generic_format beta fexp) x u -> + ((d+u)/2 < x <= u)%R -> + round beta fexp (Znearest choice) x = u. +Proof with auto with typeclass_instances. +intros choice x d u Hd Hu H. +rewrite <- (Ropp_involutive (round beta fexp (Znearest choice) x )), + <- (Ropp_involutive u) . +apply f_equal. +rewrite <- (Ropp_involutive x) . +rewrite round_N_opp, Ropp_involutive. +apply round_N_DN_betw with (-d)%R. +replace u with (round beta fexp Zceil x). +rewrite <- round_DN_opp. +apply round_DN_pt... +apply Rnd_UP_pt_unicity with (generic_format beta fexp) x... +apply round_UP_pt... +replace d with (round beta fexp Zfloor x). +rewrite <- round_UP_opp. +apply round_UP_pt... +apply Rnd_DN_pt_unicity with (generic_format beta fexp) x... +apply round_DN_pt... +split. +apply Ropp_le_contravar, H. +apply Rlt_le_trans with (-((d + u) / 2))%R. +apply Ropp_lt_contravar, H. +unfold Rdiv; right; ring. +Qed. + + End Fcore_ulp. -- cgit v1.2.3