Module Fcore_FIX
Fixed-point format
Require
Import
Fcore_Raux
.
Require
Import
Fcore_defs
.
Require
Import
Fcore_rnd
.
Require
Import
Fcore_generic_fmt
.
Require
Import
Fcore_rnd_ne
.
Section
RND_FIX
.
Variable
beta
:
radix
.
Notation
bpow
:= (
bpow
beta
).
Variable
emin
:
Z
.
Definition
FIX_format
(
x
:
R
) :=
exists
f
:
float
beta
,
x
=
F2R
f
/\ (
Fexp
f
=
emin
)%
Z
.
Definition
FIX_exp
(
e
:
Z
) :=
emin
.
Properties of the FIX format
Global
Instance
FIX_exp_valid
:
Valid_exp
FIX_exp
.
Proof.
intros
k
.
unfold
FIX_exp
.
split
;
intros
H
.
now
apply
Zlt_le_weak
.
split
.
apply
Zle_refl
.
now
intros
_
_
.
Qed.
Theorem
generic_format_FIX
:
forall
x
,
FIX_format
x
->
generic_format
beta
FIX_exp
x
.
Proof.
intros
x
((
xm
,
xe
), (
Hx1
,
Hx2
)).
rewrite
Hx1
.
now
apply
generic_format_canonic
.
Qed.
Theorem
FIX_format_generic
:
forall
x
,
generic_format
beta
FIX_exp
x
->
FIX_format
x
.
Proof.
intros
x
H
.
rewrite
H
.
eexists
;
repeat
split
.
Qed.
Theorem
FIX_format_satisfies_any
:
satisfies_any
FIX_format
.
Proof.
refine
(
satisfies_any_eq
_
_
_
(
generic_format_satisfies_any
beta
FIX_exp
)).
intros
x
.
split
.
apply
FIX_format_generic
.
apply
generic_format_FIX
.
Qed.
Global
Instance
FIX_exp_monotone
:
Monotone_exp
FIX_exp
.
Proof.
intros
ex
ey
H
.
apply
Zle_refl
.
Qed.
End
RND_FIX
.