Module Fcore_FLT


Floating-point format with gradual underflow

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_FLX.
Require Import Fcore_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.

Section RND_FLT.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.

Definition FLT_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.

Definition FLT_exp e := Zmax (e - prec) emin.

Properties of the FLT format
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
Proof.

Theorem generic_format_FLT :
  forall x, FLT_format x -> generic_format beta FLT_exp x.
Proof.

Theorem FLT_format_generic :
  forall x, generic_format beta FLT_exp x -> FLT_format x.
Proof.


Theorem FLT_format_bpow :
  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
Proof.




Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.

Theorem canonic_exp_FLT_FLX :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
Proof.

Links between FLT and FLX
Theorem generic_format_FLT_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  generic_format beta (FLX_exp prec) x ->
  generic_format beta FLT_exp x.
Proof.

Theorem generic_format_FLX_FLT :
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.

Theorem round_FLT_FLX : forall rnd x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
intros rnd x Hx.
unfold round, scaled_mantissa.
rewrite canonic_exp_FLT_FLX ; trivial.
Qed.

Links between FLT and FIX (underflow)
Theorem canonic_exp_FLT_FIX :
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
  canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
Proof.

Theorem generic_format_FIX_FLT :
  forall x : R,
  generic_format beta FLT_exp x ->
  generic_format beta (FIX_exp emin) x.
Proof.

Theorem generic_format_FLT_FIX :
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
  generic_format beta (FIX_exp emin) x ->
  generic_format beta FLT_exp x.
Proof with

Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
    ulp beta FLT_exp x = bpow emin.
Proof with

Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
  (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
Proof.


Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Proof.



FLT is a nice format: it has a monotone exponent...
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
Proof.

and it allows a rounding to nearest, ties to even.
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.

Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
Proof.

End RND_FLT.