Floating-point format without 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_FIX.
Require Import Fcore_ulp.
Require Import Fcore_rnd_ne.
Section RND_FLX.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable prec :
Z.
Class Prec_gt_0 :=
prec_gt_0 : (0 <
prec)%
Z.
Context {
prec_gt_0_ :
Prec_gt_0 }.
Definition FLX_format (
x :
R) :=
exists f :
float beta,
x =
F2R f /\ (
Zabs (
Fnum f) <
Zpower beta prec)%
Z.
Definition FLX_exp (
e :
Z) := (
e -
prec)%
Z.
Properties of the FLX format
Global Instance FLX_exp_valid :
Valid_exp FLX_exp.
Proof.
intros k.
unfold FLX_exp.
generalize prec_gt_0.
repeat split ;
intros ;
omega.
Qed.
Theorem FIX_format_FLX :
forall x e,
(
bpow (
e - 1) <=
Rabs x <=
bpow e)%
R ->
FLX_format x ->
FIX_format beta (
e -
prec)
x.
Proof.
clear prec_gt_0_.
intros x e Hx ((
xm,
xe), (
H1,
H2)).
rewrite H1, (
F2R_prec_normalize beta xm xe e prec).
now eexists.
exact H2.
now rewrite <-
H1.
Qed.
Theorem FLX_format_generic :
forall x,
generic_format beta FLX_exp x ->
FLX_format x.
Proof.
Theorem generic_format_FLX :
forall x,
FLX_format x ->
generic_format beta FLX_exp x.
Proof.
Theorem FLX_format_satisfies_any :
satisfies_any FLX_format.
Proof.
Theorem FLX_format_FIX :
forall x e,
(
bpow (
e - 1) <=
Rabs x <=
bpow e)%
R ->
FIX_format beta (
e -
prec)
x ->
FLX_format x.
Proof with
unbounded floating-point format with normal mantissas
Definition FLXN_format (
x :
R) :=
exists f :
float beta,
x =
F2R f /\ (
x <>
R0 ->
Zpower beta (
prec - 1) <=
Zabs (
Fnum f) <
Zpower beta prec)%
Z.
Theorem generic_format_FLXN :
forall x,
FLXN_format x ->
generic_format beta FLX_exp x.
Proof.
Theorem FLXN_format_generic :
forall x,
generic_format beta FLX_exp x ->
FLXN_format x.
Proof.
Theorem FLXN_format_satisfies_any :
satisfies_any FLXN_format.
Proof.
Theorem ulp_FLX_0: (
ulp beta FLX_exp 0 = 0)%
R.
Proof.
Theorem ulp_FLX_le:
forall x, (
ulp beta FLX_exp x <=
Rabs x *
bpow (1-
prec))%
R.
Proof.
Theorem ulp_FLX_ge:
forall x, (
Rabs x *
bpow (-
prec) <=
ulp beta FLX_exp x)%
R.
Proof.
FLX is a nice format: it has a monotone exponent...
Global Instance FLX_exp_monotone :
Monotone_exp FLX_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_FLX :
Exists_NE beta FLX_exp.
Proof.
destruct NE_prop as [
H|
H].
now left.
right.
unfold FLX_exp.
split ;
omega.
Qed.
End RND_FLX.