From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Round_pred Float_prop.

Section Generic.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Section Format.

Variable fexp : Z → Z.

Class Valid_exp :=
  valid_exp :
  ∀ k : Z,
  ( (fexp k < k)%Z → (fexp (k + 1) ≤ k)%Z ) ∧
  ( (k ≤ fexp k)%Z →
    (fexp (fexp k + 1) ≤ fexp k)%Z ∧
    ∀ l : Z, (l ≤ fexp k)%Z → fexp l = fexp k ).

Context { valid_exp_ : Valid_exp }.

Theorem valid_exp_large :
  ∀ k l,
  (fexp k < k)%Z → (k ≤ l)%Z →
  (fexp l < l)%Z.

Theorem valid_exp_large' :
  ∀ k l,
  (fexp k < k)%Z → (l ≤ k)%Z →
  (fexp l < k)%Z.

Definition cexp x :=
  fexp (mag beta x).

Definition canonical (f : float beta) :=
  Fexp f = cexp (F2R f).

Definition scaled_mantissa x :=
  (x × bpow (- cexp x))%R.

Definition generic_format (x : R) :=
  x = F2R (Float beta (Ztrunc (scaled_mantissa x)) (cexp x)).

Theorem generic_format_0 :
  generic_format 0.

Theorem cexp_opp :
  ∀ x,
  cexp (-x) = cexp x.

Theorem cexp_abs :
  ∀ x,
  cexp (Rabs x) = cexp x.

Theorem canonical_generic_format :
  ∀ x,
  generic_format x →
  ∃ f : float beta,
  x = F2R f ∧ canonical f.

Theorem generic_format_bpow :
  ∀ e, (fexp (e + 1) ≤ e)%Z →
  generic_format (bpow e).

Theorem generic_format_bpow' :
  ∀ e, (fexp e ≤ e)%Z →
  generic_format (bpow e).

Theorem generic_format_F2R :
  ∀ m e,
  ( m ≠ 0 → cexp (F2R (Float beta m e)) ≤ e )%Z →
  generic_format (F2R (Float beta m e)).

Lemma generic_format_F2R' :
  ∀ (x : R) (f : float beta),
  F2R f = x →
  (x ≠ 0%R → (cexp x ≤ Fexp f)%Z) →
  generic_format x.

Theorem canonical_opp :
  ∀ m e,
  canonical (Float beta m e) →
  canonical (Float beta (-m) e).

Theorem canonical_abs :
  ∀ m e,
  canonical (Float beta m e) →
  canonical (Float beta (Z.abs m) e).

Theorem canonical_0 :
  canonical (Float beta 0 (fexp (mag beta 0%R))).

Theorem canonical_unique :
  ∀ f1 f2,
  canonical f1 →
  canonical f2 →
  F2R f1 = F2R f2 →
  f1 = f2.

Theorem scaled_mantissa_generic :
  ∀ x,
  generic_format x →
  scaled_mantissa x = IZR (Ztrunc (scaled_mantissa x)).

Theorem scaled_mantissa_mult_bpow :
  ∀ x,
  (scaled_mantissa x × bpow (cexp x))%R = x.

Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = 0%R.

Theorem scaled_mantissa_opp :
  ∀ x,
  scaled_mantissa (-x) = (-scaled_mantissa x)%R.

Theorem scaled_mantissa_abs :
  ∀ x,
  scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).

Theorem generic_format_opp :
  ∀ x, generic_format x → generic_format (-x).

Theorem generic_format_abs :
  ∀ x, generic_format x → generic_format (Rabs x).

Theorem generic_format_abs_inv :
  ∀ x, generic_format (Rabs x) → generic_format x.

