Commit df0c5952 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Work around the infamous bug due to clearing section variables.

parent 0810e3f1
...@@ -846,83 +846,9 @@ Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)). ...@@ -846,83 +846,9 @@ Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)).
Definition average3 (x y : R) :=round_flt(x+round_flt(round_flt(y-x)/2)). Definition average3 (x y : R) :=round_flt(x+round_flt(round_flt(y-x)/2)).
Variables x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.
Let a:=(x+y)/2.
Let av:=average3 x y.
Lemma average3_symmetry_Ropp: forall u v, average3 (-u) (-v) = - average3 u v.
intros u v; unfold average3.
replace (-v--u) with (-(v-u)) by ring.
rewrite round_NE_opp.
replace (- round_flt (v-u) / 2) with (- (round_flt (v-u) / 2)) by (unfold Rdiv; ring).
rewrite round_NE_opp.
replace (- u + - round_flt (round_flt (v - u) / 2)) with
(-(u+round_flt (round_flt (v - u) / 2))) by ring.
apply round_NE_opp.
Qed.
Lemma average3_same_sign_1: 0 <= a -> 0 <= av.
Proof with auto with typeclass_instances.
intros H.
apply round_ge_generic...
apply generic_format_0.
apply Rplus_le_reg_l with (-x).
ring_simplify.
apply round_ge_generic...
now apply generic_format_opp.
apply Rmult_le_reg_l with (1 := Rlt_0_2).
apply Rle_trans with (-(2*x)).
right; ring.
apply Rle_trans with (round_flt (y - x)).
2: right; field.
apply round_ge_generic...
apply generic_format_opp.
now apply FLT_format_double...
apply Rplus_le_reg_l with (2*x).
apply Rmult_le_reg_r with (/2).
lra.
apply Rle_trans with 0;[right; ring|idtac].
apply Rle_trans with (1:=H).
right; unfold a, Rdiv; ring.
Qed.
Lemma average3_same_sign_2: a <= 0-> av <= 0.
Proof with auto with typeclass_instances.
intros H.
apply round_le_generic...
apply generic_format_0.
apply Rplus_le_reg_l with (-x).
ring_simplify.
apply round_le_generic...
now apply generic_format_opp.
apply Rmult_le_reg_l with (1 := Rlt_0_2).
apply Rle_trans with (-(2*x)).
2: right; ring.
apply Rle_trans with (round_flt (y - x)).
right; field.
apply round_le_generic...
apply generic_format_opp.
now apply FLT_format_double...
apply Rplus_le_reg_l with (2*x).
apply Rmult_le_reg_r with (/2).
lra.
apply Rle_trans with 0;[idtac|right; ring].
apply Rle_trans with (2:=H).
right; unfold a, Rdiv; ring.
Qed.
Lemma average3_between_aux: forall u v, format u -> format v -> u <= v -> Lemma average3_between_aux: forall u v, format u -> format v -> u <= v ->
u <= average3 u v <= v. u <= average3 u v <= v.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear Fx Fy a av x y.
intros x y Fx Fy M. intros x y Fx Fy M.
split. split.
(* . *) (* . *)
...@@ -1035,54 +961,18 @@ unfold Zminus; rewrite bpow_plus. ...@@ -1035,54 +961,18 @@ unfold Zminus; rewrite bpow_plus.
reflexivity. reflexivity.
Qed. Qed.
Lemma average3_between: Rmin x y <= av <= Rmax x y. Lemma average3_symmetry_Ropp: forall u v, average3 (-u) (-v) = - average3 u v.
Proof with auto with typeclass_instances. Proof.
case (Rle_or_lt x y); intros M. intros u v; unfold average3.
(* x <= y *) replace (-v--u) with (-(v-u)) by ring.
rewrite Rmin_left; try exact M. rewrite round_NE_opp.
rewrite Rmax_right; try exact M. replace (- round_flt (v-u) / 2) with (- (round_flt (v-u) / 2)) by (unfold Rdiv; ring).
now apply average3_between_aux. rewrite round_NE_opp.
(* y < x *) replace (- u + - round_flt (round_flt (v - u) / 2)) with
rewrite Rmin_right; try now left. (-(u+round_flt (round_flt (v - u) / 2))) by ring.
rewrite Rmax_left; try now left. apply round_NE_opp.
unfold av; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y).
rewrite average3_symmetry_Ropp.
split; apply Ropp_le_contravar.
apply average3_between_aux.
now apply generic_format_opp.
now apply generic_format_opp.
apply Ropp_le_contravar; now left.
apply average3_between_aux.
now apply generic_format_opp.
now apply generic_format_opp.
apply Ropp_le_contravar; now left.
Qed.
Lemma average3_zero: a = 0 -> av = 0.
Proof with auto with typeclass_instances.
intros H.
assert (y=-x).
apply Rplus_eq_reg_l with x.
apply Rmult_eq_reg_r with (/2).
apply trans_eq with a.
reflexivity.
rewrite H; ring.
lra.
unfold av, average3.
rewrite H0.
replace (-x-x) with (-(2*x)) by ring.
rewrite round_generic with (x:=(-(2*x)))...
replace (-(2*x)/2) with (-x) by field.
rewrite round_generic with (x:=-x)...
replace (x+-x) with 0 by ring.
apply round_0...
now apply generic_format_opp.
apply generic_format_opp.
now apply FLT_format_double.
Qed. Qed.
Lemma average3_no_underflow_aux_aux: forall z:Z, (0 < z)%Z -> Lemma average3_no_underflow_aux_aux: forall z:Z, (0 < z)%Z ->
(ZnearestE (Z2R z / 2) < z)%Z. (ZnearestE (Z2R z / 2) < z)%Z.
Proof. Proof.
...@@ -1185,7 +1075,7 @@ Lemma average3_no_underflow_aux2: forall u v, format u -> format v -> ...@@ -1185,7 +1075,7 @@ Lemma average3_no_underflow_aux2: forall u v, format u -> format v ->
u <= v -> u <= v ->
(bpow emin) <= Rabs ((u+v)/2) -> average3 u v <> 0. (bpow emin) <= Rabs ((u+v)/2) -> average3 u v <> 0.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear Fx Fy a av x y; intros x y Fx Fy same_sign xLey H; unfold average3. intros x y Fx Fy same_sign xLey H; unfold average3.
intros J. intros J.
apply round_plus_eq_zero in J... apply round_plus_eq_zero in J...
2: apply generic_format_round... 2: apply generic_format_round...
...@@ -1239,7 +1129,7 @@ Lemma average3_no_underflow_aux3: forall u v, format u -> format v -> ...@@ -1239,7 +1129,7 @@ Lemma average3_no_underflow_aux3: forall u v, format u -> format v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
(bpow emin) <= Rabs ((u+v)/2) -> average3 u v <> 0. (bpow emin) <= Rabs ((u+v)/2) -> average3 u v <> 0.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear Fx Fy a av x y; intros x y Fx Fy. intros x y Fx Fy.
intros same_sign H. intros same_sign H.
case (Rle_or_lt x y); intros H1. case (Rle_or_lt x y); intros H1.
now apply average3_no_underflow_aux2. now apply average3_no_underflow_aux2.
...@@ -1260,21 +1150,11 @@ unfold Rdiv; ring. ...@@ -1260,21 +1150,11 @@ unfold Rdiv; ring.
Qed. Qed.
Lemma average3_no_underflow:
(0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) ->
(bpow emin) <= Rabs a -> av <> 0.
Proof with auto with typeclass_instances.
intros; now apply average3_no_underflow_aux3.
Qed.
Lemma average3_correct_aux: forall u v, format u -> format v -> u <= v -> Lemma average3_correct_aux: forall u v, format u -> format v -> u <= v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
0 < Rabs ((u+v)/2) < bpow emin -> 0 < Rabs ((u+v)/2) < bpow emin ->
Rabs (average3 u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2). Rabs (average3 u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2).
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear Fx Fy x y a av.
intros u v Fu Fv uLev same_sign. intros u v Fu Fv uLev same_sign.
pose (b:=(u+v)/2); fold b. pose (b:=(u+v)/2); fold b.
(* mostly forward proof *) (* mostly forward proof *)
...@@ -1430,13 +1310,10 @@ apply bpow_ge_0. ...@@ -1430,13 +1310,10 @@ apply bpow_ge_0.
lra. lra.
Qed. Qed.
Lemma average3_correct_aux2: forall u v, format u -> format v -> u <= v -> Lemma average3_correct_aux2: forall u v, format u -> format v -> u <= v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
Rabs (average3 u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2). Rabs (average3 u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2).
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear Fx Fy a av x y.
intros u v Fu Fv uLev same_sign. intros u v Fu Fv uLev same_sign.
pose (b:=(u+v)/2); fold b. pose (b:=(u+v)/2); fold b.
assert (T: forall z, Rabs (2*z) = 2* Rabs z). assert (T: forall z, Rabs (2*z) = 2* Rabs z).
...@@ -1631,6 +1508,119 @@ lra. ...@@ -1631,6 +1508,119 @@ lra.
apply ulp_ge_0. apply ulp_ge_0.
Qed. Qed.
Variables x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.
Let a:=(x+y)/2.
Let av:=average3 x y.
Lemma average3_same_sign_1: 0 <= a -> 0 <= av.
Proof with auto with typeclass_instances.
intros H.
apply round_ge_generic...
apply generic_format_0.
apply Rplus_le_reg_l with (-x).
ring_simplify.
apply round_ge_generic...
now apply generic_format_opp.
apply Rmult_le_reg_l with (1 := Rlt_0_2).
apply Rle_trans with (-(2*x)).
right; ring.
apply Rle_trans with (round_flt (y - x)).
2: right; field.
apply round_ge_generic...
apply generic_format_opp.
now apply FLT_format_double...
apply Rplus_le_reg_l with (2*x).
apply Rmult_le_reg_r with (/2).
lra.
apply Rle_trans with 0;[right; ring|idtac].
apply Rle_trans with (1:=H).
right; unfold a, Rdiv; ring.
Qed.
Lemma average3_same_sign_2: a <= 0-> av <= 0.
Proof with auto with typeclass_instances.
intros H.
apply round_le_generic...
apply generic_format_0.
apply Rplus_le_reg_l with (-x).
ring_simplify.
apply round_le_generic...
now apply generic_format_opp.
apply Rmult_le_reg_l with (1 := Rlt_0_2).
apply Rle_trans with (-(2*x)).
2: right; ring.
apply Rle_trans with (round_flt (y - x)).
right; field.
apply round_le_generic...
apply generic_format_opp.
now apply FLT_format_double...
apply Rplus_le_reg_l with (2*x).
apply Rmult_le_reg_r with (/2).
lra.
apply Rle_trans with 0;[idtac|right; ring].
apply Rle_trans with (2:=H).
right; unfold a, Rdiv; ring.
Qed.
Lemma average3_between: Rmin x y <= av <= Rmax x y.
Proof with auto with typeclass_instances.
case (Rle_or_lt x y); intros M.
(* x <= y *)
rewrite Rmin_left; try exact M.
rewrite Rmax_right; try exact M.
now apply average3_between_aux.
(* y < x *)
rewrite Rmin_right; try now left.
rewrite Rmax_left; try now left.
unfold av; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y).
rewrite average3_symmetry_Ropp.
split; apply Ropp_le_contravar.
apply average3_between_aux.
now apply generic_format_opp.
now apply generic_format_opp.
apply Ropp_le_contravar; now left.
apply average3_between_aux.
now apply generic_format_opp.
now apply generic_format_opp.
apply Ropp_le_contravar; now left.
Qed.
Lemma average3_zero: a = 0 -> av = 0.
Proof with auto with typeclass_instances.
intros H.
assert (y=-x).
apply Rplus_eq_reg_l with x.
apply Rmult_eq_reg_r with (/2).
apply trans_eq with a.
reflexivity.
rewrite H; ring.
lra.
unfold av, average3.
rewrite H0.
replace (-x-x) with (-(2*x)) by ring.
rewrite round_generic with (x:=(-(2*x)))...
replace (-(2*x)/2) with (-x) by field.
rewrite round_generic with (x:=-x)...
replace (x+-x) with 0 by ring.
apply round_0...
now apply generic_format_opp.
apply generic_format_opp.
now apply FLT_format_double.
Qed.
Lemma average3_no_underflow:
(0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) ->
(bpow emin) <= Rabs a -> av <> 0.
Proof with auto with typeclass_instances.
intros; now apply average3_no_underflow_aux3.
Qed.
(* tight example x=1/2 and y=2^p-1: error is 5/4 ulp *) (* tight example x=1/2 and y=2^p-1: error is 5/4 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