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

14 files changed, 432 insertions, 28 deletions

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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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
 #<br />#
-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.