Helper function for computing the rounded value of a real number.
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.
Section Fcalc_round.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Section Fcalc_round_fexp.
Variable fexp :
Z ->
Z.
Context {
valid_exp :
Valid_exp fexp }.
Notation format := (
generic_format beta fexp).
Relates location and rounding.
Theorem inbetween_float_round :
forall rnd choice,
(
forall x m l,
inbetween_int m x l ->
rnd x =
choice m l ) ->
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rnd x =
F2R (
Float beta (
choice m l)
e).
Proof.
Definition cond_incr (
b :
bool)
m :=
if b then (
m + 1)%
Z else m.
Theorem inbetween_float_round_sign :
forall rnd choice,
(
forall x m l,
inbetween_int m (
Rabs x)
l ->
rnd x =
cond_Zopp (
Rlt_bool x 0) (
choice (
Rlt_bool x 0)
m l) ) ->
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e (
Rabs x)
l ->
round beta fexp rnd x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
choice (
Rlt_bool x 0)
m l))
e).
Proof.
Relates location and rounding down.
Theorem inbetween_int_DN :
forall x m l,
inbetween_int m x l ->
Zfloor x =
m.
Proof.
Theorem inbetween_float_DN :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Zfloor x =
F2R (
Float beta m e).
Proof.
Definition round_sign_DN s l :=
match l with
|
loc_Exact =>
false
|
_ =>
s
end.
Theorem inbetween_int_DN_sign :
forall x m l,
inbetween_int m (
Rabs x)
l ->
Zfloor x =
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_sign_DN (
Rlt_bool x 0)
l)
m).
Proof.
Theorem inbetween_float_DN_sign :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e (
Rabs x)
l ->
round beta fexp Zfloor x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_sign_DN (
Rlt_bool x 0)
l)
m))
e).
Proof.
Relates location and rounding up.
Definition round_UP l :=
match l with
|
loc_Exact =>
false
|
_ =>
true
end.
Theorem inbetween_int_UP :
forall x m l,
inbetween_int m x l ->
Zceil x =
cond_incr (
round_UP l)
m.
Proof.
Theorem inbetween_float_UP :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Zceil x =
F2R (
Float beta (
cond_incr (
round_UP l)
m)
e).
Proof.
Definition round_sign_UP s l :=
match l with
|
loc_Exact =>
false
|
_ =>
negb s
end.
Theorem inbetween_int_UP_sign :
forall x m l,
inbetween_int m (
Rabs x)
l ->
Zceil x =
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_sign_UP (
Rlt_bool x 0)
l)
m).
Proof.
Theorem inbetween_float_UP_sign :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e (
Rabs x)
l ->
round beta fexp Zceil x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_sign_UP (
Rlt_bool x 0)
l)
m))
e).
Proof.
Relates location and rounding toward zero.
Definition round_ZR (
s :
bool)
l :=
match l with
|
loc_Exact =>
false
|
_ =>
s
end.
Theorem inbetween_int_ZR :
forall x m l,
inbetween_int m x l ->
Ztrunc x =
cond_incr (
round_ZR (
Zlt_bool m 0)
l)
m.
Proof with
Theorem inbetween_float_ZR :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp Ztrunc x =
F2R (
Float beta (
cond_incr (
round_ZR (
Zlt_bool m 0)
l)
m)
e).
Proof.
Theorem inbetween_int_ZR_sign :
forall x m l,
inbetween_int m (
Rabs x)
l ->
Ztrunc x =
cond_Zopp (
Rlt_bool x 0)
m.
Proof.
Theorem inbetween_float_ZR_sign :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e (
Rabs x)
l ->
round beta fexp Ztrunc x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0)
m)
e).
Proof.
Relates location and rounding to nearest.
Definition round_N (
p :
bool)
l :=
match l with
|
loc_Exact =>
false
|
loc_Inexact Lt =>
false
|
loc_Inexact Eq =>
p
|
loc_Inexact Gt =>
true
end.
Theorem inbetween_int_N :
forall choice x m l,
inbetween_int m x l ->
Znearest choice x =
cond_incr (
round_N (
choice m)
l)
m.
Proof with
Theorem inbetween_int_N_sign :
forall choice x m l,
inbetween_int m (
Rabs x)
l ->
Znearest choice x =
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_N (
if Rlt_bool x 0
then negb (
choice (-(
m + 1))%
Z)
else choice m)
l)
m).
Proof with
Relates location and rounding to nearest even.
Theorem inbetween_int_NE :
forall x m l,
inbetween_int m x l ->
ZnearestE x =
cond_incr (
round_N (
negb (
Zeven m))
l)
m.
Proof.
Theorem inbetween_float_NE :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp ZnearestE x =
F2R (
Float beta (
cond_incr (
round_N (
negb (
Zeven m))
l)
m)
e).
Proof.
Theorem inbetween_int_NE_sign :
forall x m l,
inbetween_int m (
Rabs x)
l ->
ZnearestE x =
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_N (
negb (
Zeven m))
l)
m).
Proof.
Theorem inbetween_float_NE_sign :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e (
Rabs x)
l ->
round beta fexp ZnearestE x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_N (
negb (
Zeven m))
l)
m))
e).
Proof.
Relates location and rounding to nearest away.
Theorem inbetween_int_NA :
forall x m l,
inbetween_int m x l ->
ZnearestA x =
cond_incr (
round_N (
Zle_bool 0
m)
l)
m.
Proof.
Theorem inbetween_float_NA :
forall x m l,
let e :=
canonic_exp beta fexp x in
inbetween_float beta m e x l ->
round beta fexp ZnearestA x =
F2R (
Float beta (
cond_incr (
round_N (
Zle_bool 0
m)
l)
m)
e).
Proof.
Theorem inbetween_int_NA_sign :
forall x m l,
inbetween_int m (
Rabs x)
l ->
ZnearestA x =
cond_Zopp (
Rlt_bool x 0) (
cond_incr (
round_N true l)
m).
Proof.
Definition truncate_aux t k :=
let '(
m,
e,
l) :=
t in
let p :=
Zpower beta k in
(
Zdiv m p, (
e +
k)%
Z,
new_location p (
Zmod m p)
l).
Theorem truncate_aux_comp :
forall t k1 k2,
(0 <
k1)%
Z ->
(0 <
k2)%
Z ->
truncate_aux t (
k1 +
k2) =
truncate_aux (
truncate_aux t k1)
k2.
Proof.
Given a triple (mantissa, exponent, position), this function
computes a triple with a canonic exponent, assuming the
original triple had enough precision.
Definition truncate t :=
let '(
m,
e,
l) :=
t in
let k := (
fexp (
Zdigits beta m +
e) -
e)%
Z in
if Zlt_bool 0
k then truncate_aux t k
else t.
Theorem truncate_0 :
forall e l,
let '(
m',
e',
l') :=
truncate (0,
e,
l)%
Z in
m' =
Z0.
Proof.
Theorem generic_format_truncate :
forall m e l,
(0 <=
m)%
Z ->
let '(
m',
e',
l') :=
truncate (
m,
e,
l)
in
format (
F2R (
Float beta m'
e')).
Proof.
Theorem truncate_correct_format :
forall m e,
m <>
Z0 ->
let x :=
F2R (
Float beta m e)
in
generic_format beta fexp x ->
(
e <=
fexp (
Zdigits beta m +
e))%
Z ->
let '(
m',
e',
l') :=
truncate (
m,
e,
loc_Exact)
in
x =
F2R (
Float beta m'
e') /\
e' =
canonic_exp beta fexp x.
Proof.
Theorem truncate_correct_partial :
forall x m e l,
(0 <
x)%
R ->
inbetween_float beta m e x l ->
(
e <=
fexp (
Zdigits beta m +
e))%
Z ->
let '(
m',
e',
l') :=
truncate (
m,
e,
l)
in
inbetween_float beta m'
e'
x l' /\
e' =
canonic_exp beta fexp x.
Proof.
Theorem truncate_correct :
forall x m e l,
(0 <=
x)%
R ->
inbetween_float beta m e x l ->
(
e <=
fexp (
Zdigits beta m +
e))%
Z \/
l =
loc_Exact ->
let '(
m',
e',
l') :=
truncate (
m,
e,
l)
in
inbetween_float beta m'
e'
x l' /\
(
e' =
canonic_exp beta fexp x \/ (
l' =
loc_Exact /\
format x)).
Proof.
intros x m e l [
Hx|
Hx]
H1 H2.
0 < x *)
destruct (
Zle_or_lt e (
fexp (
Zdigits beta m +
e)))
as [
H3|
H3].
. enough digits *)
generalize (
truncate_correct_partial x m e l Hx H1 H3).
destruct (
truncate (
m,
e,
l))
as ((
m',
e'),
l').
intros (
H4,
H5).
split.
exact H4.
now left.
. not enough digits but loc_Exact *)
destruct H2 as [
H2|
H2].
elim (
Zlt_irrefl e).
now apply Zle_lt_trans with (1 :=
H2).
rewrite H2 in H1 |- *.
unfold truncate.
generalize (
Zlt_cases 0 (
fexp (
Zdigits beta m +
e) -
e)).
case Zlt_bool.
intros H.
apply False_ind.
omega.
intros _.
split.
exact H1.
right.
split.
apply refl_equal.
inversion_clear H1.
rewrite H.
apply generic_format_F2R.
intros Zm.
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits with (1 :=
Zm).
now apply Zlt_le_weak.
x = 0 *)
assert (
Hm:
m =
Z0).
cut (
m <= 0 <
m + 1)%
Z.
omega.
assert (
Hx': (
F2R (
Float beta m e) <=
x <
F2R (
Float beta (
m + 1)
e))%
R).
apply inbetween_float_bounds with (1 :=
H1).
rewrite <-
Hx in Hx'.
split.
apply F2R_le_0_reg with (1 :=
proj1 Hx').
apply F2R_gt_0_reg with (1 :=
proj2 Hx').
rewrite Hm, <-
Hx in H1 |- *.
clear -
H1.
case H1.
. *)
intros _.
assert (
exists e',
truncate (
Z0,
e,
loc_Exact) = (
Z0,
e',
loc_Exact)).
unfold truncate,
truncate_aux.
case Zlt_bool.
rewrite Zdiv_0_l,
Zmod_0_l.
eexists.
apply f_equal.
unfold new_location.
now case Zeven.
now eexists.
destruct H as (
e',
H).
rewrite H.
split.
constructor.
apply sym_eq.
apply F2R_0.
right.
repeat split.
apply generic_format_0.
. *)
intros l' (
H,
_)
_.
rewrite F2R_0 in H.
elim Rlt_irrefl with (1 :=
H).
Qed.
Section round_dir.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Variable choice :
Z ->
location ->
Z.
Hypothesis inbetween_int_valid :
forall x m l,
inbetween_int m x l ->
rnd x =
choice m l.
Theorem round_any_correct :
forall x m e l,
inbetween_float beta m e x l ->
(
e =
canonic_exp beta fexp x \/ (
l =
loc_Exact /\
format x)) ->
round beta fexp rnd x =
F2R (
Float beta (
choice m l)
e).
Proof with
Truncating a triple is sufficient to round a real number.
Theorem round_trunc_any_correct :
forall x m e l,
(0 <=
x)%
R ->
inbetween_float beta m e x l ->
(
e <=
fexp (
Zdigits beta m +
e))%
Z \/
l =
loc_Exact ->
round beta fexp rnd x =
let '(
m',
e',
l') :=
truncate (
m,
e,
l)
in F2R (
Float beta (
choice m'
l')
e').
Proof.
End round_dir.
Section round_dir_sign.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Variable choice :
bool ->
Z ->
location ->
Z.
Hypothesis inbetween_int_valid :
forall x m l,
inbetween_int m (
Rabs x)
l ->
rnd x =
cond_Zopp (
Rlt_bool x 0) (
choice (
Rlt_bool x 0)
m l).
Theorem round_sign_any_correct :
forall x m e l,
inbetween_float beta m e (
Rabs x)
l ->
(
e =
canonic_exp beta fexp x \/ (
l =
loc_Exact /\
format x)) ->
round beta fexp rnd x =
F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
choice (
Rlt_bool x 0)
m l))
e).
Proof with
Truncating a triple is sufficient to round a real number.
Theorem round_trunc_sign_any_correct :
forall x m e l,
inbetween_float beta m e (
Rabs x)
l ->
(
e <=
fexp (
Zdigits beta m +
e))%
Z \/
l =
loc_Exact ->
round beta fexp rnd x =
let '(
m',
e',
l') :=
truncate (
m,
e,
l)
in F2R (
Float beta (
cond_Zopp (
Rlt_bool x 0) (
choice (
Rlt_bool x 0)
m'
l'))
e').
Proof.
End round_dir_sign.
Instances of the theorems above, for the usual rounding modes.
Definition round_DN_correct :=
round_any_correct _ (
fun m _ =>
m)
inbetween_int_DN.
Definition round_trunc_DN_correct :=
round_trunc_any_correct _ (
fun m _ =>
m)
inbetween_int_DN.
Definition round_sign_DN_correct :=
round_sign_any_correct _ (
fun s m l =>
cond_incr (
round_sign_DN s l)
m)
inbetween_int_DN_sign.
Definition round_trunc_sign_DN_correct :=
round_trunc_sign_any_correct _ (
fun s m l =>
cond_incr (
round_sign_DN s l)
m)
inbetween_int_DN_sign.
Definition round_UP_correct :=
round_any_correct _ (
fun m l =>
cond_incr (
round_UP l)
m)
inbetween_int_UP.
Definition round_trunc_UP_correct :=
round_trunc_any_correct _ (
fun m l =>
cond_incr (
round_UP l)
m)
inbetween_int_UP.
Definition round_sign_UP_correct :=
round_sign_any_correct _ (
fun s m l =>
cond_incr (
round_sign_UP s l)
m)
inbetween_int_UP_sign.
Definition round_trunc_sign_UP_correct :=
round_trunc_sign_any_correct _ (
fun s m l =>
cond_incr (
round_sign_UP s l)
m)
inbetween_int_UP_sign.
Definition round_ZR_correct :=
round_any_correct _ (
fun m l =>
cond_incr (
round_ZR (
Zlt_bool m 0)
l)
m)
inbetween_int_ZR.
Definition round_trunc_ZR_correct :=
round_trunc_any_correct _ (
fun m l =>
cond_incr (
round_ZR (
Zlt_bool m 0)
l)
m)
inbetween_int_ZR.
Definition round_sign_ZR_correct :=
round_sign_any_correct _ (
fun s m l =>
m)
inbetween_int_ZR_sign.
Definition round_trunc_sign_ZR_correct :=
round_trunc_sign_any_correct _ (
fun s m l =>
m)
inbetween_int_ZR_sign.
Definition round_NE_correct :=
round_any_correct _ (
fun m l =>
cond_incr (
round_N (
negb (
Zeven m))
l)
m)
inbetween_int_NE.
Definition round_trunc_NE_correct :=
round_trunc_any_correct _ (
fun m l =>
cond_incr (
round_N (
negb (
Zeven m))
l)
m)
inbetween_int_NE.
Definition round_sign_NE_correct :=
round_sign_any_correct _ (
fun s m l =>
cond_incr (
round_N (
negb (
Zeven m))
l)
m)
inbetween_int_NE_sign.
Definition round_trunc_sign_NE_correct :=
round_trunc_sign_any_correct _ (
fun s m l =>
cond_incr (
round_N (
negb (
Zeven m))
l)
m)
inbetween_int_NE_sign.
Definition round_NA_correct :=
round_any_correct _ (
fun m l =>
cond_incr (
round_N (
Zle_bool 0
m)
l)
m)
inbetween_int_NA.
Definition round_trunc_NA_correct :=
round_trunc_any_correct _ (
fun m l =>
cond_incr (
round_N (
Zle_bool 0
m)
l)
m)
inbetween_int_NA.
Definition round_sign_NA_correct :=
round_sign_any_correct _ (
fun s m l =>
cond_incr (
round_N true l)
m)
inbetween_int_NA_sign.
Definition round_trunc_sign_NA_correct :=
round_trunc_sign_any_correct _ (
fun s m l =>
cond_incr (
round_N true l)
m)
inbetween_int_NA_sign.
End Fcalc_round_fexp.
Specialization of truncate for FIX formats.
Variable emin :
Z.
Definition truncate_FIX t :=
let '(
m,
e,
l) :=
t in
let k := (
emin -
e)%
Z in
if Zlt_bool 0
k then
let p :=
Zpower beta k in
(
Zdiv m p, (
e +
k)%
Z,
new_location p (
Zmod m p)
l)
else t.
Theorem truncate_FIX_correct :
forall x m e l,
inbetween_float beta m e x l ->
(
e <=
emin)%
Z \/
l =
loc_Exact ->
let '(
m',
e',
l') :=
truncate_FIX (
m,
e,
l)
in
inbetween_float beta m'
e'
x l' /\
(
e' =
canonic_exp beta (
FIX_exp emin)
x \/ (
l' =
loc_Exact /\
generic_format beta (
FIX_exp emin)
x)).
Proof.
End Fcalc_round.