Commit 4d4cef15 authored by BOLDO Sylvie's avatar BOLDO Sylvie

New rounding_N_opp (with negb (choice -x))

New theorems:  ulp_error_f and ulp_half error_f with the ulp of the rounding
parent d095c75c
......@@ -1170,34 +1170,6 @@ apply Rmult_lt_compat_r with (2 := H1).
now apply (Z2R_lt 0 2).
Qed.
Theorem Znearest_opp :
( forall x, (x - Z2R (Zfloor x) = /2)%R -> choice (-x) = negb (choice x) ) ->
forall x,
Znearest (- x) = (- Znearest x)%Z.
Proof.
intros Hc x.
destruct (Req_dec (Z2R (Zfloor x)) x) as [Hx|Hx].
rewrite <- Hx.
rewrite <- opp_Z2R.
now rewrite 2!Znearest_Z2R.
unfold Znearest.
replace (- x - Z2R (Zfloor (-x)))%R with (Z2R (Zceil x) - x)%R.
rewrite Rcompare_ceil_floor_mid with (1 := Hx).
rewrite Rcompare_sym.
rewrite <- Rcompare_floor_ceil_mid with (1 := Hx).
unfold Zceil.
rewrite Ropp_involutive.
case Rcompare_spec ; simpl ; trivial.
intros H.
rewrite Hc with (1 := H).
case choice ; simpl ; trivial.
now rewrite Zopp_involutive.
intros _.
now rewrite Zopp_involutive.
unfold Zceil.
rewrite opp_Z2R.
apply Rplus_comm.
Qed.
Definition ZrndN := mkZrounding2 Znearest Znearest_monotone Znearest_Z2R.
......@@ -1346,21 +1318,54 @@ apply Rle_trans with (1 := H).
apply Rmin_r.
Qed.
End Znearest.
Section ZrndN_opp.
Theorem Znearest_opp :
forall choice x,
Znearest choice (- x) = (- Znearest (fun t => negb (choice (-t)%R)) x)%Z.
Proof.
intros choice x.
destruct (Req_dec (Z2R (Zfloor x)) x) as [Hx|Hx].
rewrite <- Hx.
rewrite <- opp_Z2R.
now rewrite 2!Znearest_Z2R.
unfold Znearest.
replace (- x - Z2R (Zfloor (-x)))%R with (Z2R (Zceil x) - x)%R.
rewrite Rcompare_ceil_floor_mid with (1 := Hx).
rewrite Rcompare_floor_ceil_mid with (1 := Hx).
rewrite Rcompare_sym.
unfold Zceil.
rewrite Ropp_involutive.
case Rcompare_spec ; simpl ; trivial.
intros H.
case (choice (-x)%R); simpl; trivial.
now rewrite Zopp_involutive.
intros _.
now rewrite Zopp_involutive.
unfold Zceil.
rewrite opp_Z2R.
apply Rplus_comm.
Qed.
Theorem rounding_N_opp :
( forall x, (x - Z2R (Zfloor x) = /2)%R -> choice (-x) = negb (choice x) ) ->
forall choice,
forall x,
rounding ZrndN (-x) = (- rounding ZrndN x)%R.
rounding (ZrndN choice) (-x) = (- rounding (ZrndN (fun t => negb (choice (-t)%R))) x)%R.
Proof.
intros Hc x.
intros choice x.
unfold rounding, F2R. simpl.
rewrite canonic_exponent_opp.
rewrite scaled_mantissa_opp.
rewrite Znearest_opp.
rewrite opp_Z2R.
now rewrite Ropp_mult_distr_l_reverse.
exact Hc.
Qed.
End Znearest.
End ZrndN_opp.
End RND_generic.
......@@ -463,22 +463,24 @@ Theorem rounding_NE_opp :
forall x,
rounding beta fexp ZrndNE (-x) = (- rounding beta fexp ZrndNE x)%R.
Proof.
apply rounding_N_opp.
intros x Hx.
assert (H: Z2R (Zfloor x) <> x).
intros H.
apply Rlt_not_eq with (2 := Hx).
rewrite H.
unfold Rminus. rewrite Rplus_opp_r.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
rewrite Bool.negb_involutive.
intros x; unfold ZrndNE.
rewrite rounding_N_opp.
unfold rounding.
apply f_equal; apply f_equal; apply f_equal2; trivial.
unfold Zrnd; simpl.
generalize ((scaled_mantissa beta fexp x)); clear x; intros x.
unfold Znearest; case Rcompare_spec ; simpl ; trivial.
intros.
replace (negb (Zeven (Zfloor (- x)))) with (Zeven (Zfloor x)); trivial.
rewrite <- (Zopp_involutive (Zfloor (- x))).
fold (Zceil x).
rewrite Zeven_opp.
rewrite Zceil_floor_neq with (1 := H).
rewrite Zceil_floor_neq.
rewrite Zeven_plus.
now case (Zeven (Zfloor x)).
intros H1; contradict H.
rewrite H1; ring_simplify (x-x)%R.
apply sym_not_eq; apply Rinv_neq_0_compat; replace 2%R with (INR 2); auto with real.
Qed.
Theorem generic_NE_pt :
......
......@@ -190,4 +190,117 @@ unfold ulp.
now rewrite canonic_exponent_DN with (2 := Hd).
Qed.
Theorem ulp_error_f :
(forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) ->
forall Zrnd x,
(rounding beta fexp Zrnd x <> 0)%R ->
(Rabs (rounding beta fexp Zrnd x - x) < ulp (rounding beta fexp Zrnd x))%R.
Proof.
intros Hf Zrnd x Hfx.
case (rounding_DN_or_UP beta fexp Zrnd x); intros Hx.
(* *)
case (Rle_or_lt 0 (rounding beta fexp ZrndDN x)).
intros H; destruct H.
rewrite Hx at 2.
rewrite ulp_DN_pt_eq; trivial.
apply ulp_error.
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
apply Rlt_le_trans with (1:=ulp_error _ _).
rewrite <- (ulp_opp x), <- (ulp_opp (rounding beta fexp Zrnd x)).
apply ulp_monotone; trivial.
apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
case (Rle_or_lt 0 x); trivial.
intros H1; contradict H.
apply Rle_not_lt.
apply rounding_monotone_l; trivial.
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
apply (generic_DN_pt beta fexp prop_exp x).
(* *)
rewrite Hx; case (Rle_or_lt 0 (rounding beta fexp ZrndUP x)).
intros H; destruct H.
apply Rlt_le_trans with (1:=ulp_error _ _).
apply ulp_monotone; trivial.
case (Rle_or_lt x 0); trivial.
intros H1; contradict H.
apply Rle_not_lt.
apply rounding_monotone_r; trivial.
apply generic_format_0.
apply (generic_UP_pt beta fexp prop_exp x).
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
rewrite <- (ulp_opp (rounding beta fexp ZrndUP x)).
rewrite <- rounding_DN_opp.
rewrite ulp_DN_pt_eq; trivial.
replace (rounding beta fexp ZrndUP x - x)%R with (-((rounding beta fexp ZrndDN (-x) - (-x))))%R.
rewrite Rabs_Ropp.
apply ulp_error.
rewrite rounding_DN_opp; ring.
rewrite rounding_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
Qed.
Theorem ulp_half_error_f :
(forall m n, (m <= n)%Z -> (fexp m <= fexp n)%Z ) ->
forall choice x,
(rounding beta fexp (ZrndN choice) x <> 0)%R ->
(Rabs (rounding beta fexp (ZrndN choice) x - x) <= /2 * ulp (rounding beta fexp (ZrndN choice) x))%R.
intros Hf choice x Hfx.
case (rounding_DN_or_UP beta fexp (ZrndN choice) x); intros Hx.
(* *)
case (Rle_or_lt 0 (rounding beta fexp ZrndDN x)).
intros H; destruct H.
rewrite Hx at 2.
rewrite ulp_DN_pt_eq; trivial.
apply ulp_half_error.
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
apply Rle_trans with (1:=ulp_half_error _ _).
apply Rmult_le_compat_l.
auto with real.
rewrite <- (ulp_opp x), <- (ulp_opp (rounding beta fexp (ZrndN choice) x)).
apply ulp_monotone; trivial.
apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
case (Rle_or_lt 0 x); trivial.
intros H1; contradict H.
apply Rle_not_lt.
apply rounding_monotone_l; trivial.
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
apply (generic_DN_pt beta fexp prop_exp x).
(* *)
case (Rle_or_lt 0 (rounding beta fexp ZrndUP x)).
intros H; destruct H.
apply Rle_trans with (1:=ulp_half_error _ _).
apply Rmult_le_compat_l.
auto with real.
apply ulp_monotone; trivial.
case (Rle_or_lt x 0); trivial.
intros H1; contradict H.
apply Rle_not_lt.
apply rounding_monotone_r; trivial.
apply generic_format_0.
rewrite Hx; apply (generic_UP_pt beta fexp prop_exp x).
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
rewrite Hx at 2; rewrite <- (ulp_opp (rounding beta fexp ZrndUP x)).
rewrite <- rounding_DN_opp.
rewrite ulp_DN_pt_eq; trivial.
replace (rounding beta fexp (ZrndN choice) x - x)%R with
(-((rounding beta fexp (ZrndN (fun t => negb (choice (-t)%R))) (-x) - (-x))))%R.
rewrite Rabs_Ropp.
apply ulp_half_error.
rewrite <- (Ropp_involutive x) at 3.
rewrite rounding_N_opp with (x:=(-x)%R).
ring.
rewrite rounding_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
Qed.
End Fcore_ulp.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment