Module Fcore_rnd_ne
Lemma round_NE_pt_pos :
forall x,
(0 < x)%R ->
Rnd_NE_pt x (round beta fexp ZnearestE x).
Proof with
auto with typeclass_instances.
intros x Hx.
split.
now apply round_N_pt.
unfold NE_prop.
set (
mx :=
scaled_mantissa beta fexp x).
set (
xr :=
round beta fexp ZnearestE x).
destruct (
Req_dec (
mx -
Z2R (
Zfloor mx)) (/2))
as [
Hm|
Hm].
midpoint *)
left.
exists (
Float beta (
Ztrunc (
scaled_mantissa beta fexp xr)) (
canonic_exp beta fexp xr)).
split.
apply round_N_pt...
split.
unfold Fcore_generic_fmt.canonic.
simpl.
apply f_equal.
apply round_N_pt...
simpl.
unfold xr,
round,
Znearest.
fold mx.
rewrite Hm.
rewrite Rcompare_Eq. 2:
apply refl_equal.
case_eq (
Zeven (
Zfloor mx)) ;
intros Hmx.
. even floor *)
change (
Zeven (
Ztrunc (
scaled_mantissa beta fexp (
round beta fexp Zfloor x))) =
true).
destruct (
Rle_or_lt (
round beta fexp Zfloor x) 0)
as [
Hr|
Hr].
rewrite (
Rle_antisym _ _ Hr).
unfold scaled_mantissa.
rewrite Rmult_0_l.
change R0 with (
Z2R 0).
now rewrite (
Ztrunc_Z2R 0).
rewrite <- (
round_0 beta fexp Zfloor).
apply round_le...
now apply Rlt_le.
rewrite scaled_mantissa_DN...
now rewrite Ztrunc_Z2R.
. odd floor *)
change (
Zeven (
Ztrunc (
scaled_mantissa beta fexp (
round beta fexp Zceil x))) =
true).
destruct (
ln_beta beta x)
as (
ex,
Hex).
specialize (
Hex (
Rgt_not_eq _ _ Hx)).
rewrite (
Rabs_pos_eq _ (
Rlt_le _ _ Hx))
in Hex.
destruct (
Z_lt_le_dec (
fexp ex)
ex)
as [
He|
He].
.. large pos *)
assert (
Hu :=
round_bounded_large_pos _ _ Zceil _ _ He Hex).
assert (
Hfc:
Zceil mx = (
Zfloor mx + 1)%
Z).
apply Zceil_floor_neq.
intros H.
rewrite H in Hm.
unfold Rminus in Hm.
rewrite Rplus_opp_r in Hm.
elim (
Rlt_irrefl 0).
rewrite Hm at 2.
apply Rinv_0_lt_compat.
now apply (
Z2R_lt 0 2).
destruct (
proj2 Hu)
as [
Hu'|
Hu'].
... u <> bpow *)
unfold scaled_mantissa.
rewrite canonic_exp_fexp_pos with (1 :=
conj (
proj1 Hu)
Hu').
unfold round,
F2R.
simpl.
rewrite canonic_exp_fexp_pos with (1 :=
Hex).
rewrite Rmult_assoc, <-
bpow_plus,
Zplus_opp_r,
Rmult_1_r.
rewrite Ztrunc_Z2R.
fold mx.
rewrite Hfc.
now rewrite Zeven_plus,
Hmx.
... u = bpow *)
rewrite Hu'.
unfold scaled_mantissa,
canonic_exp.
rewrite ln_beta_bpow.
rewrite <-
bpow_plus, <-
Z2R_Zpower.
rewrite Ztrunc_Z2R.
case_eq (
Zeven beta) ;
intros Hr.
destruct exists_NE_ as [
Hs|
Hs].
now rewrite Hs in Hr.
destruct (
Hs ex)
as (
H,
_).
rewrite Zeven_Zpower.
exact Hr.
omega.
assert (
Zeven (
Zfloor mx) =
true). 2:
now rewrite H in Hmx.
replace (
Zfloor mx)
with (
Zceil mx + -1)%
Z by omega.
rewrite Zeven_plus.
apply eqb_true.
unfold mx.
replace (
Zceil (
scaled_mantissa beta fexp x))
with (
Zpower beta (
ex -
fexp ex)).
rewrite Zeven_Zpower_odd with (2 :=
Hr).
easy.
omega.
apply eq_Z2R.
rewrite Z2R_Zpower. 2:
omega.
apply Rmult_eq_reg_r with (
bpow (
fexp ex)).
unfold Zminus.
rewrite bpow_plus.
rewrite Rmult_assoc, <-
bpow_plus,
Zplus_opp_l,
Rmult_1_r.
pattern (
fexp ex) ;
rewrite <-
canonic_exp_fexp_pos with (1 :=
Hex).
now apply sym_eq.
apply Rgt_not_eq.
apply bpow_gt_0.
generalize (
proj1 (
valid_exp ex)
He).
omega.
.. small pos *)
assert (
Zeven (
Zfloor mx) =
true). 2:
now rewrite H in Hmx.
unfold mx,
scaled_mantissa.
rewrite canonic_exp_fexp_pos with (1 :=
Hex).
now rewrite mantissa_DN_small_pos.
not midpoint *)
right.
intros g Hg.
destruct (
Req_dec x g)
as [
Hxg|
Hxg].
rewrite <-
Hxg.
apply sym_eq.
apply round_generic...
rewrite Hxg.
apply Hg.
set (
d :=
round beta fexp Zfloor x).
set (
u :=
round beta fexp Zceil x).
apply Rnd_N_pt_unicity with (
d :=
d) (
u :=
u) (4 :=
Hg).
now apply round_DN_pt.
now apply round_UP_pt.
2:
now apply round_N_pt.
rewrite <- (
scaled_mantissa_mult_bpow beta fexp x).
unfold d,
u,
round,
F2R.
simpl.
fold mx.
rewrite <- 2!
Rmult_minus_distr_r.
intros H.
apply Rmult_eq_reg_r in H.
apply Hm.
apply Rcompare_Eq_inv.
rewrite Rcompare_floor_ceil_mid.
now apply Rcompare_Eq.
contradict Hxg.
apply sym_eq.
apply Rnd_N_pt_idempotent with (1 :=
Hg).
rewrite <- (
scaled_mantissa_mult_bpow beta fexp x).
fold mx.
rewrite <-
Hxg.
change (
Z2R (
Zfloor mx) *
bpow (
canonic_exp beta fexp x))%
R with d.
now eapply round_DN_pt.
apply Rgt_not_eq.
apply bpow_gt_0.
Qed.
Theorem round_NE_opp :
forall x,
round beta fexp ZnearestE (-x) = (- round beta fexp ZnearestE x)%R.
Proof.
Lemma round_NE_abs:
forall x : R,
round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x).
Proof with
Theorem round_NE_pt :
forall x,
Rnd_NE_pt x (round beta fexp ZnearestE x).
Proof with
End Fcore_rnd_NE.
Notations for backward-compatibility with Flocq 1.4.
Notation rndNE := ZnearestE (only parsing).