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.

Lemma Zrnd_odd_Zodd: ∀ x, x ≠ (Z2R (Zfloor x)) →
  (Zeven (Zrnd_odd x)) = false.

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) ∧
    ∃ g : float beta, f = F2R g ∧ canonic g ∧ Zeven (Fnum g) = false)).

Definition Rnd_odd (rnd : R → R) :=
  ∀ x : R, Rnd_odd_pt x (rnd x).

Theorem Rnd_odd_pt_sym : ∀ x f : R,
  Rnd_odd_pt (-x) (-f) → Rnd_odd_pt x f.

Theorem round_odd_opp :
  ∀ x,
  (round beta fexp Zrnd_odd (-x) = (- round beta fexp Zrnd_odd x))%R.

Theorem round_odd_pt :
  ∀ x,
  Rnd_odd_pt x (round beta fexp Zrnd_odd x).

Theorem Rnd_odd_pt_unicity :
  ∀ x f1 f2 : R,
  Rnd_odd_pt x f1 → Rnd_odd_pt x f2 →
  f1 = f2.

Theorem Rnd_odd_pt_monotone :
  round_pred_monotone (Rnd_odd_pt).

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 }. Context { valid_expe : Valid_exp fexpe }.
Context { exists_NE_e : Exists_NE beta fexpe }.
Hypothesis fexpe_fexp: ∀ e, (fexpe e ≤ fexp e -2)%Z.

Lemma generic_format_fexpe_fexp: ∀ x,
 generic_format beta fexp x → generic_format beta fexpe x.

Lemma exists_even_fexp_lt: ∀ (c:Z→Z), ∀ (x:R),
      (∃ f:float beta, F2R f = x ∧ (c (ln_beta beta x) < Fexp f)%Z) →
      ∃ f:float beta, F2R f =x ∧ canonic beta c f ∧ Zeven (Fnum f) = true.

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.

Lemma u_eq: F2R u= round beta fexp Zceil x.

Lemma d_ge_0: (0 ≤ F2R d)%R.

Lemma ln_beta_d: (0< F2R d)%R →
    (ln_beta beta (F2R d) = ln_beta beta x :>Z).

Lemma Fexp_d: (0 < F2R d)%R → Fexp d =fexp (ln_beta beta x).

Lemma format_bpow_x: (0 < F2R d)%R
    → generic_format beta fexp (bpow (ln_beta beta x)).

Lemma format_bpow_d: (0 < F2R d)%R →
  generic_format beta fexp (bpow (ln_beta beta (F2R d))).

Lemma d_le_m: (F2R d ≤ m)%R.

Lemma m_le_u: (m ≤ F2R u)%R.

Lemma ln_beta_m: (0 < F2R d)%R → (ln_beta beta m =ln_beta beta (F2R d) :>Z).

Lemma ln_beta_m_0: (0 = F2R d)%R
    → (ln_beta beta m =ln_beta beta (F2R u)-1:>Z)%Z.

Lemma u'_eq: (0 < F2R d)%R → ∃ f:float beta, F2R f = F2R u ∧ (Fexp f = Fexp d)%Z.

Lemma m_eq: (0 < F2R d)%R → ∃ f:float beta,
   F2R f = m ∧ (Fexp f = fexp (ln_beta beta x) -1)%Z.

Lemma m_eq_0: (0 = F2R d)%R → ∃ f:float beta,
   F2R f = m ∧ (Fexp f = fexp (ln_beta beta (F2R u)) -1)%Z.

Lemma fexp_m_eq_0: (0 = F2R d)%R →
  (fexp (ln_beta beta (F2R u)-1) < fexp (ln_beta beta (F2R u))+1)%Z.

Lemma Fm: generic_format beta fexpe m.

Lemma Zm:
   ∃ g : float beta, F2R g = m ∧ canonic beta fexpe g ∧ Zeven (Fnum g) = true.

Lemma DN_odd_d_aux: ∀ z, (F2R d≤ z< F2R u)%R →
    Rnd_DN_pt (generic_format beta fexp) z (F2R d).

Lemma UP_odd_d_aux: ∀ z, (F2R d< z ≤ F2R u)%R →
    Rnd_UP_pt (generic_format beta fexp) z (F2R u).

Theorem round_odd_prop_pos:
  round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
               round beta fexp (Znearest choice) x.

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 }. Context { valid_expe : Valid_exp fexpe }.
Context { exists_NE_e : Exists_NE beta fexpe }.
Hypothesis fexpe_fexp: ∀ e, (fexpe e ≤ fexp e -2)%Z.

Theorem canonizer: ∀ f, generic_format beta fexp f
   → ∃ g : float beta, f = F2R g ∧ canonic beta fexp g.

Theorem round_odd_prop: ∀ x,
  round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
               round beta fexp (Znearest choice) x.

End Odd_prop.