Unit in the Last Place: our definition using fexp and its properties, successor and predecessor
Require Import Reals Psatz.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Section Fcore_ulp.
Variable beta :
radix.
Notation bpow e := (
bpow beta e).
Variable fexp :
Z ->
Z.
Definition and basic properties about the minimal exponent, when it exists
Lemma Z_le_dec_aux:
forall x y :
Z, (
x <=
y)%
Z \/ ~ (
x <=
y)%
Z.
Proof.
intros.
destruct (
Z_le_dec x y).
now left.
now right.
Qed.
negligible_exp is either none (as in FLX) or Some n such that n <= fexp n.
Definition negligible_exp:
option Z :=
match (
LPO_Z _ (
fun z =>
Z_le_dec_aux z (
fexp z)))
with
|
inleft N =>
Some (
proj1_sig N)
|
inright _ =>
None
end.
Inductive negligible_exp_prop:
option Z ->
Prop :=
|
negligible_None: (
forall n, (
fexp n <
n)%
Z) ->
negligible_exp_prop None
|
negligible_Some:
forall n, (
n <=
fexp n)%
Z ->
negligible_exp_prop (
Some n).
Lemma negligible_exp_spec:
negligible_exp_prop negligible_exp.
Proof.
Lemma negligible_exp_spec': (
negligible_exp =
None /\
forall n, (
fexp n <
n)%
Z)
\/
exists n, (
negligible_exp =
Some n /\ (
n <=
fexp n)%
Z).
Proof.
unfold negligible_exp;
destruct LPO_Z as [(
n,
Hn)|
Hn].
right;
simpl;
exists n;
now split.
left;
split;
trivial.
intros n;
specialize (
Hn n);
omega.
Qed.
Context {
valid_exp :
Valid_exp fexp }.
Lemma fexp_negligible_exp_eq:
forall n m, (
n <=
fexp n)%
Z -> (
m <=
fexp m)%
Z ->
fexp n =
fexp m.
Proof.
Definition and basic properties about the ulp
Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal
exponent, such as in FLX, and beta^(fexp n) when there is a n such
that n <= fexp n. For instance, the value of ulp(O) is then
beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
is equivalent to the previous "unfold ulp" provided the value is
not zero.
Definition ulp x :=
match Req_bool x 0
with
|
true =>
match negligible_exp with
|
Some n =>
bpow (
fexp n)
|
None => 0%
R
end
|
false =>
bpow (
canonic_exp beta fexp x)
end.
Lemma ulp_neq_0 :
forall x:
R, (
x <> 0)%
R ->
ulp x =
bpow (
canonic_exp beta fexp x).
Proof.
intros x Hx.
unfold ulp;
case (
Req_bool_spec x);
trivial.
intros H;
now contradict H.
Qed.
Notation F := (
generic_format beta fexp).
Theorem ulp_opp :
forall x,
ulp (-
x) =
ulp x.
Proof.
Theorem ulp_abs :
forall x,
ulp (
Rabs x) =
ulp x.
Proof.
Theorem ulp_ge_0:
forall x, (0 <=
ulp x)%
R.
Proof.
Theorem ulp_le_id:
forall x,
(0 <
x)%
R ->
F x ->
(
ulp x <=
x)%
R.
Proof.
Theorem ulp_le_abs:
forall x,
(
x <> 0)%
R ->
F x ->
(
ulp x <=
Rabs x)%
R.
Proof.
Theorem round_UP_DN_ulp :
forall x, ~
F x ->
round beta fexp Zceil x = (
round beta fexp Zfloor x +
ulp x)%
R.
Proof.
Theorem ulp_bpow :
forall e,
ulp (
bpow e) =
bpow (
fexp (
e + 1)).
Proof.
Lemma generic_format_ulp_0:
F (
ulp 0).
Proof.
Lemma generic_format_bpow_ge_ulp_0:
forall e,
(
ulp 0 <=
bpow e)%
R ->
F (
bpow e).
Proof.
The three following properties are equivalent:
Exp_not_FTZ ; forall x, F (ulp x) ; forall x, ulp 0 <= ulp x
Lemma generic_format_ulp:
Exp_not_FTZ fexp ->
forall x,
F (
ulp x).
Proof.
Lemma not_FTZ_generic_format_ulp:
(
forall x,
F (
ulp x)) ->
Exp_not_FTZ fexp.
Proof.
Lemma ulp_ge_ulp_0:
Exp_not_FTZ fexp ->
forall x, (
ulp 0 <=
ulp x)%
R.
Proof.
Lemma not_FTZ_ulp_ge_ulp_0:
(
forall x, (
ulp 0 <=
ulp x)%
R) ->
Exp_not_FTZ fexp.
Proof.
Theorem ulp_le_pos :
forall {
Hm :
Monotone_exp fexp },
forall x y:
R,
(0 <=
x)%
R -> (
x <=
y)%
R ->
(
ulp x <=
ulp y)%
R.
Proof with
Theorem ulp_le :
forall {
Hm :
Monotone_exp fexp },
forall x y:
R,
(
Rabs x <=
Rabs y)%
R ->
(
ulp x <=
ulp y)%
R.
Proof.
Definition and properties of pred and succ
Definition pred_pos x :=
if Req_bool x (
bpow (
ln_beta beta x - 1))
then
(
x -
bpow (
fexp (
ln_beta beta x - 1)))%
R
else
(
x -
ulp x)%
R.
Definition succ x :=
if (
Rle_bool 0
x)
then
(
x+
ulp x)%
R
else
(-
pred_pos (-
x))%
R.
Definition pred x := (-
succ (-
x))%
R.
Theorem pred_eq_pos:
forall x, (0 <=
x)%
R -> (
pred x =
pred_pos x)%
R.
Proof.
Theorem succ_eq_pos:
forall x, (0 <=
x)%
R -> (
succ x =
x +
ulp x)%
R.
Proof.
Lemma pred_eq_opp_succ_opp:
forall x,
pred x = (-
succ (-
x))%
R.
Proof.
reflexivity.
Qed.
Lemma succ_eq_opp_pred_opp:
forall x,
succ x = (-
pred (-
x))%
R.
Proof.
Lemma succ_opp:
forall x, (
succ (-
x) = -
pred x)%
R.
Proof.
Lemma pred_opp:
forall x, (
pred (-
x) = -
succ x)%
R.
Proof.
pred and succ are in the format
Theorem id_m_ulp_ge_bpow :
forall x e,
F x ->
x <>
ulp x ->
(
bpow e <
x)%
R ->
(
bpow e <=
x -
ulp x)%
R.
Proof.
Theorem id_p_ulp_le_bpow :
forall x e, (0 <
x)%
R ->
F x ->
(
x <
bpow e)%
R ->
(
x +
ulp x <=
bpow e)%
R.
Proof.
Lemma generic_format_pred_aux1:
forall x, (0 <
x)%
R ->
F x ->
x <>
bpow (
ln_beta beta x - 1) ->
F (
x -
ulp x).
Proof.
Lemma generic_format_pred_aux2 :
forall x, (0 <
x)%
R ->
F x ->
let e :=
ln_beta_val beta x (
ln_beta beta x)
in
x =
bpow (
e - 1) ->
F (
x -
bpow (
fexp (
e - 1))).
Proof.
Theorem generic_format_succ_aux1 :
forall x, (0 <
x)%
R ->
F x ->
F (
x +
ulp x).
Proof.
Theorem generic_format_pred_pos :
forall x,
F x -> (0 <
x)%
R ->
F (
pred_pos x).
Proof.
Theorem generic_format_succ :
forall x,
F x ->
F (
succ x).
Proof.
Theorem generic_format_pred :
forall x,
F x ->
F (
pred x).
Proof.
Theorem pred_pos_lt_id :
forall x, (
x <> 0)%
R ->
(
pred_pos x <
x)%
R.
Proof.
Theorem succ_gt_id :
forall x, (
x <> 0)%
R ->
(
x <
succ x)%
R.
Proof.
Theorem pred_lt_id :
forall x, (
x <> 0)%
R ->
(
pred x <
x)%
R.
Proof.
Theorem succ_ge_id :
forall x, (
x <=
succ x)%
R.
Proof.
Theorem pred_le_id :
forall x, (
pred x <=
x)%
R.
Proof.
Theorem pred_pos_ge_0 :
forall x,
(0 <
x)%
R ->
F x -> (0 <=
pred_pos x)%
R.
Proof.
Theorem pred_ge_0 :
forall x,
(0 <
x)%
R ->
F x -> (0 <=
pred x)%
R.
Proof.
Lemma pred_pos_plus_ulp_aux1 :
forall x, (0 <
x)%
R ->
F x ->
x <>
bpow (
ln_beta beta x - 1) ->
((
x -
ulp x) +
ulp (
x-
ulp x) =
x)%
R.
Proof.
Lemma pred_pos_plus_ulp_aux2 :
forall x, (0 <
x)%
R ->
F x ->
let e :=
ln_beta_val beta x (
ln_beta beta x)
in
x =
bpow (
e - 1) ->
(
x -
bpow (
fexp (
e-1)) <> 0)%
R ->
((
x -
bpow (
fexp (
e-1))) +
ulp (
x -
bpow (
fexp (
e-1))) =
x)%
R.
Proof.
Lemma pred_pos_plus_ulp_aux3 :
forall x, (0 <
x)%
R ->
F x ->
let e :=
ln_beta_val beta x (
ln_beta beta x)
in
x =
bpow (
e - 1) ->
(
x -
bpow (
fexp (
e-1)) = 0)%
R ->
(
ulp 0 =
x)%
R.
Proof.
The following one is false for x = 0 in FTZ
Theorem pred_pos_plus_ulp :
forall x, (0 <
x)%
R ->
F x ->
(
pred_pos x +
ulp (
pred_pos x) =
x)%
R.
Proof.
Rounding x + small epsilon
Theorem ln_beta_plus_eps:
forall x, (0 <
x)%
R ->
F x ->
forall eps, (0 <=
eps <
ulp x)%
R ->
ln_beta beta (
x +
eps) =
ln_beta beta x :>
Z.
Proof.
Theorem round_DN_plus_eps_pos:
forall x, (0 <=
x)%
R ->
F x ->
forall eps, (0 <=
eps <
ulp x)%
R ->
round beta fexp Zfloor (
x +
eps) =
x.
Proof.
intros x Zx Fx eps Heps.
destruct Zx as [
Zx|
Zx].
pattern x at 2 ;
rewrite Fx.
unfold round.
unfold scaled_mantissa.
simpl.
unfold canonic_exp at 1 2.
rewrite ln_beta_plus_eps ;
trivial.
apply (
f_equal (
fun m =>
F2R (
Float beta m _))).
rewrite Ztrunc_floor.
apply Zfloor_imp.
split.
apply (
Rle_trans _ _ _ (
Zfloor_lb _)).
apply Rmult_le_compat_r.
apply bpow_ge_0.
pattern x at 1 ;
rewrite <-
Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with ((
x +
ulp x) *
bpow (-
canonic_exp beta fexp x))%
R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply Rplus_lt_compat_l.
rewrite Rmult_plus_distr_r.
rewrite Z2R_plus.
apply Rplus_le_compat.
pattern x at 1 3 ;
rewrite Fx.
unfold F2R.
simpl.
rewrite Rmult_assoc.
rewrite <-
bpow_plus.
rewrite Zplus_opp_r.
rewrite Rmult_1_r.
rewrite Zfloor_Z2R.
apply Rle_refl.
rewrite ulp_neq_0.
2:
now apply Rgt_not_eq.
rewrite <-
bpow_plus.
rewrite Zplus_opp_r.
apply Rle_refl.
apply Rmult_le_pos.
now apply Rlt_le.
apply bpow_ge_0.
rewrite <-
Zx,
Rplus_0_l;
rewrite <-
Zx in Heps.
case (
proj1 Heps);
intros P.
unfold round,
scaled_mantissa,
canonic_exp.
revert Heps;
unfold ulp.
rewrite Req_bool_true;
trivial.
case negligible_exp_spec.
intros _ (
H1,
H2).
absurd (0 < 0)%
R;
auto with real.
now apply Rle_lt_trans with (1:=
H1).
intros n Hn H.
assert (
fexp (
ln_beta beta eps) =
fexp n).
apply valid_exp;
try assumption.
assert(
ln_beta beta eps-1 <
fexp n)%
Z;[
idtac|
omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=
proj2 H).
destruct (
ln_beta beta eps)
as (
e,
He).
simpl;
rewrite Rabs_pos_eq in He.
now apply He,
Rgt_not_eq.
now left.
replace (
Zfloor (
eps *
bpow (-
fexp (
ln_beta beta eps))))
with 0%
Z.
unfold F2R;
simpl;
ring.
apply sym_eq,
Zfloor_imp.
split.
apply Rmult_le_pos.
now left.
apply bpow_ge_0.
apply Rmult_lt_reg_r with (
bpow (
fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <-
bpow_plus.
rewrite H0;
ring_simplify (-
fexp n +
fexp n)%
Z.
simpl;
rewrite Rmult_1_l,
Rmult_1_r.
apply H.
rewrite <-
P,
round_0;
trivial.
apply valid_rnd_DN.
Qed.
Theorem round_UP_plus_eps_pos :
forall x, (0 <=
x)%
R ->
F x ->
forall eps, (0 <
eps <=
ulp x)%
R ->
round beta fexp Zceil (
x +
eps) = (
x +
ulp x)%
R.
Proof with
auto with typeclass_instances.
intros x Zx Fx eps.
case Zx;
intros Zx1.
intros (
Heps1,[
Heps2|
Heps2]).
assert (
Heps: (0 <=
eps <
ulp x)%
R).
split.
now apply Rlt_le.
exact Heps2.
assert (
Hd :=
round_DN_plus_eps_pos x Zx Fx eps Heps).
rewrite round_UP_DN_ulp.
rewrite Hd.
rewrite 2!
ulp_neq_0.
unfold canonic_exp.
now rewrite ln_beta_plus_eps.
now apply Rgt_not_eq.
now apply Rgt_not_eq,
Rplus_lt_0_compat.
intros Fs.
rewrite round_generic in Hd...
apply Rgt_not_eq with (2 :=
Hd).
pattern x at 2 ;
rewrite <-
Rplus_0_r.
now apply Rplus_lt_compat_l.
rewrite Heps2.
apply round_generic...
now apply generic_format_succ_aux1.
rewrite <-
Zx1, 2!
Rplus_0_l.
intros Heps.
case (
proj2 Heps).
unfold round,
scaled_mantissa,
canonic_exp.
unfold ulp.
rewrite Req_bool_true;
trivial.
case negligible_exp_spec.
intros H2.
intros J;
absurd (0 < 0)%
R;
auto with real.
apply Rlt_trans with eps;
try assumption;
apply Heps.
intros n Hn H.
assert (
fexp (
ln_beta beta eps) =
fexp n).
apply valid_exp;
try assumption.
assert(
ln_beta beta eps-1 <
fexp n)%
Z;[
idtac|
omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=
H).
destruct (
ln_beta beta eps)
as (
e,
He).
simpl;
rewrite Rabs_pos_eq in He.
now apply He,
Rgt_not_eq.
now left.
replace (
Zceil (
eps *
bpow (-
fexp (
ln_beta beta eps))))
with 1%
Z.
unfold F2R;
simpl;
rewrite H0;
ring.
apply sym_eq,
Zceil_imp.
split.
simpl;
apply Rmult_lt_0_compat.
apply Heps.
apply bpow_gt_0.
apply Rmult_le_reg_r with (
bpow (
fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <-
bpow_plus.
rewrite H0;
ring_simplify (-
fexp n +
fexp n)%
Z.
simpl;
rewrite Rmult_1_l,
Rmult_1_r.
now left.
intros P;
rewrite P.
apply round_generic...
apply generic_format_ulp_0.
Qed.
Theorem round_UP_pred_plus_eps_pos :
forall x, (0 <
x)%
R ->
F x ->
forall eps, (0 <
eps <=
ulp (
pred x) )%
R ->
round beta fexp Zceil (
pred x +
eps) =
x.
Proof.
Theorem round_DN_minus_eps_pos :
forall x, (0 <
x)%
R ->
F x ->
forall eps, (0 <
eps <=
ulp (
pred x))%
R ->
round beta fexp Zfloor (
x -
eps) =
pred x.
Proof.
Theorem round_DN_plus_eps:
forall x,
F x ->
forall eps, (0 <=
eps <
if (
Rle_bool 0
x)
then (
ulp x)
else (
ulp (
pred (-
x))))%
R ->
round beta fexp Zfloor (
x +
eps) =
x.
Proof.
Theorem round_UP_plus_eps :
forall x,
F x ->
forall eps, (0 <
eps <=
if (
Rle_bool 0
x)
then (
ulp x)
else (
ulp (
pred (-
x))))%
R ->
round beta fexp Zceil (
x +
eps) = (
succ x)%
R.
Proof with
Lemma le_pred_pos_lt :
forall x y,
F x ->
F y ->
(0 <=
x <
y)%
R ->
(
x <=
pred_pos y)%
R.
Proof with
Theorem succ_le_lt_aux:
forall x y,
F x ->
F y ->
(0 <=
x)%
R -> (
x <
y)%
R ->
(
succ x <=
y)%
R.
Proof with
Theorem succ_le_lt:
forall x y,
F x ->
F y ->
(
x <
y)%
R ->
(
succ x <=
y)%
R.
Proof with
Theorem le_pred_lt :
forall x y,
F x ->
F y ->
(
x <
y)%
R ->
(
x <=
pred y)%
R.
Proof.
Theorem lt_succ_le :
forall x y,
(
y <> 0)%
R ->
(
x <=
y)%
R ->
(
x <
succ y)%
R.
Proof.
Theorem pred_lt_le :
forall x y,
(
x <> 0)%
R ->
(
x <=
y)%
R ->
(
pred x <
y)%
R.
Proof.
Theorem succ_pred_aux :
forall x,
F x -> (0 <
x)%
R ->
succ (
pred x)=
x.
Proof.
Theorem pred_ulp_0 :
pred (
ulp 0) = 0%
R.
Proof.
Theorem succ_0 :
succ 0 =
ulp 0.
Proof.
Theorem pred_0 :
pred 0 =
Ropp (
ulp 0).
Proof.
Theorem pred_succ_aux :
forall x,
F x -> (0 <
x)%
R ->
pred (
succ x) =
x.
Proof.
Theorem succ_pred :
forall x,
F x ->
succ (
pred x) =
x.
Proof.
Theorem pred_succ :
forall x,
F x ->
pred (
succ x) =
x.
Proof.
Theorem round_UP_pred_plus_eps :
forall x,
F x ->
forall eps, (0 <
eps <=
if (
Rle_bool x 0)
then (
ulp x)
else (
ulp (
pred x)))%
R ->
round beta fexp Zceil (
pred x +
eps) =
x.
Proof.
Theorem round_DN_minus_eps:
forall x,
F x ->
forall eps, (0 <
eps <=
if (
Rle_bool x 0)
then (
ulp x)
else (
ulp (
pred x)))%
R ->
round beta fexp Zfloor (
x -
eps) =
pred x.
Proof.
Error of a rounding, expressed in number of ulps
false for x=0 in the FLX format
Theorem error_lt_ulp :
forall rnd {
Zrnd :
Valid_rnd rnd }
x,
(
x <> 0)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
ulp x)%
R.
Proof with
Theorem error_le_ulp :
forall rnd {
Zrnd :
Valid_rnd rnd }
x,
(
Rabs (
round beta fexp rnd x -
x) <=
ulp x)%
R.
Proof with
Theorem error_le_half_ulp :
forall choice x,
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
ulp x)%
R.
Proof with
Theorem ulp_DN :
forall x,
(0 <
round beta fexp Zfloor x)%
R ->
ulp (
round beta fexp Zfloor x) =
ulp x.
Proof with
Theorem round_neq_0_negligible_exp:
negligible_exp=
None ->
forall rnd {
Zrnd :
Valid_rnd rnd }
x,
(
x <> 0)%
R -> (
round beta fexp rnd x <> 0)%
R.
Proof with
auto with typeclass_instances.
intros H rndn Hrnd x Hx K.
case negligible_exp_spec'.
intros (
_,
Hn).
destruct (
ln_beta beta x)
as (
e,
He).
absurd (
fexp e <
e)%
Z.
apply Zle_not_lt.
apply exp_small_round_0 with beta rndn x...
apply (
Hn e).
intros (
n,(
H1,
_)).
rewrite H in H1;
discriminate.
Qed.
allows rnd x to be 0
Theorem error_lt_ulp_round :
forall {
Hm :
Monotone_exp fexp }
rnd {
Zrnd :
Valid_rnd rnd }
x,
(
x <> 0)%
R ->
(
Rabs (
round beta fexp rnd x -
x) <
ulp (
round beta fexp rnd x))%
R.
Proof with
allows both x and rnd x to be 0
Theorem error_le_half_ulp_round :
forall {
Hm :
Monotone_exp fexp },
forall choice x,
(
Rabs (
round beta fexp (
Znearest choice)
x -
x) <= /2 *
ulp (
round beta fexp (
Znearest choice)
x))%
R.
Proof with
auto with typeclass_instances.
intros Hm choice x.
case (
Req_dec (
round beta fexp (
Znearest choice)
x) 0);
intros Hfx.
case (
Req_dec x 0);
intros Hx.
apply Rle_trans with (1:=
error_le_half_ulp _ _).
rewrite Hx,
round_0...
right;
ring.
generalize (
error_le_half_ulp choice x).
rewrite Hfx.
unfold Rminus;
rewrite Rplus_0_l,
Rabs_Ropp.
intros N.
unfold ulp;
rewrite Req_bool_true;
trivial.
case negligible_exp_spec'.
intros (
H1,
H2).
contradict Hfx.
apply round_neq_0_negligible_exp...
intros (
n,(
H1,
Hn));
rewrite H1.
apply Rle_trans with (1:=
N).
right;
apply f_equal.
rewrite ulp_neq_0;
trivial.
apply f_equal.
unfold canonic_exp.
apply valid_exp;
trivial.
assert (
ln_beta beta x -1 <
fexp n)%
Z;[
idtac|
omega].
apply lt_bpow with beta.
destruct (
ln_beta beta x)
as (
e,
He).
simpl.
apply Rle_lt_trans with (
Rabs x).
now apply He.
apply Rle_lt_trans with (
Rabs (
round beta fexp (
Znearest choice)
x -
x)).
right;
rewrite Hfx;
unfold Rminus;
rewrite Rplus_0_l.
apply sym_eq,
Rabs_Ropp.
apply Rlt_le_trans with (
ulp 0).
rewrite <-
Hfx.
apply error_lt_ulp_round...
unfold ulp;
rewrite Req_bool_true,
H1;
trivial.
now right.
case (
round_DN_or_UP beta fexp (
Znearest choice)
x);
intros Hx.
case (
Rle_or_lt 0 (
round beta fexp Zfloor x)).
intros H;
destruct H.
rewrite Hx at 2.
rewrite ulp_DN;
trivial.
apply error_le_half_ulp.
rewrite Hx in Hfx;
contradict Hfx;
auto with real.
intros H.
apply Rle_trans with (1:=
error_le_half_ulp _ _).
apply Rmult_le_compat_l.
apply Rlt_le,
pos_half_prf.
apply ulp_le.
rewrite Hx;
rewrite (
Rabs_left1 x),
Rabs_left;
try assumption.
apply Ropp_le_contravar.
apply (
round_DN_pt beta fexp x).
case (
Rle_or_lt x 0);
trivial.
intros H1;
contradict H.
apply Rle_not_lt.
apply round_ge_generic...
apply generic_format_0.
now left.
case (
Rle_or_lt 0 (
round beta fexp Zceil x)).
intros H;
destruct H.
apply Rle_trans with (1:=
error_le_half_ulp _ _).
apply Rmult_le_compat_l.
apply Rlt_le,
pos_half_prf.
apply ulp_le_pos;
trivial.
case (
Rle_or_lt 0
x);
trivial.
intros H1;
contradict H.
apply Rle_not_lt.
apply round_le_generic...
apply generic_format_0.
now left.
rewrite Hx;
apply (
round_UP_pt beta fexp x).
rewrite Hx in Hfx;
contradict Hfx;
auto with real.
intros H.
rewrite Hx at 2;
rewrite <- (
ulp_opp (
round beta fexp Zceil x)).
rewrite <-
round_DN_opp.
rewrite ulp_DN;
trivial.
pattern x at 1 2;
rewrite <-
Ropp_involutive.
rewrite round_N_opp.
unfold Rminus.
rewrite <-
Ropp_plus_distr,
Rabs_Ropp.
apply error_le_half_ulp.
rewrite round_DN_opp;
apply Ropp_0_gt_lt_contravar;
apply Rlt_gt;
assumption.
Qed.
Theorem pred_le :
forall x y,
F x ->
F y -> (
x <=
y)%
R ->
(
pred x <=
pred y)%
R.
Proof.
Theorem succ_le:
forall x y,
F x ->
F y -> (
x <=
y)%
R -> (
succ x <=
succ y)%
R.
Proof.
Theorem pred_le_inv:
forall x y,
F x ->
F y
-> (
pred x <=
pred y)%
R -> (
x <=
y)%
R.
Proof.
Theorem succ_le_inv:
forall x y,
F x ->
F y
-> (
succ x <=
succ y)%
R -> (
x <=
y)%
R.
Proof.
Theorem pred_lt :
forall x y,
F x ->
F y -> (
x <
y)%
R ->
(
pred x <
pred y)%
R.
Proof.
Theorem succ_lt :
forall x y,
F x ->
F y -> (
x <
y)%
R ->
(
succ x <
succ y)%
R.
Proof.
Theorem le_round_DN_lt_UP :
forall x y,
F y ->
(
y <
round beta fexp Zceil x ->
y <=
round beta fexp Zfloor x)%
R.
Proof with
Theorem round_UP_le_gt_DN :
forall x y,
F y ->
(
round beta fexp Zfloor x <
y ->
round beta fexp Zceil x <=
y)%
R.
Proof with
Theorem pred_UP_le_DN :
forall x, (
pred (
round beta fexp Zceil x) <=
round beta fexp Zfloor x)%
R.
Proof with
Theorem pred_UP_eq_DN :
forall x, ~
F x ->
(
pred (
round beta fexp Zceil x) =
round beta fexp Zfloor x)%
R.
Proof with
Theorem succ_DN_eq_UP :
forall x, ~
F x ->
(
succ (
round beta fexp Zfloor x) =
round beta fexp Zceil x)%
R.
Proof with
Theorem round_DN_eq_betw:
forall x d,
F d
-> (
d <=
x <
succ d)%
R
->
round beta fexp Zfloor x =
d.
Proof with
Theorem round_UP_eq_betw:
forall x u,
F u
-> (
pred u <
x <=
u)%
R
->
round beta fexp Zceil x =
u.
Proof with
Properties of rounding to nearest and ulp
Theorem round_N_le_midp:
forall choice u v,
F u -> (
v < (
u +
succ u)/2)%
R
-> (
round beta fexp (
Znearest choice)
v <=
u)%
R.
Proof with
Theorem round_N_ge_midp:
forall choice u v,
F u -> ((
u +
pred u)/2 <
v)%
R
-> (
u <=
round beta fexp (
Znearest choice)
v)%
R.
Proof with
Lemma round_N_eq_DN:
forall choice x,
let d:=
round beta fexp Zfloor x in
let u:=
round beta fexp Zceil x in
(
x<(
d+
u)/2)%
R ->
round beta fexp (
Znearest choice)
x =
d.
Proof with
Lemma round_N_eq_DN_pt:
forall choice x d u,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
(
x<(
d+
u)/2)%
R ->
round beta fexp (
Znearest choice)
x =
d.
Proof with
Lemma round_N_eq_UP:
forall choice x,
let d:=
round beta fexp Zfloor x in
let u:=
round beta fexp Zceil x in
((
d+
u)/2 <
x)%
R ->
round beta fexp (
Znearest choice)
x =
u.
Proof with
Lemma round_N_eq_UP_pt:
forall choice x d u,
Rnd_DN_pt F x d ->
Rnd_UP_pt F x u ->
((
d+
u)/2 <
x)%
R ->
round beta fexp (
Znearest choice)
x =
u.
Proof with
End Fcore_ulp.