Module Fcore_ulp
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.
intros H e.
specialize (
H (
bpow (
e-1))).
rewrite ulp_neq_0 in H.
2:
apply Rgt_not_eq,
bpow_gt_0.
unfold canonic_exp in H.
rewrite ln_beta_bpow in H.
apply generic_format_bpow_inv'
in H...
now replace (
e-1+1)%
Z with e in H by ring.
Qed.
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].
. 0 < x *)
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.
. x=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.
. 0 < x *)
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.
. x=0 *)
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,
F x -> F y -> (y <> 0)%R ->
(x <= y)%R ->
(x < succ y)%R.
Proof.
Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x.
Proof.
Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R.
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.
intros x y Fx Fy Hxy.
assert (
V:( ((
x = 0) /\ (
y = 0)) \/ (
x <>0 \/
x <
y))%
R).
case (
Req_dec x 0);
intros Zx.
case Hxy;
intros Zy.
now right;
right.
left;
split;
trivial;
now rewrite <-
Zy.
now right;
left.
destruct V as [(
V1,
V2)|
V].
rewrite V1,
V2;
now right.
apply le_pred_lt;
try assumption.
apply generic_format_pred;
try assumption.
case V;
intros V1.
apply Rlt_le_trans with (2:=
Hxy).
now apply pred_lt_id.
apply Rle_lt_trans with (2:=
V1).
now apply pred_le_id.
Qed.
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 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.