(**
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.