summaryrefslogtreecommitdiff
path: root/flocq/Appli/Fappli_rnd_odd.v
diff options
context:
space:
mode:
Diffstat (limited to 'flocq/Appli/Fappli_rnd_odd.v')
-rw-r--r--flocq/Appli/Fappli_rnd_odd.v979
1 files changed, 979 insertions, 0 deletions
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v
new file mode 100644
index 0000000..b4a2c52
--- /dev/null
+++ b/flocq/Appli/Fappli_rnd_odd.v
@@ -0,0 +1,979 @@
+(**
+This file is part of the Flocq formalization of floating-point
+arithmetic in Coq: http://flocq.gforge.inria.fr/
+
+Copyright (C) 2010-2013 Sylvie Boldo
+#<br />#
+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
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Rounding to odd and its properties, including the equivalence
+ between rnd_NE and double rounding with rnd_odd and then rnd_NE *)
+
+
+Require Import Fcore.
+Require Import Fcalc_ops.
+
+Definition Zrnd_odd x := match Req_EM_T x (Z2R (Zfloor x)) with
+ | left _ => Zfloor x
+ | right _ => match (Zeven (Zfloor x)) with
+ | true => Zceil x
+ | false => Zfloor x
+ end
+ end.
+
+
+
+Global Instance valid_rnd_odd : Valid_rnd Zrnd_odd.
+Proof.
+split.
+(* . *)
+intros x y Hxy.
+assert (Zfloor x <= Zrnd_odd y)%Z.
+(* .. *)
+apply Zle_trans with (Zfloor y).
+now apply Zfloor_le.
+unfold Zrnd_odd; destruct (Req_EM_T y (Z2R (Zfloor y))).
+now apply Zle_refl.
+case (Zeven (Zfloor y)).
+apply le_Z2R.
+apply Rle_trans with y.
+apply Zfloor_lb.
+apply Zceil_ub.
+now apply Zle_refl.
+unfold Zrnd_odd at 1.
+(* . *)
+destruct (Req_EM_T x (Z2R (Zfloor x))) as [Hx|Hx].
+(* .. *)
+apply H.
+(* .. *)
+case_eq (Zeven (Zfloor x)); intros Hx2.
+2: apply H.
+unfold Zrnd_odd; destruct (Req_EM_T y (Z2R (Zfloor y))) as [Hy|Hy].
+apply Zceil_glb.
+now rewrite <- Hy.
+case_eq (Zeven (Zfloor y)); intros Hy2.
+now apply Zceil_le.
+apply Zceil_glb.
+assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le.
+case (Zle_lt_or_eq _ _ H0); intros H1.
+apply Rle_trans with (1:=Zceil_ub _).
+rewrite Zceil_floor_neq.
+apply Z2R_le; omega.
+now apply sym_not_eq.
+contradict Hy2.
+rewrite <- H1, Hx2; discriminate.
+(* . *)
+intros n; unfold Zrnd_odd.
+rewrite Zfloor_Z2R, Zceil_Z2R.
+destruct (Req_EM_T (Z2R n) (Z2R n)); trivial.
+case (Zeven n); trivial.
+Qed.
+
+
+
+Lemma Zrnd_odd_Zodd: forall x, x <> (Z2R (Zfloor x)) ->
+ (Zeven (Zrnd_odd x)) = false.
+Proof.
+intros x Hx; unfold Zrnd_odd.
+destruct (Req_EM_T x (Z2R (Zfloor x))) as [H|H].
+now contradict H.
+case_eq (Zeven (Zfloor x)).
+(* difficult case *)
+intros H'.
+rewrite Zceil_floor_neq.
+rewrite Zeven_plus, H'.
+reflexivity.
+now apply sym_not_eq.
+trivial.
+Qed.
+
+
+
+
+Section Fcore_rnd_odd.
+
+Variable beta : radix.
+
+Notation bpow e := (bpow beta e).
+
+Variable fexp : Z -> Z.
+
+Context { valid_exp : Valid_exp fexp }.
+Context { exists_NE_ : Exists_NE beta fexp }.
+
+Notation format := (generic_format beta fexp).
+Notation canonic := (canonic beta fexp).
+Notation cexp := (canonic_exp beta fexp).
+
+
+Definition Rnd_odd_pt (x f : R) :=
+ format f /\ ((f = x)%R \/
+ ((Rnd_DN_pt format x f \/ Rnd_UP_pt format x f) /\
+ exists g : float beta, f = F2R g /\ canonic g /\ Zeven (Fnum g) = false)).
+
+Definition Rnd_odd (rnd : R -> R) :=
+ forall x : R, Rnd_odd_pt x (rnd x).
+
+
+Theorem Rnd_odd_pt_sym : forall x f : R,
+ Rnd_odd_pt (-x) (-f) -> Rnd_odd_pt x f.
+Proof with auto with typeclass_instances.
+intros x f (H1,H2).
+split.
+replace f with (-(-f))%R by ring.
+now apply generic_format_opp.
+destruct H2.
+left.
+replace f with (-(-f))%R by ring.
+rewrite H; ring.
+right.
+destruct H as (H2,(g,(Hg1,(Hg2,Hg3)))).
+split.
+destruct H2.
+right.
+replace f with (-(-f))%R by ring.
+replace x with (-(-x))%R by ring.
+apply Rnd_DN_UP_pt_sym...
+apply generic_format_opp.
+left.
+replace f with (-(-f))%R by ring.
+replace x with (-(-x))%R by ring.
+apply Rnd_UP_DN_pt_sym...
+apply generic_format_opp.
+exists (Float beta (-Fnum g) (Fexp g)).
+split.
+rewrite F2R_Zopp.
+replace f with (-(-f))%R by ring.
+rewrite Hg1; reflexivity.
+split.
+now apply canonic_opp.
+simpl.
+now rewrite Zeven_opp.
+Qed.
+
+
+Theorem round_odd_opp :
+ forall x,
+ (round beta fexp Zrnd_odd (-x) = (- round beta fexp Zrnd_odd x))%R.
+Proof.
+intros x; unfold round.
+rewrite <- F2R_Zopp.
+unfold F2R; simpl.
+apply f_equal2; apply f_equal.
+rewrite scaled_mantissa_opp.
+generalize (scaled_mantissa beta fexp x); intros r.
+unfold Zrnd_odd.
+case (Req_EM_T (- r) (Z2R (Zfloor (- r)))).
+case (Req_EM_T r (Z2R (Zfloor r))).
+intros Y1 Y2.
+apply eq_Z2R.
+now rewrite Z2R_opp, <- Y1, <-Y2.
+intros Y1 Y2.
+absurd (r=Z2R (Zfloor r)); trivial.
+pattern r at 2; replace r with (-(-r))%R by ring.
+rewrite Y2, <- Z2R_opp.
+rewrite Zfloor_Z2R.
+rewrite Z2R_opp, <- Y2.
+ring.
+case (Req_EM_T r (Z2R (Zfloor r))).
+intros Y1 Y2.
+absurd (-r=Z2R (Zfloor (-r)))%R; trivial.
+pattern r at 2; rewrite Y1.
+rewrite <- Z2R_opp, Zfloor_Z2R.
+now rewrite Z2R_opp, <- Y1.
+intros Y1 Y2.
+unfold Zceil; rewrite Ropp_involutive.
+replace (Zeven (Zfloor (- r))) with (negb (Zeven (Zfloor r))).
+case (Zeven (Zfloor r)); simpl; ring.
+apply trans_eq with (Zeven (Zceil r)).
+rewrite Zceil_floor_neq.
+rewrite Zeven_plus.
+simpl; reflexivity.
+now apply sym_not_eq.
+rewrite <- (Zeven_opp (Zfloor (- r))).
+reflexivity.
+apply canonic_exp_opp.
+Qed.
+
+
+
+Theorem round_odd_pt :
+ forall x,
+ Rnd_odd_pt x (round beta fexp Zrnd_odd x).
+Proof with auto with typeclass_instances.
+cut (forall x : R, (0 < x)%R -> Rnd_odd_pt x (round beta fexp Zrnd_odd x)).
+intros H x; case (Rle_or_lt 0 x).
+intros H1; destruct H1.
+now apply H.
+rewrite <- H0.
+rewrite round_0...
+split.
+apply generic_format_0.
+now left.
+intros Hx; apply Rnd_odd_pt_sym.
+rewrite <- round_odd_opp.
+apply H.
+auto with real.
+(* *)
+intros x Hxp.
+generalize (generic_format_round beta fexp Zrnd_odd x).
+set (o:=round beta fexp Zrnd_odd x).
+intros Ho.
+split.
+assumption.
+(* *)
+case (Req_dec o x); intros Hx.
+now left.
+right.
+assert (o=round beta fexp Zfloor x \/ o=round beta fexp Zceil x).
+unfold o, round, F2R;simpl.
+case (Zrnd_DN_or_UP Zrnd_odd (scaled_mantissa beta fexp x))...
+intros H; rewrite H; now left.
+intros H; rewrite H; now right.
+split.
+destruct H; rewrite H.
+left; apply round_DN_pt...
+right; apply round_UP_pt...
+(* *)
+unfold o, Zrnd_odd, round.
+case (Req_EM_T (scaled_mantissa beta fexp x)
+ (Z2R (Zfloor (scaled_mantissa beta fexp x)))).
+intros T.
+absurd (o=x); trivial.
+apply round_generic...
+unfold generic_format, F2R; simpl.
+rewrite <- (scaled_mantissa_mult_bpow beta fexp) at 1.
+apply f_equal2; trivial; rewrite T at 1.
+apply f_equal, sym_eq, Ztrunc_floor.
+apply Rmult_le_pos.
+now left.
+apply bpow_ge_0.
+intros L.
+case_eq (Zeven (Zfloor (scaled_mantissa beta fexp x))).
+(* . *)
+generalize (generic_format_round beta fexp Zceil x).
+unfold generic_format.
+set (f:=round beta fexp Zceil x).
+set (ef := canonic_exp beta fexp f).
+set (mf := Ztrunc (scaled_mantissa beta fexp f)).
+exists (Float beta mf ef).
+unfold Fcore_generic_fmt.canonic.
+rewrite <- H0.
+repeat split; try assumption.
+apply trans_eq with (negb (Zeven (Zfloor (scaled_mantissa beta fexp x)))).
+2: rewrite H1; reflexivity.
+apply trans_eq with (negb (Zeven (Fnum
+ (Float beta (Zfloor (scaled_mantissa beta fexp x)) (cexp x))))).
+2: reflexivity.
+case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)).
+rewrite <- round_0 with beta fexp Zfloor...
+apply round_le...
+now left.
+intros Y.
+generalize (DN_UP_parity_generic beta fexp)...
+unfold DN_UP_parity_prop.
+intros T; apply T with x; clear T.
+unfold generic_format.
+rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1.
+unfold F2R; simpl.
+apply Rmult_neq_compat_r.
+apply Rgt_not_eq, bpow_gt_0.
+rewrite Ztrunc_floor.
+assumption.
+apply Rmult_le_pos.
+now left.
+apply bpow_ge_0.
+unfold Fcore_generic_fmt.canonic.
+simpl.
+apply sym_eq, canonic_exp_DN...
+unfold Fcore_generic_fmt.canonic.
+rewrite <- H0; reflexivity.
+reflexivity.
+apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)).
+reflexivity.
+apply round_generic...
+intros Y.
+replace (Fnum {| Fnum := Zfloor (scaled_mantissa beta fexp x); Fexp := cexp x |})
+ with (Fnum (Float beta 0 (fexp (ln_beta beta 0)))).
+generalize (DN_UP_parity_generic beta fexp)...
+unfold DN_UP_parity_prop.
+intros T; apply T with x; clear T.
+unfold generic_format.
+rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1.
+unfold F2R; simpl.
+apply Rmult_neq_compat_r.
+apply Rgt_not_eq, bpow_gt_0.
+rewrite Ztrunc_floor.
+assumption.
+apply Rmult_le_pos.
+now left.
+apply bpow_ge_0.
+apply canonic_0.
+unfold Fcore_generic_fmt.canonic.
+rewrite <- H0; reflexivity.
+rewrite <- Y; unfold F2R; simpl; ring.
+apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)).
+reflexivity.
+apply round_generic...
+simpl.
+apply eq_Z2R, Rmult_eq_reg_r with (bpow (cexp x)).
+unfold round, F2R in Y; simpl in Y; rewrite <- Y.
+simpl; ring.
+apply Rgt_not_eq, bpow_gt_0.
+(* . *)
+intros Y.
+case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)).
+rewrite <- round_0 with beta fexp Zfloor...
+apply round_le...
+now left.
+intros Hrx.
+set (ef := canonic_exp beta fexp x).
+set (mf := Zfloor (scaled_mantissa beta fexp x)).
+exists (Float beta mf ef).
+unfold Fcore_generic_fmt.canonic.
+repeat split; try assumption.
+simpl.
+apply trans_eq with (cexp (round beta fexp Zfloor x )).
+apply sym_eq, canonic_exp_DN...
+reflexivity.
+intros Hrx; contradict Y.
+replace (Zfloor (scaled_mantissa beta fexp x)) with 0%Z.
+simpl; discriminate.
+apply eq_Z2R, Rmult_eq_reg_r with (bpow (cexp x)).
+unfold round, F2R in Hrx; simpl in Hrx; rewrite <- Hrx.
+simpl; ring.
+apply Rgt_not_eq, bpow_gt_0.
+Qed.
+
+End Fcore_rnd_odd.
+
+Section Odd_prop_aux.
+
+Variable beta : radix.
+Hypothesis Even_beta: Zeven (radix_val beta)=true.
+
+Notation bpow e := (bpow beta e).
+
+Variable fexp : Z -> Z.
+Variable fexpe : Z -> Z.
+
+Context { valid_exp : Valid_exp fexp }.
+Context { exists_NE_ : Exists_NE beta fexp }. (* for underflow reason *)
+Context { valid_expe : Valid_exp fexpe }.
+Context { exists_NE_e : Exists_NE beta fexpe }. (* for defining rounding to odd *)
+
+Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z.
+
+
+Lemma generic_format_fexpe_fexp: forall x,
+ generic_format beta fexp x -> generic_format beta fexpe x.
+Proof.
+intros x Hx.
+apply generic_inclusion_ln_beta with fexp; trivial; intros Hx2.
+generalize (fexpe_fexp (ln_beta beta x)).
+omega.
+Qed.
+
+
+
+Lemma exists_even_fexp_lt: forall (c:Z->Z), forall (x:R),
+ (exists f:float beta, F2R f = x /\ (c (ln_beta beta x) < Fexp f)%Z) ->
+ exists f:float beta, F2R f =x /\ canonic beta c f /\ Zeven (Fnum f) = true.
+Proof with auto with typeclass_instances.
+intros c x (g,(Hg1,Hg2)).
+exists (Float beta
+ (Fnum g*Z.pow (radix_val beta) (Fexp g - c (ln_beta beta x)))
+ (c (ln_beta beta x))).
+assert (F2R (Float beta
+ (Fnum g*Z.pow (radix_val beta) (Fexp g - c (ln_beta beta x)))
+ (c (ln_beta beta x))) = x).
+unfold F2R; simpl.
+rewrite Z2R_mult, Z2R_Zpower.
+rewrite Rmult_assoc, <- bpow_plus.
+rewrite <- Hg1; unfold F2R.
+apply f_equal, f_equal.
+ring.
+omega.
+split; trivial.
+split.
+unfold canonic, canonic_exp.
+now rewrite H.
+simpl.
+rewrite Zeven_mult.
+rewrite Zeven_Zpower.
+rewrite Even_beta.
+apply Bool.orb_true_intro.
+now right.
+omega.
+Qed.
+
+
+Variable choice:Z->bool.
+Variable x:R.
+
+
+Variable d u: float beta.
+Hypothesis Hd: Rnd_DN_pt (generic_format beta fexp) x (F2R d).
+Hypothesis Cd: canonic beta fexp d.
+Hypothesis Hu: Rnd_UP_pt (generic_format beta fexp) x (F2R u).
+Hypothesis Cu: canonic beta fexp u.
+
+Hypothesis xPos: (0 < x)%R.
+
+
+Let m:= ((F2R d+F2R u)/2)%R.
+
+
+Lemma d_eq: F2R d= round beta fexp Zfloor x.
+Proof with auto with typeclass_instances.
+apply Rnd_DN_pt_unicity with (generic_format beta fexp) x...
+apply round_DN_pt...
+Qed.
+
+
+Lemma u_eq: F2R u= round beta fexp Zceil x.
+Proof with auto with typeclass_instances.
+apply Rnd_UP_pt_unicity with (generic_format beta fexp) x...
+apply round_UP_pt...
+Qed.
+
+
+Lemma d_ge_0: (0 <= F2R d)%R.
+Proof with auto with typeclass_instances.
+rewrite d_eq; apply round_ge_generic...
+apply generic_format_0.
+now left.
+Qed.
+
+
+
+Lemma ln_beta_d: (0< F2R d)%R ->
+ (ln_beta beta (F2R d) = ln_beta beta x :>Z).
+Proof with auto with typeclass_instances.
+intros Y.
+rewrite d_eq; apply ln_beta_round_DN...
+now rewrite <- d_eq.
+Qed.
+
+
+Lemma Fexp_d: (0 < F2R d)%R -> Fexp d =fexp (ln_beta beta x).
+Proof with auto with typeclass_instances.
+intros Y.
+now rewrite Cd, <- ln_beta_d.
+Qed.
+
+
+
+Lemma format_bpow_x: (0 < F2R d)%R
+ -> generic_format beta fexp (bpow (ln_beta beta x)).
+Proof with auto with typeclass_instances.
+intros Y.
+apply generic_format_bpow.
+apply valid_exp.
+rewrite <- Fexp_d; trivial.
+apply Zlt_le_trans with (ln_beta beta (F2R d))%Z.
+rewrite Cd; apply ln_beta_generic_gt...
+now apply Rgt_not_eq.
+apply Hd.
+apply ln_beta_le; trivial.
+apply Hd.
+Qed.
+
+
+Lemma format_bpow_d: (0 < F2R d)%R ->
+ generic_format beta fexp (bpow (ln_beta beta (F2R d))).
+Proof with auto with typeclass_instances.
+intros Y; apply generic_format_bpow.
+apply valid_exp.
+apply ln_beta_generic_gt...
+now apply Rgt_not_eq.
+now apply generic_format_canonic.
+Qed.
+
+
+Lemma d_le_m: (F2R d <= m)%R.
+apply Rmult_le_reg_l with 2%R.
+auto with real.
+apply Rplus_le_reg_l with (-F2R d)%R.
+apply Rle_trans with (F2R d).
+right; ring.
+apply Rle_trans with (F2R u).
+apply Rle_trans with x.
+apply Hd.
+apply Hu.
+right; unfold m; field.
+Qed.
+
+Lemma m_le_u: (m <= F2R u)%R.
+apply Rmult_le_reg_l with 2%R.
+auto with real.
+apply Rplus_le_reg_l with (-F2R u)%R.
+apply Rle_trans with (F2R d).
+right; unfold m; field.
+apply Rle_trans with (F2R u).
+apply Rle_trans with x.
+apply Hd.
+apply Hu.
+right; ring.
+Qed.
+
+Lemma ln_beta_m: (0 < F2R d)%R -> (ln_beta beta m =ln_beta beta (F2R d) :>Z).
+Proof with auto with typeclass_instances.
+intros dPos; apply ln_beta_unique_pos.
+split.
+apply Rle_trans with (F2R d).
+destruct (ln_beta beta (F2R d)) as (e,He).
+simpl.
+rewrite Rabs_right in He.
+apply He.
+now apply Rgt_not_eq.
+apply Rle_ge; now left.
+apply d_le_m.
+case m_le_u; intros H.
+apply Rlt_le_trans with (1:=H).
+rewrite u_eq.
+apply round_le_generic...
+apply generic_format_bpow.
+apply valid_exp.
+apply ln_beta_generic_gt...
+now apply Rgt_not_eq.
+now apply generic_format_canonic.
+case (Rle_or_lt x (bpow (ln_beta beta (F2R d)))); trivial; intros Z.
+absurd ((bpow (ln_beta beta (F2R d)) <= (F2R d)))%R.
+apply Rlt_not_le.
+destruct (ln_beta beta (F2R d)) as (e,He).
+simpl in *; rewrite Rabs_right in He.
+apply He.
+now apply Rgt_not_eq.
+apply Rle_ge; now left.
+apply Rle_trans with (round beta fexp Zfloor x).
+2: right; apply sym_eq, d_eq.
+apply round_ge_generic...
+apply generic_format_bpow.
+apply valid_exp.
+apply ln_beta_generic_gt...
+now apply Rgt_not_eq.
+now apply generic_format_canonic.
+now left.
+replace m with (F2R d).
+destruct (ln_beta beta (F2R d)) as (e,He).
+simpl in *; rewrite Rabs_right in He.
+apply He.
+now apply Rgt_not_eq.
+apply Rle_ge; now left.
+assert (F2R d = F2R u).
+apply Rmult_eq_reg_l with (/2)%R.
+apply Rplus_eq_reg_l with (/2*F2R u)%R.
+apply trans_eq with m.
+unfold m, Rdiv; ring.
+rewrite H; field.
+auto with real.
+apply Rgt_not_eq, Rlt_gt; auto with real.
+unfold m; rewrite <- H0; field.
+Qed.
+
+
+Lemma ln_beta_m_0: (0 = F2R d)%R
+ -> (ln_beta beta m =ln_beta beta (F2R u)-1:>Z)%Z.
+Proof with auto with typeclass_instances.
+intros Y.
+apply ln_beta_unique_pos.
+unfold m; rewrite <- Y, Rplus_0_l.
+rewrite u_eq.
+destruct (ln_beta beta x) as (e,He).
+rewrite Rabs_right in He.
+rewrite round_UP_small_pos with (ex:=e).
+rewrite ln_beta_bpow.
+ring_simplify (fexp e + 1 - 1)%Z.
+split.
+unfold Zminus; rewrite bpow_plus.
+unfold Rdiv; apply Rmult_le_compat_l.
+apply bpow_ge_0.
+simpl; unfold Z.pow_pos; simpl.
+rewrite Zmult_1_r; apply Rinv_le.
+auto with real.
+apply (Z2R_le 2).
+specialize (radix_gt_1 beta).
+omega.
+apply Rlt_le_trans with (bpow (fexp e)*1)%R.
+2: right; ring.
+unfold Rdiv; apply Rmult_lt_compat_l.
+apply bpow_gt_0.
+rewrite <- Rinv_1 at 3.
+apply Rinv_lt; auto with real.
+now apply He, Rgt_not_eq.
+apply exp_small_round_0_pos with beta (Zfloor) x...
+now apply He, Rgt_not_eq.
+now rewrite <- d_eq, Y.
+now left.
+Qed.
+
+
+
+
+
+Lemma u'_eq: (0 < F2R d)%R -> exists f:float beta, F2R f = F2R u /\ (Fexp f = Fexp d)%Z.
+Proof with auto with typeclass_instances.
+intros Y.
+rewrite u_eq; unfold round.
+eexists; repeat split.
+simpl; now rewrite Fexp_d.
+Qed.
+
+
+
+
+Lemma m_eq: (0 < F2R d)%R -> exists f:float beta,
+ F2R f = m /\ (Fexp f = fexp (ln_beta beta x) -1)%Z.
+Proof with auto with typeclass_instances.
+intros Y.
+specialize (Zeven_ex (radix_val beta)); rewrite Even_beta.
+intros (b, Hb); rewrite Zplus_0_r in Hb.
+destruct u'_eq as (u', (Hu'1,Hu'2)); trivial.
+exists (Fmult beta (Float beta b (-1)) (Fplus beta d u'))%R.
+split.
+rewrite F2R_mult, F2R_plus, Hu'1.
+unfold m; rewrite Rmult_comm.
+unfold Rdiv; apply f_equal.
+unfold F2R; simpl; unfold Z.pow_pos; simpl.
+rewrite Zmult_1_r, Hb, Z2R_mult.
+simpl; field.
+apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
+simpl; auto with real.
+rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply radix_pos.
+apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z.
+unfold Fmult.
+destruct (Fplus beta d u'); reflexivity.
+rewrite Zplus_comm; unfold Zminus; apply f_equal2.
+2: reflexivity.
+rewrite Fexp_Fplus.
+rewrite Z.min_l.
+now rewrite Fexp_d.
+rewrite Hu'2; omega.
+Qed.
+
+Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta,
+ F2R f = m /\ (Fexp f = fexp (ln_beta beta (F2R u)) -1)%Z.
+Proof with auto with typeclass_instances.
+intros Y.
+specialize (Zeven_ex (radix_val beta)); rewrite Even_beta.
+intros (b, Hb); rewrite Zplus_0_r in Hb.
+exists (Fmult beta (Float beta b (-1)) u)%R.
+split.
+rewrite F2R_mult; unfold m; rewrite <- Y, Rplus_0_l.
+rewrite Rmult_comm.
+unfold Rdiv; apply f_equal.
+unfold F2R; simpl; unfold Z.pow_pos; simpl.
+rewrite Zmult_1_r, Hb, Z2R_mult.
+simpl; field.
+apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
+simpl; auto with real.
+rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply radix_pos.
+apply trans_eq with (-1+Fexp u)%Z.
+unfold Fmult.
+destruct u; reflexivity.
+rewrite Zplus_comm, Cu; unfold Zminus; now apply f_equal2.
+Qed.
+
+Lemma fexp_m_eq_0: (0 = F2R d)%R ->
+ (fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z.
+Proof with auto with typeclass_instances.
+intros Y.
+assert ((fexp (ln_beta beta (F2R u) - 1) <= fexp (ln_beta beta (F2R u))))%Z.
+2: omega.
+destruct (ln_beta beta x) as (e,He).
+rewrite Rabs_right in He.
+2: now left.
+assert (e <= fexp e)%Z.
+apply exp_small_round_0_pos with beta (Zfloor) x...
+now apply He, Rgt_not_eq.
+now rewrite <- d_eq, Y.
+rewrite u_eq, round_UP_small_pos with (ex:=e); trivial.
+2: now apply He, Rgt_not_eq.
+rewrite ln_beta_bpow.
+ring_simplify (fexp e + 1 - 1)%Z.
+replace (fexp (fexp e)) with (fexp e).
+case exists_NE_; intros V.
+contradict V; rewrite Even_beta; discriminate.
+rewrite (proj2 (V e)); omega.
+apply sym_eq, valid_exp; omega.
+Qed.
+
+Lemma Fm: generic_format beta fexpe m.
+case (d_ge_0); intros Y.
+(* *)
+destruct m_eq as (g,(Hg1,Hg2)); trivial.
+apply generic_format_F2R' with g.
+now apply sym_eq.
+intros H; unfold canonic_exp; rewrite Hg2.
+rewrite ln_beta_m; trivial.
+rewrite <- Fexp_d; trivial.
+rewrite Cd.
+unfold canonic_exp.
+generalize (fexpe_fexp (ln_beta beta (F2R d))).
+omega.
+(* *)
+destruct m_eq_0 as (g,(Hg1,Hg2)); trivial.
+apply generic_format_F2R' with g.
+assumption.
+intros H; unfold canonic_exp; rewrite Hg2.
+rewrite ln_beta_m_0; try assumption.
+apply Zle_trans with (1:=fexpe_fexp _).
+assert (fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z;[idtac|omega].
+now apply fexp_m_eq_0.
+Qed.
+
+
+
+Lemma Zm:
+ exists g : float beta, F2R g = m /\ canonic beta fexpe g /\ Zeven (Fnum g) = true.
+Proof with auto with typeclass_instances.
+case (d_ge_0); intros Y.
+(* *)
+destruct m_eq as (g,(Hg1,Hg2)); trivial.
+apply exists_even_fexp_lt.
+exists g; split; trivial.
+rewrite Hg2.
+rewrite ln_beta_m; trivial.
+rewrite <- Fexp_d; trivial.
+rewrite Cd.
+unfold canonic_exp.
+generalize (fexpe_fexp (ln_beta beta (F2R d))).
+omega.
+(* *)
+destruct m_eq_0 as (g,(Hg1,Hg2)); trivial.
+apply exists_even_fexp_lt.
+exists g; split; trivial.
+rewrite Hg2.
+rewrite ln_beta_m_0; trivial.
+apply Zle_lt_trans with (1:=fexpe_fexp _).
+assert (fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z;[idtac|omega].
+now apply fexp_m_eq_0.
+Qed.
+
+
+Lemma DN_odd_d_aux: forall z, (F2R d<= z< F2R u)%R ->
+ Rnd_DN_pt (generic_format beta fexp) z (F2R d).
+Proof with auto with typeclass_instances.
+intros z Hz1.
+replace (F2R d) with (round beta fexp Zfloor z).
+apply round_DN_pt...
+case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zfloor z)).
+apply generic_format_round...
+intros Y; apply Rle_antisym; trivial.
+apply round_DN_pt...
+apply Hd.
+apply Hz1.
+intros Y; absurd (z < z)%R.
+auto with real.
+apply Rlt_le_trans with (1:=proj2 Hz1), Rle_trans with (1:=Y).
+apply round_DN_pt...
+Qed.
+
+Lemma UP_odd_d_aux: forall z, (F2R d< z <= F2R u)%R ->
+ Rnd_UP_pt (generic_format beta fexp) z (F2R u).
+Proof with auto with typeclass_instances.
+intros z Hz1.
+replace (F2R u) with (round beta fexp Zceil z).
+apply round_UP_pt...
+case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zceil z)).
+apply generic_format_round...
+intros Y; absurd (z < z)%R.
+auto with real.
+apply Rle_lt_trans with (2:=proj1 Hz1), Rle_trans with (2:=Y).
+apply round_UP_pt...
+intros Y; apply Rle_antisym; trivial.
+apply round_UP_pt...
+apply Hu.
+apply Hz1.
+Qed.
+
+
+Theorem round_odd_prop_pos:
+ round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
+ round beta fexp (Znearest choice) x.
+Proof with auto with typeclass_instances.
+set (o:=round beta fexpe Zrnd_odd x).
+case (generic_format_EM beta fexp x); intros Hx.
+replace o with x; trivial.
+unfold o; apply sym_eq, round_generic...
+now apply generic_format_fexpe_fexp.
+assert (K1:(F2R d <= o)%R).
+apply round_ge_generic...
+apply generic_format_fexpe_fexp, Hd.
+apply Hd.
+assert (K2:(o <= F2R u)%R).
+apply round_le_generic...
+apply generic_format_fexpe_fexp, Hu.
+apply Hu.
+assert (P:(x <> m -> o=m -> (forall P:Prop, P))).
+intros Y1 Y2.
+assert (H:(Rnd_odd_pt beta fexpe x o)).
+apply round_odd_pt...
+destruct H as (_,H); destruct H.
+absurd (x=m)%R; try trivial.
+now rewrite <- Y2, H.
+destruct H as (_,(k,(Hk1,(Hk2,Hk3)))).
+destruct Zm as (k',(Hk'1,(Hk'2,Hk'3))).
+absurd (true=false).
+discriminate.
+rewrite <- Hk3, <- Hk'3.
+apply f_equal, f_equal.
+apply canonic_unicity with fexpe...
+now rewrite Hk'1, <- Y2.
+assert (generic_format beta fexp o -> (forall P:Prop, P)).
+intros Y.
+assert (H:(Rnd_odd_pt beta fexpe x o)).
+apply round_odd_pt...
+destruct H as (_,H); destruct H.
+absurd (generic_format beta fexp x); trivial.
+now rewrite <- H.
+destruct H as (_,(k,(Hk1,(Hk2,Hk3)))).
+destruct (exists_even_fexp_lt fexpe o) as (k',(Hk'1,(Hk'2,Hk'3))).
+eexists; split.
+apply sym_eq, Y.
+simpl; unfold canonic_exp.
+apply Zle_lt_trans with (1:=fexpe_fexp _).
+omega.
+absurd (true=false).
+discriminate.
+rewrite <- Hk3, <- Hk'3.
+apply f_equal, f_equal.
+apply canonic_unicity with fexpe...
+now rewrite Hk'1, <- Hk1.
+case K1; clear K1; intros K1.
+2: apply H; rewrite <- K1; apply Hd.
+case K2; clear K2; intros K2.
+2: apply H; rewrite K2; apply Hu.
+case (Rle_or_lt x m); intros Y;[destruct Y|idtac].
+(* . *)
+apply trans_eq with (F2R d).
+apply round_N_DN_betw with (F2R u)...
+apply DN_odd_d_aux; split; try left; assumption.
+apply UP_odd_d_aux; split; try left; assumption.
+split.
+apply round_ge_generic...
+apply generic_format_fexpe_fexp, Hd.
+apply Hd.
+assert (o <= (F2R d + F2R u) / 2)%R.
+apply round_le_generic...
+apply Fm.
+now left.
+destruct H1; trivial.
+apply P.
+now apply Rlt_not_eq.
+trivial.
+apply sym_eq, round_N_DN_betw with (F2R u)...
+split.
+apply Hd.
+exact H0.
+(* . *)
+replace o with x.
+reflexivity.
+apply sym_eq, round_generic...
+rewrite H0; apply Fm.
+(* . *)
+apply trans_eq with (F2R u).
+apply round_N_UP_betw with (F2R d)...
+apply DN_odd_d_aux; split; try left; assumption.
+apply UP_odd_d_aux; split; try left; assumption.
+split.
+assert ((F2R d + F2R u) / 2 <= o)%R.
+apply round_ge_generic...
+apply Fm.
+now left.
+destruct H0; trivial.
+apply P.
+now apply Rgt_not_eq.
+rewrite <- H0; trivial.
+apply round_le_generic...
+apply generic_format_fexpe_fexp, Hu.
+apply Hu.
+apply sym_eq, round_N_UP_betw with (F2R d)...
+split.
+exact Y.
+apply Hu.
+Qed.
+
+
+End Odd_prop_aux.
+
+Section Odd_prop.
+
+Variable beta : radix.
+Hypothesis Even_beta: Zeven (radix_val beta)=true.
+
+Variable fexp : Z -> Z.
+Variable fexpe : Z -> Z.
+Variable choice:Z->bool.
+
+Context { valid_exp : Valid_exp fexp }.
+Context { exists_NE_ : Exists_NE beta fexp }. (* for underflow reason *)
+Context { valid_expe : Valid_exp fexpe }.
+Context { exists_NE_e : Exists_NE beta fexpe }. (* for defining rounding to odd *)
+
+Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z.
+
+
+Theorem canonizer: forall f, generic_format beta fexp f
+ -> exists g : float beta, f = F2R g /\ canonic beta fexp g.
+Proof with auto with typeclass_instances.
+intros f Hf.
+exists (Float beta (Ztrunc (scaled_mantissa beta fexp f)) (canonic_exp beta fexp f)).
+assert (L:(f = F2R (Float beta (Ztrunc (scaled_mantissa beta fexp f)) (canonic_exp beta fexp f)))).
+apply trans_eq with (round beta fexp Ztrunc f).
+apply sym_eq, round_generic...
+reflexivity.
+split; trivial.
+unfold canonic; rewrite <- L.
+reflexivity.
+Qed.
+
+
+
+
+Theorem round_odd_prop: forall x,
+ round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
+ round beta fexp (Znearest choice) x.
+Proof with auto with typeclass_instances.
+intros x.
+case (total_order_T x 0); intros H; [case H; clear H; intros H | idtac].
+rewrite <- (Ropp_involutive x).
+rewrite round_odd_opp.
+rewrite 2!round_N_opp.
+apply f_equal.
+destruct (canonizer (round beta fexp Zfloor (-x))) as (d,(Hd1,Hd2)).
+apply generic_format_round...
+destruct (canonizer (round beta fexp Zceil (-x))) as (u,(Hu1,Hu2)).
+apply generic_format_round...
+apply round_odd_prop_pos with d u...
+rewrite <- Hd1; apply round_DN_pt...
+rewrite <- Hu1; apply round_UP_pt...
+auto with real.
+(* . *)
+rewrite H; repeat rewrite round_0...
+(* . *)
+destruct (canonizer (round beta fexp Zfloor x)) as (d,(Hd1,Hd2)).
+apply generic_format_round...
+destruct (canonizer (round beta fexp Zceil x)) as (u,(Hu1,Hu2)).
+apply generic_format_round...
+apply round_odd_prop_pos with d u...
+rewrite <- Hd1; apply round_DN_pt...
+rewrite <- Hu1; apply round_UP_pt...
+Qed.
+
+
+End Odd_prop.