Module Fcore_FLT
Links between FLT and FIX (underflow)
Theorem canonic_exp_FLT_FIX :
forall x, x <> 0%R ->
(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.
intros ex ey.
unfold FLT_exp.
zify ;
omega.
Qed.
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.