Module Fcore_float_prop
Basic properties of floating-point formats: lemmas about mantissa, exponent...
Require Import Fcore_Raux.
Require Import Fcore_defs.
Section Float_prop.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Theorem Rcompare_F2R :
forall e m1 m2 :
Z,
Rcompare (
F2R (
Float beta m1 e)) (
F2R (
Float beta m2 e)) =
Zcompare m1 m2.
Proof.
Basic facts
Theorem F2R_le_reg :
forall e m1 m2 :
Z,
(
F2R (
Float beta m1 e) <=
F2R (
Float beta m2 e))%
R ->
(
m1 <=
m2)%
Z.
Proof.
Theorem F2R_le_compat :
forall m1 m2 e :
Z,
(
m1 <=
m2)%
Z ->
(
F2R (
Float beta m1 e) <=
F2R (
Float beta m2 e))%
R.
Proof.
Theorem F2R_lt_reg :
forall e m1 m2 :
Z,
(
F2R (
Float beta m1 e) <
F2R (
Float beta m2 e))%
R ->
(
m1 <
m2)%
Z.
Proof.
Theorem F2R_lt_compat :
forall e m1 m2 :
Z,
(
m1 <
m2)%
Z ->
(
F2R (
Float beta m1 e) <
F2R (
Float beta m2 e))%
R.
Proof.
Theorem F2R_eq_compat :
forall e m1 m2 :
Z,
(
m1 =
m2)%
Z ->
(
F2R (
Float beta m1 e) =
F2R (
Float beta m2 e))%
R.
Proof.
intros e m1 m2 H.
now apply (
f_equal (
fun m =>
F2R (
Float beta m e))).
Qed.
Theorem F2R_eq_reg :
forall e m1 m2 :
Z,
F2R (
Float beta m1 e) =
F2R (
Float beta m2 e) ->
m1 =
m2.
Proof.
Theorem F2R_Zabs:
forall m e :
Z,
F2R (
Float beta (
Zabs m)
e) =
Rabs (
F2R (
Float beta m e)).
Proof.
Theorem F2R_Zopp :
forall m e :
Z,
F2R (
Float beta (
Zopp m)
e) =
Ropp (
F2R (
Float beta m e)).
Proof.
Sign facts
Theorem F2R_0 :
forall e :
Z,
F2R (
Float beta 0
e) =
R0.
Proof.
Theorem F2R_eq_0_reg :
forall m e :
Z,
F2R (
Float beta m e) =
R0 ->
m =
Z0.
Proof.
Theorem F2R_ge_0_reg :
forall m e :
Z,
(0 <=
F2R (
Float beta m e))%
R ->
(0 <=
m)%
Z.
Proof.
Theorem F2R_le_0_reg :
forall m e :
Z,
(
F2R (
Float beta m e) <= 0)%
R ->
(
m <= 0)%
Z.
Proof.
Theorem F2R_gt_0_reg :
forall m e :
Z,
(0 <
F2R (
Float beta m e))%
R ->
(0 <
m)%
Z.
Proof.
Theorem F2R_lt_0_reg :
forall m e :
Z,
(
F2R (
Float beta m e) < 0)%
R ->
(
m < 0)%
Z.
Proof.
Theorem F2R_ge_0_compat :
forall f :
float beta,
(0 <=
Fnum f)%
Z ->
(0 <=
F2R f)%
R.
Proof.
Theorem F2R_le_0_compat :
forall f :
float beta,
(
Fnum f <= 0)%
Z ->
(
F2R f <= 0)%
R.
Proof.
Theorem F2R_gt_0_compat :
forall f :
float beta,
(0 <
Fnum f)%
Z ->
(0 <
F2R f)%
R.
Proof.
Theorem F2R_lt_0_compat :
forall f :
float beta,
(
Fnum f < 0)%
Z ->
(
F2R f < 0)%
R.
Proof.
Theorem F2R_neq_0_compat :
forall f :
float beta,
(
Fnum f <> 0)%
Z ->
(
F2R f <> 0)%
R.
Proof.
Lemma Fnum_ge_0_compat:
forall (
f :
float beta),
(0 <=
F2R f)%
R -> (0 <=
Fnum f)%
Z.
Proof.
Lemma Fnum_le_0_compat:
forall (
f :
float beta),
(
F2R f <= 0)%
R -> (
Fnum f <= 0)%
Z.
Proof.
Floats and bpow
Theorem F2R_bpow :
forall e :
Z,
F2R (
Float beta 1
e) =
bpow e.
Proof.
Theorem bpow_le_F2R :
forall m e :
Z,
(0 <
m)%
Z ->
(
bpow e <=
F2R (
Float beta m e))%
R.
Proof.
Theorem F2R_p1_le_bpow :
forall m e1 e2 :
Z,
(0 <
m)%
Z ->
(
F2R (
Float beta m e1) <
bpow e2)%
R ->
(
F2R (
Float beta (
m + 1)
e1) <=
bpow e2)%
R.
Proof.
Theorem bpow_le_F2R_m1 :
forall m e1 e2 :
Z,
(1 <
m)%
Z ->
(
bpow e2 <
F2R (
Float beta m e1))%
R ->
(
bpow e2 <=
F2R (
Float beta (
m - 1)
e1))%
R.
Proof.
Theorem F2R_lt_bpow :
forall f :
float beta,
forall e',
(
Zabs (
Fnum f) <
Zpower beta (
e' -
Fexp f))%
Z ->
(
Rabs (
F2R f) <
bpow e')%
R.
Proof.
Theorem F2R_change_exp :
forall e'
m e :
Z,
(
e' <=
e)%
Z ->
F2R (
Float beta m e) =
F2R (
Float beta (
m *
Zpower beta (
e -
e'))
e').
Proof.
Theorem F2R_prec_normalize :
forall m e e'
p :
Z,
(
Zabs m <
Zpower beta p)%
Z ->
(
bpow (
e' - 1)%
Z <=
Rabs (
F2R (
Float beta m e)))%
R ->
F2R (
Float beta m e) =
F2R (
Float beta (
m *
Zpower beta (
e -
e' +
p)) (
e' -
p)).
Proof.
Floats and ln_beta
Theorem ln_beta_F2R_bounds :
forall x m e, (0 <
m)%
Z ->
(
F2R (
Float beta m e) <=
x <
F2R (
Float beta (
m + 1)
e))%
R ->
ln_beta beta x =
ln_beta beta (
F2R (
Float beta m e)) :>
Z.
Proof.
Theorem ln_beta_F2R :
forall m e :
Z,
m <>
Z0 ->
(
ln_beta beta (
F2R (
Float beta m e)) =
ln_beta beta (
Z2R m) +
e :>
Z)%
Z.
Proof.
Theorem float_distribution_pos :
forall m1 e1 m2 e2 :
Z,
(0 <
m1)%
Z ->
(
F2R (
Float beta m1 e1) <
F2R (
Float beta m2 e2) <
F2R (
Float beta (
m1 + 1)
e1))%
R ->
(
e2 <
e1)%
Z /\ (
e1 +
ln_beta beta (
Z2R m1) =
e2 +
ln_beta beta (
Z2R m2))%
Z.
Proof.
Theorem F2R_cond_Zopp :
forall b m e,
F2R (
Float beta (
cond_Zopp b m)
e) =
cond_Ropp b (
F2R (
Float beta m e)).
Proof.
End Float_prop.