Theorem cexp_fexp :
  ∀ x ex,
  (bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
  cexp x = fexp ex.

Theorem cexp_fexp_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  cexp x = fexp ex.

Theorem mantissa_small_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  (0 < x × bpow (- fexp ex) < 1)%R.

Theorem scaled_mantissa_lt_1 :
  ∀ x ex,
  (Rabs x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  (Rabs (scaled_mantissa x) < 1)%R.

Theorem scaled_mantissa_lt_bpow :
  ∀ x,
  (Rabs (scaled_mantissa x) < bpow (mag beta x - cexp x))%R.

Theorem mag_generic_gt :
  ∀ x, (x ≠ 0)%R →
  generic_format x →
  (cexp x < mag beta x)%Z.

Lemma mantissa_DN_small_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  Zfloor (x × bpow (- fexp ex)) = Z0.

Lemma mantissa_UP_small_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  Zceil (x × bpow (- fexp ex)) = 1%Z.

Theorem generic_format_discrete :
  ∀ x m,
  let e := cexp x in
  (F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R →
  ¬ generic_format x.

Theorem generic_format_canonical :
  ∀ f, canonical f →
  generic_format (F2R f).

Theorem generic_format_ge_bpow :
  ∀ emin,
  ( ∀ e, (emin ≤ fexp e)%Z ) →
  ∀ x,
  (0 < x)%R →
  generic_format x →
  (bpow emin ≤ x)%R.

Theorem abs_lt_bpow_prec:
  ∀ prec,
  (∀ e, (e - prec ≤ fexp e)%Z) →
  
  ∀ x,
  (Rabs x < bpow (prec + cexp x))%R.

Theorem generic_format_bpow_inv' :
  ∀ e,
  generic_format (bpow e) →
  (fexp (e + 1) ≤ e)%Z.

Theorem generic_format_bpow_inv :
  ∀ e,
  generic_format (bpow e) →
  (fexp e ≤ e)%Z.

Section Fcore_generic_round_pos.

Variable rnd : R → Z.

Class Valid_rnd := {
  Zrnd_le : ∀ x y, (x ≤ y)%R → (rnd x ≤ rnd y)%Z ;
  Zrnd_IZR : ∀ n, rnd (IZR n) = n
}.

Context { valid_rnd : Valid_rnd }.

Theorem Zrnd_DN_or_UP :
  ∀ x, rnd x = Zfloor x ∨ rnd x = Zceil x.

Theorem Zrnd_ZR_or_AW :
  ∀ x, rnd x = Ztrunc x ∨ rnd x = Zaway x.

Definition round x :=
  F2R (Float beta (rnd (scaled_mantissa x)) (cexp x)).

Theorem round_bounded_large_pos :
  ∀ x ex,
  (fexp ex < ex)%Z →
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (bpow (ex - 1) ≤ round x ≤ bpow ex)%R.

Theorem round_bounded_small_pos :
  ∀ x ex,
  (ex ≤ fexp ex)%Z →
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  round x = 0%R ∨ round x = bpow (fexp ex).

Lemma round_le_pos :
  ∀ x y, (0 < x)%R → (x ≤ y)%R → (round x ≤ round y)%R.

Theorem round_generic :
  ∀ x,
  generic_format x →
  round x = x.

Theorem round_0 :
  round 0 = 0%R.

Theorem exp_small_round_0_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  round x = 0%R → (ex ≤ fexp ex)%Z .

Lemma generic_format_round_pos :
  ∀ x,
  (0 < x)%R →
  generic_format (round x).

End Fcore_generic_round_pos.

Theorem round_ext :
  ∀ rnd1 rnd2,
  ( ∀ x, rnd1 x = rnd2 x ) →
  ∀ x,
  round rnd1 x = round rnd2 x.

Section Zround_opp.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Definition Zrnd_opp x := Z.opp (rnd (-x)).

Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.

Theorem round_opp :
  ∀ x,
  round rnd (- x) = Ropp (round Zrnd_opp x).

End Zround_opp.

Global Instance valid_rnd_DN : Valid_rnd Zfloor.

Global Instance valid_rnd_UP : Valid_rnd Zceil.

Global Instance valid_rnd_ZR : Valid_rnd Ztrunc.

Global Instance valid_rnd_AW : Valid_rnd Zaway.

Section monotone.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem round_DN_or_UP :
  ∀ x,
  round rnd x = round Zfloor x ∨ round rnd x = round Zceil x.

Theorem round_ZR_or_AW :
  ∀ x,
  round rnd x = round Ztrunc x ∨ round rnd x = round Zaway x.

Theorem round_le :
  ∀ x y, (x ≤ y)%R → (round rnd x ≤ round rnd y)%R.

Theorem round_ge_generic :
  ∀ x y, generic_format x → (x ≤ y)%R → (x ≤ round rnd y)%R.

Theorem round_le_generic :
  ∀ x y, generic_format y → (x ≤ y)%R → (round rnd x ≤ y)%R.

End monotone.

Theorem round_abs_abs :
  ∀ P : R → R → Prop,
  ( ∀ rnd (Hr : Valid_rnd rnd) x, (0 ≤ x)%R → P x (round rnd x) ) →
  ∀ rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).

Theorem round_bounded_large :
  ∀ rnd {Hr : Valid_rnd rnd} x ex,
  (fexp ex < ex)%Z →
  (bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
  (bpow (ex - 1) ≤ Rabs (round rnd x) ≤ bpow ex)%R.

Theorem exp_small_round_0 :
  ∀ rnd {Hr : Valid_rnd rnd} x ex,
  (bpow (ex - 1) ≤ Rabs x < bpow ex)%R →
   round rnd x = 0%R → (ex ≤ fexp ex)%Z .

Section monotone_abs.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem abs_round_ge_generic :
  ∀ x y, generic_format x → (x ≤ Rabs y)%R → (x ≤ Rabs (round rnd y))%R.

Theorem abs_round_le_generic :
  ∀ x y, generic_format y → (Rabs x ≤ y)%R → (Rabs (round rnd x) ≤ y)%R.

End monotone_abs.

Theorem round_DN_opp :
  ∀ x,
  round Zfloor (-x) = (- round Zceil x)%R.

Theorem round_UP_opp :
  ∀ x,
  round Zceil (-x) = (- round Zfloor x)%R.

Theorem round_ZR_opp :
  ∀ x,
  round Ztrunc (- x) = Ropp (round Ztrunc x).

Theorem round_ZR_abs :
  ∀ x,
  round Ztrunc (Rabs x) = Rabs (round Ztrunc x).

Theorem round_AW_opp :
  ∀ x,
  round Zaway (- x) = Ropp (round Zaway x).

Theorem round_AW_abs :
  ∀ x,
  round Zaway (Rabs x) = Rabs (round Zaway x).

Theorem round_ZR_DN :
  ∀ x,
  (0 ≤ x)%R →
  round Ztrunc x = round Zfloor x.

Theorem round_ZR_UP :
  ∀ x,
  (x ≤ 0)%R →
  round Ztrunc x = round Zceil x.

Theorem round_AW_UP :
  ∀ x,
  (0 ≤ x)%R →
  round Zaway x = round Zceil x.

Theorem round_AW_DN :
  ∀ x,
  (x ≤ 0)%R →
  round Zaway x = round Zfloor x.

Theorem generic_format_round :
  ∀ rnd { Hr : Valid_rnd rnd } x,
  generic_format (round rnd x).

Theorem round_DN_pt :
  ∀ x,
  Rnd_DN_pt generic_format x (round Zfloor x).

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.

Theorem round_UP_pt :
  ∀ x,
  Rnd_UP_pt generic_format x (round Zceil x).

Theorem round_ZR_pt :
  ∀ x,
  Rnd_ZR_pt generic_format x (round Ztrunc x).

Lemma round_DN_small_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  round Zfloor x = 0%R.

Theorem round_DN_UP_lt :
  ∀ x, ¬ generic_format x →
  (round Zfloor x < x < round Zceil x)%R.

Lemma round_UP_small_pos :
  ∀ x ex,
  (bpow (ex - 1) ≤ x < bpow ex)%R →
  (ex ≤ fexp ex)%Z →
  round Zceil x = (bpow (fexp ex)).

Theorem generic_format_EM :
  ∀ x,
  generic_format x ∨ ¬generic_format x.

Section round_large.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Lemma round_large_pos_ge_bpow :
  ∀ x e,
  (0 < round rnd x)%R →
  (bpow e ≤ x)%R →
  (bpow e ≤ round rnd x)%R.

End round_large.

Theorem mag_round_ZR :
  ∀ x,
  (round Ztrunc x ≠ 0)%R →
  (mag beta (round Ztrunc x) = mag beta x :> Z).

Theorem mag_round :
  ∀ rnd {Hrnd : Valid_rnd rnd} x,
  (round rnd x ≠ 0)%R →
  (mag beta (round rnd x) = mag beta x :> Z) ∨
  Rabs (round rnd x) = bpow (Z.max (mag beta x) (fexp (mag beta x))).

Theorem mag_DN :
  ∀ x,
  (0 < round Zfloor x)%R →
  (mag beta (round Zfloor x) = mag beta x :> Z).

Theorem cexp_DN :
  ∀ x,
  (0 < round Zfloor x)%R →
  cexp (round Zfloor x) = cexp x.

Theorem scaled_mantissa_DN :
  ∀ x,
  (0 < round Zfloor x)%R →
  scaled_mantissa (round Zfloor x) = IZR (Zfloor (scaled_mantissa x)).

Theorem generic_N_pt_DN_or_UP :
  ∀ x f,
  Rnd_N_pt generic_format x f →
  f = round Zfloor x ∨ f = round Zceil x.

Section not_FTZ.

Class Exp_not_FTZ :=
  exp_not_FTZ : ∀ e, (fexp (fexp e + 1) ≤ fexp e)%Z.

Context { exp_not_FTZ_ : Exp_not_FTZ }.

Theorem subnormal_exponent :
  ∀ e x,
  (e ≤ fexp e)%Z →
  generic_format x →
  x = F2R (Float beta (Ztrunc (x × bpow (- fexp e))) (fexp e)).

End not_FTZ.

Section monotone_exp.

Class Monotone_exp :=
  monotone_exp : ∀ ex ey, (ex ≤ ey)%Z → (fexp ex ≤ fexp ey)%Z.

Context { monotone_exp_ : Monotone_exp }.

Global Instance monotone_exp_not_FTZ : Exp_not_FTZ.

Lemma cexp_le_bpow :
  ∀ (x : R) (e : Z),
  x ≠ 0%R →
  (Rabs x < bpow e)%R →
  (cexp x ≤ fexp e)%Z.

Lemma cexp_ge_bpow :
  ∀ (x : R) (e : Z),
  (bpow (e - 1) ≤ Rabs x)%R →
  (fexp e ≤ cexp x)%Z.

Lemma lt_cexp_pos :
  ∀ x y,
  (0 < y)%R →
  (cexp x < cexp y)%Z →
  (x < y)%R.

Theorem lt_cexp :
  ∀ x y,
  (y ≠ 0)%R →
  (cexp x < cexp y)%Z →
  (Rabs x < Rabs y)%R.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem mag_round_ge :
  ∀ x,
  round rnd x ≠ 0%R →
  (mag beta x ≤ mag beta (round rnd x))%Z.

Theorem cexp_round_ge :
  ∀ x,
  round rnd x ≠ 0%R →
  (cexp x ≤ cexp (round rnd x))%Z.

End monotone_exp.

Section Znearest.

Variable choice : Z → bool.

Definition Znearest x :=
  match Rcompare (x - IZR (Zfloor x)) (/2) with
  | Lt ⇒ Zfloor x
  | Eq ⇒ if choice (Zfloor x) then Zceil x else Zfloor x
  | Gt ⇒ Zceil x
  end.

Theorem Znearest_DN_or_UP :
  ∀ x,
  Znearest x = Zfloor x ∨ Znearest x = Zceil x.

Theorem Znearest_ge_floor :
  ∀ x,
  (Zfloor x ≤ Znearest x)%Z.

Theorem Znearest_le_ceil :
  ∀ x,
  (Znearest x ≤ Zceil x)%Z.

Global Instance valid_rnd_N : Valid_rnd Znearest.

Theorem Znearest_N_strict :
  ∀ x,
  (x - IZR (Zfloor x) ≠ /2)%R →
  (Rabs (x - IZR (Znearest x)) < /2)%R.

Theorem Znearest_half :
  ∀ x,
  (Rabs (x - IZR (Znearest x)) ≤ /2)%R.

Theorem Znearest_imp :
  ∀ x n,
  (Rabs (x - IZR n) < /2)%R →
  Znearest x = n.

Theorem round_N_pt :
  ∀ x,
  Rnd_N_pt generic_format x (round Znearest x).

Theorem round_N_middle :
  ∀ x,
  (x - round Zfloor x = round Zceil x - x)%R →
  round Znearest x = if choice (Zfloor (scaled_mantissa x)) then round Zceil x else round Zfloor x.

Lemma round_N_small_pos :
  ∀ x,
  ∀ ex,
  (Raux.bpow beta (ex - 1) ≤ x < Raux.bpow beta ex)%R →
  (ex < fexp ex)%Z →
  (round Znearest x = 0)%R.

End Znearest.

Section rndNA.

Global Instance valid_rnd_NA : Valid_rnd (Znearest (Zle_bool 0)) := valid_rnd_N _.

Theorem round_NA_pt :
  ∀ x,
  Rnd_NA_pt generic_format x (round (Znearest (Zle_bool 0)) x).

End rndNA.

Notation Znearest0 := (Znearest (fun x ⇒ (Zlt_bool x 0))).

Section rndN0.

Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _.

Theorem round_N0_pt :
  ∀ x,
  Rnd_N0_pt generic_format x (round Znearest0 x).

End rndN0.

Section rndN_opp.

Theorem Znearest_opp :
  ∀ choice x,
  Znearest choice (- x) = (- Znearest (fun t ⇒ negb (choice (- (t + 1))%Z)) x)%Z.

Theorem round_N_opp :
  ∀ choice,
  ∀ x,
  round (Znearest choice) (-x) = (- round (Znearest (fun t ⇒ negb (choice (- (t + 1))%Z))) x)%R.

Lemma round_N0_opp :
  ∀ x,
  (round Znearest0 (- x) = - round Znearest0 x)%R.

End rndN_opp.

Lemma round_N_small :
  ∀ choice,
  ∀ x,
  ∀ ex,
  (Raux.bpow beta (ex - 1) ≤ Rabs x < Raux.bpow beta ex)%R →
  (ex < fexp ex)%Z →
  (round (Znearest choice) x = 0)%R.

End Format.

Section Inclusion.

Variables fexp1 fexp2 : Z → Z.

Context { valid_exp1 : Valid_exp fexp1 }.
Context { valid_exp2 : Valid_exp fexp2 }.

Theorem generic_inclusion_mag :
  ∀ x,
  ( x ≠ 0%R → (fexp2 (mag beta x) ≤ fexp1 (mag beta x))%Z ) →
  generic_format fexp1 x →
  generic_format fexp2 x.

Theorem generic_inclusion_lt_ge :
  ∀ e1 e2,
  ( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
  ∀ x,
  (bpow e1 ≤ Rabs x < bpow e2)%R →
  generic_format fexp1 x →
  generic_format fexp2 x.

Theorem generic_inclusion :
  ∀ e,
  (fexp2 e ≤ fexp1 e)%Z →
  ∀ x,
  (bpow (e - 1) ≤ Rabs x ≤ bpow e)%R →
  generic_format fexp1 x →
  generic_format fexp2 x.

Theorem generic_inclusion_le_ge :
  ∀ e1 e2,
  (e1 < e2)%Z →
  ( ∀ e, (e1 < e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
  ∀ x,
  (bpow e1 ≤ Rabs x ≤ bpow e2)%R →
  generic_format fexp1 x →
  generic_format fexp2 x.

Theorem generic_inclusion_le :
  ∀ e2,
  ( ∀ e, (e ≤ e2)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
  ∀ x,
  (Rabs x ≤ bpow e2)%R →
  generic_format fexp1 x →
  generic_format fexp2 x.

Theorem generic_inclusion_ge :
  ∀ e1,
  ( ∀ e, (e1 < e)%Z → (fexp2 e ≤ fexp1 e)%Z ) →
  ∀ x,
  (bpow e1 ≤ Rabs x)%R →
  generic_format fexp1 x →
  generic_format fexp2 x.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem generic_round_generic :
  ∀ x,
  generic_format fexp1 x →
  generic_format fexp1 (round fexp2 rnd x).

End Inclusion.

End Generic.

Notation ZnearestA := (Znearest (Zle_bool 0)).

Section rndNA_opp.

Lemma round_NA_opp :
  ∀ beta : radix,
  ∀ (fexp : Z → Z),
  ∀ x,
  (round beta fexp ZnearestA (- x) = - round beta fexp ZnearestA x)%R.

End rndNA_opp.

Notation rndDN := Zfloor (only parsing).
Notation rndUP := Zceil (only parsing).
Notation rndZR := Ztrunc (only parsing).
Notation rndNA := ZnearestA (only parsing).