Commit 1d9288f8 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Renaming + moving theorems + generalizing round_UP_plus_eps (& similar)

parent ef1c2fb4
......@@ -294,7 +294,7 @@ case (Rle_or_lt 0 h); intros H3;[destruct H3|idtac].
rewrite Rabs_right in Hh.
2: now apply Rle_ge, Rlt_le.
apply round_N_eq_DN_pt with (f+ ulp_flt f)...
pattern f at 2; rewrite <- (round_DN_plus_eps radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
pattern f at 2; rewrite <- (round_DN_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
apply round_DN_pt...
now left.
split.
......@@ -305,7 +305,7 @@ apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
fourier.
rewrite <- (round_UP_plus_eps radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
rewrite <- (round_UP_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
apply round_UP_pt...
now left.
split; trivial.
......@@ -456,7 +456,7 @@ clear T1.
destruct T.
(* normal case *)
apply round_N_eq_UP_pt with (pred_flt f)...
rewrite <- (round_DN_minus_eps radix2 (FLT_exp emin prec) f) with (eps:=-h); try assumption.
rewrite <- (round_DN_minus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=-h); try assumption.
replace (f--h) with (f+h) by ring.
apply round_DN_pt...
split.
......@@ -474,7 +474,7 @@ apply ulp_ge_0.
fourier.
intros Y; rewrite (proj1 Y); now right.
replace (f+h) with (pred_flt f + (f-pred_flt f+h)) by ring.
pattern f at 4; rewrite <- (round_UP_pred_plus_eps radix2 (FLT_exp emin prec) f) with (eps:=(f - pred_flt f + h)); try assumption.
pattern f at 4; rewrite <- (round_UP_pred_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=(f - pred_flt f + h)); try assumption.
apply round_UP_pt...
replace (f-pred_flt f) with (ulp_flt (pred_flt f)).
split.
......@@ -529,7 +529,7 @@ omega.
intros Y; now contradict T2.
assert (round radix2 (FLT_exp emin prec) Zfloor (f+h) = pred_flt f).
replace (f+h) with (f-(-h)) by ring.
apply round_DN_minus_eps...
apply round_DN_minus_eps_pos...
split.
auto with real.
rewrite T3, T1.
......@@ -538,7 +538,7 @@ apply ulp_ge_0.
fourier.
assert (round radix2 (FLT_exp emin prec) Zceil (f+h) = f).
replace (f+h) with (pred_flt f + /2*ulp_flt (pred_flt f)).
apply round_UP_pred_plus_eps...
apply round_UP_pred_plus_eps_pos...
split.
apply Rmult_lt_0_compat.
fourier.
......
......@@ -486,7 +486,7 @@ assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
now apply Rplus_lt_compat_l, Rmult_lt_compat_l; [lra|apply bpow_lt].
+ unfold ex1; rewrite <- Hl1.
fold (canonic_exp beta fexp1 rx1); rewrite <- ulp_neq_0; try now apply Rgt_not_eq.
apply succ_le_bpow; [exact Prx1| |].
apply id_p_ulp_le_bpow; [exact Prx1| |].
* now apply generic_format_round; [|apply valid_rnd_DN].
* destruct (ln_beta rx1) as (erx1, Herx1); simpl.
rewrite <- (Rabs_right rx1) at 1; [|now apply Rle_ge, Rlt_le].
......
......@@ -205,7 +205,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
{ apply (Rplus_le_reg_r (ulp beta fexp1 x)); ring_simplify.
rewrite <- ulp_DN.
- change (round _ _ _ _) with x'.
apply succ_le_bpow.
apply id_p_ulp_le_bpow.
+ exact Px'.
+ change x' with (round beta fexp1 Zfloor x).
now apply generic_format_round; [|apply valid_rnd_DN].
......@@ -2733,7 +2733,7 @@ destruct (Req_dec a 0) as [Za|Nza].
apply Rmult_lt_compat_r; [apply bpow_gt_0|lra].
+ apply Rle_trans with (a+ ulp beta fexp1 a).
right; now rewrite ulp_neq_0.
apply (succ_le_bpow _ _ _ _ Pa Fa).
apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa).
apply Rabs_lt_inv, bpow_ln_beta_gt.
- apply Rle_trans with (bpow (- 2) * u1 ^ 2).
+ unfold pow; rewrite Rmult_1_r.
......@@ -2779,7 +2779,7 @@ destruct (Req_dec a 0) as [Za|Nza].
unfold u1; fold (canonic_exp beta fexp1 (sqrt x)).
rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a.
rewrite <- ulp_neq_0; trivial.
apply succ_le_bpow.
apply id_p_ulp_le_bpow.
+ exact Pa.
+ now apply round_DN_pt.
+ apply Rle_lt_trans with (sqrt x).
......@@ -3175,7 +3175,7 @@ destruct (Req_dec a 0) as [Za|Nza].
rewrite <- (Rmult_1_l (ulp _ _ _)).
rewrite ulp_neq_0; trivial.
apply Rmult_lt_compat_r; [apply bpow_gt_0|lra].
+ apply (succ_le_bpow _ _ _ _ Pa Fa).
+ apply (id_p_ulp_le_bpow _ _ _ _ Pa Fa).
apply Rabs_lt_inv, bpow_ln_beta_gt.
- apply Rle_trans with (bpow (- 1) * u1 ^ 2).
+ unfold pow; rewrite Rmult_1_r.
......@@ -3221,7 +3221,7 @@ destruct (Req_dec a 0) as [Za|Nza].
unfold u1; fold (canonic_exp beta fexp1 (sqrt x)).
rewrite <- canonic_exp_DN; [|exact Vfexp1|exact Pa]; fold a.
rewrite <- ulp_neq_0; trivial.
apply succ_le_bpow.
apply id_p_ulp_le_bpow.
+ exact Pa.
+ now apply round_DN_pt.
+ apply Rle_lt_trans with (sqrt x).
......
......@@ -413,9 +413,12 @@ Qed.
(** pred and succ are in the format *)
Theorem pred_ge_bpow : (* TODO x <> ulp 0 (?) , renommer ? après pred ?*)
(* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *)
(* was pred_ge_bpow *)
Theorem id_m_ulp_ge_bpow :
forall x e, F x ->
x <> ulp x ->
(bpow e < x)%R ->
......@@ -455,7 +458,8 @@ apply Rgt_not_eq, Rlt_gt.
apply Rlt_trans with (2:=Hx), bpow_gt_0.
Qed.
Theorem succ_le_bpow : (* TODO mettre succ ? *)
(* was succ_le_bpow *)
Theorem id_p_ulp_le_bpow :
forall x e, (0 < x)%R -> F x ->
(x < bpow e)%R ->
(x + ulp x <= bpow e)%R.
......@@ -511,7 +515,7 @@ now rewrite Rmult_1_l.
now apply Rgt_not_eq.
rewrite Rabs_pos_eq.
split.
apply pred_ge_bpow; trivial.
apply id_m_ulp_ge_bpow; trivial.
rewrite ulp_neq_0.
intro H.
assert (ex-1 < canonic_exp beta fexp x < ex)%Z.
......@@ -617,7 +621,7 @@ destruct (ln_beta beta x) as (ex, Ex).
specialize (Ex (Rgt_not_eq _ _ Zx)).
assert (Ex' := Ex).
rewrite Rabs_pos_eq in Ex'.
destruct (succ_le_bpow x ex) ; try easy.
destruct (id_p_ulp_le_bpow x ex) ; try easy.
unfold generic_format, scaled_mantissa, canonic_exp.
rewrite ln_beta_unique with beta (x + ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
......@@ -706,196 +710,6 @@ now apply generic_format_opp.
Qed.
(** 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.
intros x Zx Fx eps Heps.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rgt_not_eq _ _ Zx)).
apply ln_beta_unique.
rewrite Rabs_pos_eq.
rewrite Rabs_pos_eq in He.
split.
apply Rle_trans with (1 := proj1 He).
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with (x + ulp x)%R.
now apply Rplus_lt_compat_l.
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_plus.
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
now apply Rlt_le.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply Heps.
Qed.
Theorem round_DN_plus_eps :
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 : (* TODO succ ! ou aux...*)
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 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 pred_pos_lt_id :
forall x, (x <> 0)%R ->
......@@ -1038,7 +852,7 @@ rewrite Rabs_right in Hex.
split.
destruct Hex as ([H1|H1],H2).
apply Rle_trans with (x-ulp x)%R.
apply pred_ge_bpow; trivial.
apply id_m_ulp_ge_bpow; trivial.
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold canonic_exp; now rewrite Lex.
......@@ -1167,13 +981,204 @@ Qed.
Theorem round_UP_pred_plus_eps :
(** 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.
intros x Zx Fx eps Heps.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rgt_not_eq _ _ Zx)).
apply ln_beta_unique.
rewrite Rabs_pos_eq.
rewrite Rabs_pos_eq in He.
split.
apply Rle_trans with (1 := proj1 He).
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with (x + ulp x)%R.
now apply Rplus_lt_compat_l.
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_plus.
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
now apply Rlt_le.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply Heps.
Qed.
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.
intros x Hx Fx eps Heps.
rewrite round_UP_plus_eps; trivial.
rewrite round_UP_plus_eps_pos; trivial.
rewrite pred_eq_pos.
apply pred_pos_plus_ulp; trivial.
now left.
......@@ -1181,8 +1186,8 @@ now apply pred_ge_0.
apply generic_format_pred; trivial.
Qed.
Theorem round_DN_minus_eps :
forall x, (0 < x)%R -> F x ->
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.
......@@ -1191,7 +1196,7 @@ rewrite pred_eq_pos;[intros Heps|now left].
replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R.
2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial.
2: ring.
rewrite round_DN_plus_eps; trivial.
rewrite round_DN_plus_eps_pos; trivial.
now apply pred_pos_ge_0.
now apply generic_format_pred_pos.
split.
......@@ -1204,6 +1209,86 @@ apply Ropp_lt_contravar.
now apply Heps.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_DN_plus_eps:
forall x, F x ->
forall eps, (0 <= eps < Rmin (ulp x) (ulp (pred (-x))))%R ->
round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
apply round_DN_plus_eps_pos; try assumption.
split; try apply Heps.
apply Rlt_le_trans with (1:=proj2 Heps).
apply Rmin_l.
(* *)
rewrite <- (Ropp_involutive (x+eps)).
pattern x at 2; rewrite <- (Ropp_involutive x).
rewrite round_DN_opp.
apply f_equal.
replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R.
rewrite round_UP_pred_plus_eps_pos; try reflexivity.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
split.
apply Rplus_lt_reg_l with eps; ring_simplify.
apply Rlt_le_trans with (1:=proj2 Heps).
apply Rmin_r.
apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify.
apply Heps.
unfold pred.
rewrite Ropp_involutive.
unfold succ; rewrite Rle_bool_false; try assumption.
rewrite Ropp_involutive; unfold Rminus.
rewrite <- Rplus_assoc, pred_pos_plus_ulp.
ring.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.
(* TODO: Rmin -> Rle_bool x 0 *)
Theorem round_UP_plus_eps :
forall x, F x ->
forall eps, (0 < eps <= Rmin (ulp x) (ulp (pred (-x))))%R ->
round beta fexp Zceil (x + eps) = (succ x)%R.
Proof with auto with typeclass_instances.