From Coq Require Import ZArith Reals Psatz.

Require Import Core Operations.

Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with
  | left _ ⇒ Zfloor x
  | right _ ⇒ match (Z.even (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 ≠ (IZR (Zfloor x)) →
  (Z.even (Zrnd_odd x)) = false.

Lemma Zfloor_plus: ∀ (n:Z) y,
  (Zfloor (IZR n+y) = n + Zfloor y)%Z.

Lemma Zceil_plus: ∀ (n:Z) y,
  (Zceil (IZR n+y) = n + Zceil y)%Z.

Lemma Zeven_abs: ∀ z, Z.even (Z.abs z) = Z.even z.

Lemma Zrnd_odd_plus: ∀ x y, (x = IZR (Zfloor x)) →
    Z.even (Zfloor x) = true →
   (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.

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 canonical := (canonical beta fexp).
Notation cexp := (cexp 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 ∧ canonical g ∧ Z.even (Fnum g) = false)).

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

Theorem Rnd_odd_pt_opp_inv : ∀ 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_unique :
  ∀ 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: Z.even (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 (mag beta x) < Fexp f)%Z) →
      ∃ f:float beta, F2R f =x ∧ canonical beta c f ∧ Z.even (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: canonical beta fexp d.
Hypothesis Hu: Rnd_UP_pt (generic_format beta fexp) x (F2R u).
Hypothesis Cu: canonical 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 mag_d: (0< F2R d)%R →
    (mag beta (F2R d) = mag beta x :>Z).

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

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

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

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

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

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

Lemma mag_m_0: (0 = F2R d)%R
    → (mag beta m =mag 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 (mag beta x) - 1)%Z.

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

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

Lemma Fm: generic_format beta fexpe m.

Lemma Zm:
   ∃ g : float beta, F2R g = m ∧ canonical beta fexpe g ∧ Z.even (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).

Lemma round_N_odd_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: Z.even (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 round_N_odd :
  ∀ x,
  round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) =
               round beta fexp (Znearest choice) x.

End Odd_prop.

Section Odd_propbis.

Variable beta : radix.
Hypothesis Even_beta: Z.even (radix_val beta)=true.

Variable emin prec:Z.
Variable choice:Z→bool.

Hypothesis prec_gt_1: (1 < prec)%Z.

Notation format := (generic_format beta (FLT_exp emin prec)).
Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)).
Notation cexp_flt := (cexp beta (FLT_exp emin prec)).
Notation fexpe k := (FLT_exp (emin-k) (prec+k)).

Lemma Zrnd_odd_plus': ∀ x y,
  (∃ n:Z, ∃ e:Z, (x = IZR n×bpow beta e)%R ∧ (1 ≤ e)%Z) →
   (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R.

Theorem mag_round_odd: ∀ (x:R),
 (emin < mag beta x)%Z →
  (mag_val beta _ (mag beta (round beta (FLT_exp emin prec) Zrnd_odd x))
      = mag_val beta x (mag beta x))%Z.

Theorem fexp_round_odd: ∀ (x:R),
  (cexp_flt (round beta (FLT_exp emin prec) Zrnd_odd x)
      = cexp_flt x)%Z.

End Odd_propbis.