Error of the rounded-to-nearest addition is representable.
Require Import Psatz.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_generic_fmt.
Require Import Fcore_FIX.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
Require Import Fcore_ulp.
Require Import Fcalc_ops.
Section Fprop_plus_error.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable fexp :
Z ->
Z.
Context {
valid_exp :
Valid_exp fexp }.
Section round_repr_same_exp.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Theorem round_repr_same_exp :
forall m e,
exists m',
round beta fexp rnd (
F2R (
Float beta m e)) =
F2R (
Float beta m'
e).
Proof with
End round_repr_same_exp.
Context {
monotone_exp :
Monotone_exp fexp }.
Notation format := (
generic_format beta fexp).
Variable choice :
Z ->
bool.
Lemma plus_error_aux :
forall x y,
(
canonic_exp beta fexp x <=
canonic_exp beta fexp y)%
Z ->
format x ->
format y ->
format (
round beta fexp (
Znearest choice) (
x +
y) - (
x +
y))%
R.
Proof.
Error of the addition
Theorem plus_error :
forall x y,
format x ->
format y ->
format (
round beta fexp (
Znearest choice) (
x +
y) - (
x +
y))%
R.
Proof.
End Fprop_plus_error.
Section Fprop_plus_zero.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable fexp :
Z ->
Z.
Context {
valid_exp :
Valid_exp fexp }.
Context {
exp_not_FTZ :
Exp_not_FTZ fexp }.
Notation format := (
generic_format beta fexp).
Section round_plus_eq_zero_aux.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Lemma round_plus_eq_zero_aux :
forall x y,
(
canonic_exp beta fexp x <=
canonic_exp beta fexp y)%
Z ->
format x ->
format y ->
(0 <=
x +
y)%
R ->
round beta fexp rnd (
x +
y) = 0%
R ->
(
x +
y = 0)%
R.
Proof with
End round_plus_eq_zero_aux.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format
Theorem round_plus_eq_zero :
forall x y,
format x ->
format y ->
round beta fexp rnd (
x +
y) = 0%
R ->
(
x +
y = 0)%
R.
Proof with
End Fprop_plus_zero.
Section Fprop_plus_FLT.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable emin prec :
Z.
Context {
prec_gt_0_ :
Prec_gt_0 prec }.
Theorem FLT_format_plus_small:
forall x y,
generic_format beta (
FLT_exp emin prec)
x ->
generic_format beta (
FLT_exp emin prec)
y ->
(
Rabs (
x+
y) <=
bpow (
prec+
emin))%
R ->
generic_format beta (
FLT_exp emin prec) (
x+
y).
Proof with
End Fprop_plus_FLT.
Section Fprop_plus_mult_ulp.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable fexp :
Z ->
Z.
Context {
valid_exp :
Valid_exp fexp }.
Context {
monotone_exp :
Monotone_exp fexp }.
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Notation format := (
generic_format beta fexp).
Notation cexp := (
canonic_exp beta fexp).
Lemma ex_shift :
forall x e,
format x -> (
e <=
cexp x)%
Z ->
exists m, (
x =
Z2R m *
bpow e)%
R.
Proof with
Lemma ln_beta_minus1 :
forall z,
z <> 0%
R ->
(
ln_beta beta z - 1)%
Z =
ln_beta beta (
z /
Z2R beta).
Proof.
Theorem round_plus_mult_ulp :
forall x y,
format x ->
format y -> (
x <> 0)%
R ->
exists m, (
round beta fexp rnd (
x+
y) =
Z2R m *
ulp beta fexp (
x/
Z2R beta))%
R.
Proof with
Context {
exp_not_FTZ :
Exp_not_FTZ fexp}.
Theorem round_plus_ge_ulp :
forall x y,
format x ->
format y ->
round beta fexp rnd (
x+
y) = 0%
R \/
(
ulp beta fexp (
x/
Z2R beta) <=
Rabs (
round beta fexp rnd (
x+
y)))%
R.
Proof with
End Fprop_plus_mult_ulp.
Section Fprop_plus_ge_ulp.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable rnd :
R ->
Z.
Context {
valid_rnd :
Valid_rnd rnd }.
Variable emin prec :
Z.
Context {
prec_gt_0_ :
Prec_gt_0 prec }.
Theorem round_plus_ge_ulp_FLT :
forall x y e,
generic_format beta (
FLT_exp emin prec)
x ->
generic_format beta (
FLT_exp emin prec)
y ->
(
bpow e <=
Rabs x)%
R ->
round beta (
FLT_exp emin prec)
rnd (
x+
y) = 0%
R \/
(
bpow (
e -
prec) <=
Rabs (
round beta (
FLT_exp emin prec)
rnd (
x+
y)))%
R.
Proof with
Theorem round_plus_ge_ulp_FLX :
forall x y e,
generic_format beta (
FLX_exp prec)
x ->
generic_format beta (
FLX_exp prec)
y ->
(
bpow e <=
Rabs x)%
R ->
round beta (
FLX_exp prec)
rnd (
x+
y) = 0%
R \/
(
bpow (
e -
prec) <=
Rabs (
round beta (
FLX_exp prec)
rnd (
x+
y)))%
R.
Proof with
End Fprop_plus_ge_ulp.