Commit a962d8f3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename ln_beta into mag.

parent 25fa9f62
......@@ -104,18 +104,18 @@ intros K; contradict Hz.
rewrite K, Rabs_R0; apply Rlt_not_le.
apply bpow_gt_0.
assert (cexp (z/2) = cexp z -1)%Z.
assert (prec+emin < ln_beta radix2 z)%Z.
assert (prec+emin < mag radix2 z)%Z.
apply lt_bpow with radix2.
destruct ln_beta as (e,He); simpl.
destruct mag as (e,He); simpl.
apply Rle_lt_trans with (1:=Hz).
now apply He.
unfold cexp, FLT_exp.
replace ((ln_beta radix2 (z/2))-prec)%Z with ((ln_beta radix2 z -1) -prec)%Z.
replace ((mag radix2 (z/2))-prec)%Z with ((mag radix2 z -1) -prec)%Z.
rewrite Z.max_l; try omega.
rewrite Z.max_l; try omega.
apply Zplus_eq_compat; try reflexivity.
apply sym_eq, ln_beta_unique.
destruct (ln_beta radix2 z) as (e,He); simpl.
apply sym_eq, mag_unique.
destruct (mag radix2 z) as (e,He); simpl.
unfold Rdiv; rewrite Rabs_mult.
rewrite (Rabs_right (/2)).
split.
......@@ -154,7 +154,7 @@ rewrite ulp_neq_0.
case (Rle_or_lt (bpow (emin+prec-1)) u); intros Hu.
unfold ulp; rewrite cexp_FLT_FLX.
unfold cexp, FLX_exp.
destruct (ln_beta radix2 u) as (e,He); simpl.
destruct (mag radix2 u) as (e,He); simpl.
apply Rle_trans with (bpow (e-1)).
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -201,7 +201,7 @@ rewrite cexp_FLT_FLX.
rewrite cexp_FLT_FLX; trivial.
unfold cexp, FLX_exp.
replace 2 with (bpow 1) by reflexivity.
rewrite Rmult_comm, ln_beta_mult_bpow.
rewrite Rmult_comm, mag_mult_bpow.
omega.
intros H; contradict Hu.
apply Rlt_not_le; rewrite H, Rabs_R0.
......@@ -290,48 +290,48 @@ omega.
apply Rlt_le_trans with (2:=H1).
apply bpow_lt.
unfold Prec_gt_0 in prec_gt_0_; omega.
assert (M:(prec + emin +1 <= ln_beta radix2 f)%Z).
apply ln_beta_ge_bpow.
assert (M:(prec + emin +1 <= mag radix2 f)%Z).
apply mag_ge_bpow.
replace (prec+emin+1-1)%Z with (prec+emin)%Z by ring.
rewrite Rabs_right; try assumption.
apply Rle_ge; now left.
assert (T1:(ulp_flt (pred_flt f) = ulp_flt f)
\/ ( ulp_flt (pred_flt f) = /2* ulp_flt f
/\ f = bpow (ln_beta radix2 f -1))).
/\ f = bpow (mag radix2 f -1))).
generalize H; rewrite pred_eq_pos; [idtac|now left].
unfold pred_pos; case Req_bool_spec; intros K HH.
(**)
right; split; try assumption.
rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
apply trans_eq with (bpow (ln_beta radix2 f- prec -1)).
apply trans_eq with (bpow (mag radix2 f- prec -1)).
apply f_equal.
unfold cexp.
apply trans_eq with (FLT_exp emin prec (ln_beta radix2 f -1)%Z).
apply trans_eq with (FLT_exp emin prec (mag radix2 f -1)%Z).
apply f_equal.
unfold FLT_exp.
rewrite Z.max_l.
2: omega.
apply ln_beta_unique.
apply mag_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f -1-prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f -1-prec)).
ring_simplify.
apply Rle_trans with (bpow (ln_beta radix2 f - 1 - 1) + bpow (ln_beta radix2 f - 1 - 1)).
apply Rle_trans with (bpow (mag radix2 f - 1 - 1) + bpow (mag radix2 f - 1 - 1)).
apply Rplus_le_compat_r.
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
apply Rle_trans with (bpow 1*bpow (ln_beta radix2 f - 1 - 1)).
apply Rle_trans with (bpow 1*bpow (mag radix2 f - 1 - 1)).
simpl; right; ring.
rewrite <- bpow_plus.
apply Rle_trans with (bpow (ln_beta radix2 f -1)).
apply Rle_trans with (bpow (mag radix2 f -1)).
apply bpow_le; omega.
rewrite <- K; now right.
rewrite <- K.
apply Rplus_lt_reg_l with (-f+bpow (ln_beta radix2 f-1-prec)); ring_simplify.
apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f-1-prec)); ring_simplify.
apply bpow_gt_0.
apply Rle_ge.
rewrite K at 1.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f - 1 - prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f - 1 - prec)).
ring_simplify.
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -345,8 +345,8 @@ unfold cexp, FLT_exp.
rewrite Z.max_l;[ring|omega].
(**)
left.
assert (bpow (ln_beta radix2 f -1) < f).
destruct (ln_beta radix2 f); simpl in *.
assert (bpow (mag radix2 f -1) < f).
destruct (mag radix2 f); simpl in *.
destruct a.
now apply Rgt_not_eq.
rewrite Rabs_right in H0.
......@@ -354,7 +354,7 @@ destruct H0; try assumption.
contradict H0.
now apply sym_not_eq.
apply Rle_ge; now left.
assert (bpow (ln_beta radix2 f -1) + ulp_flt (bpow (ln_beta radix2 f-1)) <= f).
assert (bpow (mag radix2 f -1) + ulp_flt (bpow (mag radix2 f-1)) <= f).
rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0].
apply succ_le_lt...
apply FLT_format_bpow...
......@@ -363,26 +363,26 @@ rewrite ulp_bpow in H4.
unfold FLT_exp in H4.
rewrite Z.max_l in H4.
2: omega.
replace (ln_beta radix2 f - 1 + 1 - prec)%Z with (ln_beta radix2 f - prec)%Z in H4 by ring.
replace (mag radix2 f - 1 + 1 - prec)%Z with (mag radix2 f - prec)%Z in H4 by ring.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
rewrite ulp_neq_0 at 2; try now apply Rgt_not_eq.
unfold cexp.
apply f_equal; apply f_equal.
replace (ulp_flt f) with (bpow (ln_beta radix2 f -prec)).
apply ln_beta_unique.
replace (ulp_flt f) with (bpow (mag radix2 f -prec)).
apply mag_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f -prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f -prec)).
ring_simplify.
apply Rle_trans with (2:=H4); right; ring.
apply Rlt_trans with f.
apply Rplus_lt_reg_l with (-f+bpow (ln_beta radix2 f - prec)).
apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f - prec)).
ring_simplify.
apply bpow_gt_0.
apply Rle_lt_trans with (1:=RRle_abs _).
apply bpow_ln_beta_gt.
apply bpow_mag_gt.
apply Rle_ge.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f - prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f - prec)).
ring_simplify.
left; apply Rle_lt_trans with (2:=H0).
apply bpow_le.
......@@ -395,7 +395,7 @@ omega.
assert (T: (ulp_flt (pred_flt f) = ulp_flt f \/
(ulp_flt (pred_flt f) = / 2 * ulp_flt f /\ - h < / 4 * ulp_flt f))
\/ (ulp_flt (pred_flt f) = / 2 * ulp_flt f /\
f = bpow (ln_beta radix2 f - 1) /\
f = bpow (mag radix2 f - 1) /\
- h = / 4 * ulp_flt f) ).
destruct T1.
left; now left.
......@@ -470,7 +470,7 @@ rewrite Y1.
right; field.
(* complex case: even choosing *)
elim H0; intros T1 (T2,T3); clear H0.
assert (pred_flt f = bpow (ln_beta radix2 f - 1) - bpow (ln_beta radix2 f - 1 -prec)).
assert (pred_flt f = bpow (mag radix2 f - 1) - bpow (mag radix2 f - 1 -prec)).
rewrite pred_eq_pos; try now left.
unfold pred_pos; case Req_bool_spec.
intros _; rewrite <- T2.
......@@ -503,7 +503,7 @@ apply ulp_ge_0.
fourier.
rewrite T1, H0, <- T2.
replace h with (--h) by ring; rewrite T3.
replace (bpow (ln_beta radix2 f - 1 - prec)) with (/2*ulp_flt f).
replace (bpow (mag radix2 f - 1 - prec)) with (/2*ulp_flt f).
field.
replace (/2) with (bpow (-1)) by reflexivity.
rewrite T2 at 1.
......@@ -799,8 +799,8 @@ replace (/4) with (bpow (-2)) by reflexivity.
rewrite <- bpow_plus.
apply bpow_le.
unfold cexp, FLT_exp.
assert (emin+prec+prec+1 -1 < ln_beta radix2 (x/2))%Z.
destruct (ln_beta radix2 (x/2)) as (e,He).
assert (emin+prec+prec+1 -1 < mag radix2 (x/2))%Z.
destruct (mag radix2 (x/2)) as (e,He).
simpl.
apply lt_bpow with radix2.
apply Rle_lt_trans with (Rabs (x/2)).
......@@ -1019,7 +1019,7 @@ omega.
now left.
replace (bpow emin /2) with (bpow (emin-1)).
unfold round, scaled_mantissa, cexp, FLT_exp.
rewrite ln_beta_bpow.
rewrite mag_bpow.
replace (emin - 1 + 1 - prec)%Z with (emin-prec)%Z by ring.
rewrite Z.max_r.
2: unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -1516,9 +1516,9 @@ replace 2 with (bpow 1) by reflexivity.
rewrite <- bpow_plus.
apply bpow_le.
unfold cexp, FLT_exp.
rewrite Rmult_comm, ln_beta_mult_bpow; trivial.
rewrite Rmult_comm, mag_mult_bpow; trivial.
rewrite <- Z.add_max_distr_l.
replace (ln_beta radix2 b + 1 - prec)%Z with (1 + (ln_beta radix2 b - prec))%Z by ring.
replace (mag radix2 b + 1 - prec)%Z with (1 + (mag radix2 b - prec))%Z by ring.
apply Z.max_le_compat_l.
omega.
(* . splitting case of av=0 *)
......
......@@ -38,7 +38,7 @@ Theorem pred_gt_0: forall f,
format f -> (0 < f)%R -> (0 < pred beta (FLX_exp prec) f)%R.
intros f Hf Zf.
unfold pred, Fcore_ulp.ulp, canonic_exp, FLX_exp.
destruct (ln_beta beta f) as (ef,Hef).
destruct (mag beta f) as (ef,Hef).
simpl.
assert (Zf2: (f <>0)%R) by now apply Rgt_not_eq.
specialize (Hef Zf2).
......@@ -140,7 +140,7 @@ Qed.
Theorem implies_MinOrMax_bpow:
forall x f, format f ->
f = bpow (ln_beta beta f) ->
f = bpow (mag beta f) ->
(Rabs (f-x) < /2* ulp f)%R ->
MinOrMax x f.
intros x f Hf1 Hf2 Hxf.
......
......@@ -10,7 +10,7 @@ Section Double_round_beta_odd.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Notation ln_beta x := (ln_beta beta x).
Notation mag x := (mag beta x).
(** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
Ltac bpow_simplify :=
......@@ -49,7 +49,7 @@ Lemma midpoint_beta_odd_remains_pos :
x = Z2R (Zfloor (x * bpow (- ex1))) * bpow ex1 ->
exists x',
0 < x'
/\ (ln_beta x' = ln_beta x :> Z)
/\ (mag x' = mag x :> Z)
/\ x' = Z2R (Zfloor (x' * bpow (- ex2))) * bpow ex2
/\ x + / 2 * bpow ex1 = x' + / 2 * bpow ex2.
Proof.
......@@ -105,7 +105,7 @@ induction n.
* change 0 with (Z2R 0); apply Z2R_le; omega.
* now apply bpow_ge_0.
+ rewrite <- Hlx'.
apply (ln_beta_plus_eps beta (fun e => (e - (ln_beta x' - ex2'))%Z));
apply (mag_plus_eps beta (fun e => (e - (mag x' - ex2'))%Z));
[| |split].
* exact Px'.
* unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
......@@ -193,7 +193,7 @@ Lemma neq_midpoint_beta_odd_aux1 :
forall (choice1 choice2 : Z -> bool),
forall x,
0 < x ->
(fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z ->
(fexp2 (mag x) <= fexp1 (mag x))%Z ->
midp beta fexp1 x - / 2 * ulp beta fexp2 x <= x < midp beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
......@@ -201,8 +201,8 @@ intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
unfold midp in Hx.
rewrite 2!ulp_neq_0 in Hx; try now apply Rgt_not_eq.
unfold double_round_eq.
set (ex1 := fexp1 (ln_beta x)).
set (ex2 := fexp2 (ln_beta x)).
set (ex1 := fexp1 (mag x)).
set (ex2 := fexp2 (mag x)).
set (rx1 := round beta fexp1 Zfloor x).
assert (Prx1 : 0 <= rx1).
{ rewrite <- (round_0 beta fexp1 Zfloor).
......@@ -220,7 +220,7 @@ assert (Hx' : rx2 <= x < rx2 + / 2 * bpow ex2).
- rewrite <- Hrx12; apply Hx. }
assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2).
{ unfold round, F2R, scaled_mantissa, cexp; simpl.
apply (Rmult_eq_reg_r (bpow (- fexp2 (ln_beta x))));
apply (Rmult_eq_reg_r (bpow (- fexp2 (mag x))));
[|now apply Rgt_not_eq, Rlt_gt, bpow_gt_0].
bpow_simplify.
rewrite (Znearest_imp _ _ (Zfloor (rx2 * bpow (- ex2)))).
......@@ -231,7 +231,7 @@ assert (Hr2 : round beta fexp2 (Znearest choice2) x = rx2).
apply (Rmult_le_reg_r (bpow ex2)); [now apply bpow_gt_0|].
fold ex2; bpow_simplify.
now rewrite <- Hrx2.
+ apply (Rmult_lt_reg_r (bpow (fexp2 (ln_beta x)))); [now apply bpow_gt_0|].
+ apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|].
rewrite Rmult_minus_distr_r; fold ex2; bpow_simplify.
rewrite <- Hrx2.
now apply (Rplus_lt_reg_l rx2); ring_simplify. }
......@@ -260,21 +260,21 @@ destruct (Rle_or_lt rx2 0) as [Nprx2|Prx2].
assert (Zrx2 : rx2 = 0); [now apply Rle_antisym|].
rewrite Zrx2, round_0; [|now apply valid_rnd_N].
unfold round, F2R, scaled_mantissa, cexp; simpl.
apply (Rmult_eq_reg_r (bpow (- fexp1 (ln_beta x))));
apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x))));
[|now apply Rgt_not_eq, bpow_gt_0]; rewrite Rmult_0_l; bpow_simplify.
change 0 with (Z2R 0); apply f_equal, eq_sym, Znearest_imp.
apply Rabs_lt; simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r.
split.
- apply Rlt_trans with 0; [lra|].
now apply Rmult_lt_0_compat; [|apply bpow_gt_0].
- apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta x)))); [now apply bpow_gt_0|].
- apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|].
bpow_simplify.
rewrite Zrx2, Rplus_0_l in Hx'.
apply (Rlt_le_trans _ _ _ (proj2 Hx')), Rmult_le_compat_l; [lra|].
now apply bpow_le. }
(* 0 < rx2 *)
assert (Hl2 : ln_beta rx2 = ln_beta x :> Z).
{ now rewrite Hrx2r; apply ln_beta_DN; [|rewrite <- Hrx2r]. }
assert (Hl2 : mag rx2 = mag x :> Z).
{ now rewrite Hrx2r; apply mag_DN; [|rewrite <- Hrx2r]. }
assert (Hr12 : round beta fexp1 (Znearest choice1) rx2 = rx1).
{ unfold round, F2R, scaled_mantissa, cexp; simpl.
rewrite Hl2; fold ex1.
......@@ -308,7 +308,7 @@ Lemma neq_midpoint_beta_odd_aux2 :
forall (choice1 choice2 : Z -> bool),
forall x,
0 < x ->
(fexp2 (ln_beta x) < fexp1 (ln_beta x))%Z ->
(fexp2 (mag x) < fexp1 (mag x))%Z ->
midp beta fexp1 x < x <= midp beta fexp1 x + / 2 * ulp beta fexp2 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
......@@ -316,8 +316,8 @@ intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
unfold midp in Hx.
rewrite 2!ulp_neq_0 in Hx; try now apply Rgt_not_eq.
unfold double_round_eq.
set (ex1 := fexp1 (ln_beta x)).
set (ex2 := fexp2 (ln_beta x)).
set (ex1 := fexp1 (mag x)).
set (ex2 := fexp2 (mag x)).
set (rx1 := round beta fexp1 Zfloor x).
assert (Hbeta : (2 <= beta)%Z).
{ destruct beta as (beta_val,beta_prop).
......@@ -334,15 +334,15 @@ assert (Hrx1 : rx1 = Z2R (Zfloor (rx1 * bpow (- ex1))) * bpow ex1).
unfold ex1; bpow_simplify.
now rewrite Zfloor_Z2R. }
set (rx1c := round beta fexp1 Zceil x).
assert (Hf2f1' : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z) by omega.
assert (Hf2f1' : (fexp2 (mag x) <= fexp1 (mag x))%Z) by omega.
assert (NF1x : ~ generic_format beta fexp1 x).
{ now intro H; apply NF2x, (generic_inclusion_ln_beta _ fexp1). }
{ now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). }
assert (Hrx1c : rx1c = rx1 + ulp beta fexp1 x).
{ now apply round_UP_DN_ulp. }
rewrite ulp_neq_0 in Hrx1c; try now apply Rgt_not_eq.
destruct (midpoint_beta_odd_remains rx1 Nnrx1 ex1 ex2 Hf2f1' Hrx1)
as (rx2,(Nnrx2, (Hrx2, Hrx12))).
set (rx2c := rx2 + bpow (fexp2 (ln_beta x))).
set (rx2c := rx2 + bpow (fexp2 (mag x))).
assert (Hx' : rx2c - / 2 * bpow ex2 < x <= rx2c).
{ unfold rx2c, cexp; fold ex1; fold ex2; split.
- replace (_ - _) with (rx2 + / 2 * bpow ex2) by field.
......@@ -419,8 +419,8 @@ destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
assert (Ph12 : 0 < / 2 * bpow ex1 + / 2 * bpow ex2).
{ now apply Rplus_lt_0_compat;
(apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]). }
assert (Hf1 : (fexp1 (ln_beta x) <= ln_beta x)%Z).
{ apply ln_beta_ge_bpow.
assert (Hf1 : (fexp1 (mag x) <= mag x)%Z).
{ apply mag_ge_bpow.
rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
apply Rle_trans with (/ 2 * bpow ex1).
- unfold Zminus; rewrite bpow_plus, Rmult_comm.
......@@ -430,11 +430,11 @@ destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
now change 2 with (Z2R 2); apply Z2R_le.
- apply Rlt_le.
now rewrite <- (Rplus_0_l (_ * _)), <- Zrx1. }
assert (Hl1 : ln_beta (/ 2 * bpow ex1 + / 2 * bpow ex2) = ln_beta x :> Z).
{ apply ln_beta_unique; split.
assert (Hl1 : mag (/ 2 * bpow ex1 + / 2 * bpow ex2) = mag x :> Z).
{ apply mag_unique; split.
- rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
apply Rle_trans with x.
+ destruct (ln_beta x) as (ex, Hex); simpl.
+ destruct (mag x) as (ex, Hex); simpl.
now rewrite <- (Rabs_right x);
[apply Hex, Rgt_not_eq|apply Rle_ge, Rlt_le].
+ rewrite <- (Rplus_0_l (_ * _)), <- Zrx1.
......@@ -460,10 +460,10 @@ destruct (Rle_or_lt rx1 0) as [Nprx1|Prx1].
now apply Rplus_lt_compat_l, Rmult_lt_compat;
[lra|apply bpow_ge_0|lra|apply bpow_lt]. }
(* 0 < rx1 *)
assert (Hl1 : ln_beta rx1 = ln_beta x :> Z).
{ now apply ln_beta_DN. }
assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
{ apply ln_beta_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
assert (Hl1 : mag rx1 = mag x :> Z).
{ now apply mag_DN. }
assert (Hl2 : mag rx2c = mag x :> Z).
{ apply mag_unique; rewrite Rabs_right; [|now apply Rle_ge, Rlt_le].
replace rx2c with (rx1 + (/ 2 * bpow ex1 + / 2 * bpow ex2));
[|now rewrite <- Rplus_assoc, Hrx12;
replace (_ + _) with (rx2 + bpow ex2) by field].
......@@ -471,7 +471,7 @@ assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
- rewrite <- Rplus_assoc.
apply Rle_trans with x; [|now apply Hx].
apply Rge_le; rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge, Rlt_le];
apply Rle_ge; destruct (ln_beta x) as (ex,Hex); simpl; apply Hex.
apply Rle_ge; destruct (mag x) as (ex,Hex); simpl; apply Hex.
now apply Rgt_not_eq.
- apply Rlt_le_trans with (rx1 + bpow ex1).
+ apply Rplus_lt_compat_l.
......@@ -482,7 +482,7 @@ assert (Hl2 : ln_beta rx2c = ln_beta x :> Z).
fold (cexp beta fexp1 rx1); rewrite <- ulp_neq_0; try now apply Rgt_not_eq.
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.
* destruct (mag rx1) as (erx1, Herx1); simpl.
rewrite <- (Rabs_right rx1) at 1; [|now apply Rle_ge, Rlt_le].
now apply Herx1, Rgt_not_eq. }
unfold round, F2R, scaled_mantissa, cexp; simpl.
......@@ -515,8 +515,8 @@ Lemma neq_midpoint_beta_odd_aux3 :
forall (choice1 choice2 : Z -> bool),
forall x,
0 < x ->
(fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z ->
(fexp1 (ln_beta x) <= ln_beta x)%Z ->
(fexp2 (mag x) <= fexp1 (mag x))%Z ->
(fexp1 (mag x) <= mag x)%Z ->
x <> midp beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
......@@ -527,7 +527,7 @@ destruct (generic_format_EM beta fexp2 x) as [F2x|NF2x].
now rewrite (round_generic _ fexp2); [|apply valid_rnd_N|]. }
(* ~ generic_format beta fexp2 x *)
assert (NF1x : ~ generic_format beta fexp1 x).
{ now intro H; apply NF2x, (generic_inclusion_ln_beta _ fexp1). }
{ now intro H; apply NF2x, (generic_inclusion_mag _ fexp1). }
destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
- (* x < midp fexp1 x *)
assert (H1' : x < midp beta fexp1 x) by lra.
......@@ -540,12 +540,12 @@ destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
- (* midp fexp1 x < x *)
assert (Hm : midp' beta fexp1 x = midp beta fexp1 x).
{ now unfold midp', midp; rewrite round_UP_DN_ulp; [field|]. }
destruct (Zle_or_lt (fexp1 (ln_beta x)) (fexp2 (ln_beta x))) as [H3|H3].
+ (* fexp2 (ln_beta x) = fexp1 (ln_beta x) *)
assert (H3' : fexp2 (ln_beta x) = fexp1 (ln_beta x));
destruct (Zle_or_lt (fexp1 (mag x)) (fexp2 (mag x))) as [H3|H3].
+ (* fexp2 (mag x) = fexp1 (mag x) *)
assert (H3' : fexp2 (mag x) = fexp1 (mag x));
[now apply Zle_antisym|].
now apply double_round_gt_mid_same_place; [| | |rewrite Hm].
+ (* fexp2 (ln_beta x) < fexp1 (ln_beta x) *)
+ (* fexp2 (mag x) < fexp1 (mag x) *)
destruct (Rlt_or_le (midp beta fexp1 x + / 2 * ulp beta fexp2 x) x)
as [H2|H2].
* (* midp fexp1 x + / 2 * ulp beta fexp2 x < x *)
......@@ -555,25 +555,25 @@ destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
Qed.
(* neq_midpoint_beta_odd_aux3 without the hypothesis
fexp1 (ln_beta x) <= ln_beta x *)
fexp1 (mag x) <= mag x *)
Lemma neq_midpoint_beta_odd :
forall (fexp1 fexp2 : Z -> Z),
Valid_exp fexp1 -> Valid_exp fexp2 ->
forall (choice1 choice2 : Z -> bool),
forall x,
0 < x ->
(fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z ->
(fexp2 (mag x) <= fexp1 (mag x))%Z ->
x <> midp beta fexp1 x ->
double_round_eq beta fexp1 fexp2 choice1 choice2 x.
Proof.
intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hx.
destruct (Zle_or_lt (fexp1 (ln_beta x)) (ln_beta x)) as [H1|H1].
{ (* fexp1 (ln_beta x) <= ln_beta x *)
destruct (Zle_or_lt (fexp1 (mag x)) (mag x)) as [H1|H1].
{ (* fexp1 (mag x) <= mag x *)
now apply neq_midpoint_beta_odd_aux3. }
(* ln_beta x < fexp1 (ln_beta x) *)
(* mag x < fexp1 (mag x) *)
unfold double_round_eq.
revert Hf2f1 Hx H1.
destruct (ln_beta x) as (ex,Hex); simpl.
destruct (mag x) as (ex,Hex); simpl.
specialize (Hex (Rgt_not_eq _ _ Px)).
intros Hf2f1 Hx H1.
rewrite Rabs_right in Hex; [|now apply Rle_ge, Rlt_le].
......@@ -583,7 +583,7 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
replace (fexp1 ex) with (fexp2 ex) in H1; [|now apply Zle_antisym].
rewrite (round_N_really_small_pos _ fexp2 _ x ex Hex H1).
now rewrite round_0; [|apply valid_rnd_N].
- (* fexp2 (ln_beta x) < fexp1 (ln_beta x) *)
- (* fexp2 (mag x) < fexp1 (mag x) *)
set (r2 := round beta fexp2 (Znearest choice2) x).
destruct (Req_dec r2 0) as [Zr2|Nzr2].
{ (* r2 = 0 *)
......@@ -593,13 +593,13 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
[now apply error_le_half_ulp|].
rewrite ulp_neq_0 in B1; try now apply Rgt_not_eq.
unfold round, F2R, scaled_mantissa, cexp; simpl.
apply (Rmult_eq_reg_r (bpow (- fexp1 (ln_beta r2))));
apply (Rmult_eq_reg_r (bpow (- fexp1 (mag r2))));
[|now apply Rgt_not_eq, bpow_gt_0].
rewrite Rmult_0_l; bpow_simplify.
change 0 with (Z2R 0); apply f_equal, Znearest_imp.
simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r.
rewrite Rabs_mult, (Rabs_right (bpow _)); [|now apply Rle_ge, bpow_ge_0].
apply (Rmult_lt_reg_r (bpow (fexp1 (ln_beta r2)))); [now apply bpow_gt_0|].
apply (Rmult_lt_reg_r (bpow (fexp1 (mag r2)))); [now apply bpow_gt_0|].
bpow_simplify.
replace r2 with (r2 - x + x) by ring.
apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)).
......@@ -610,11 +610,11 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
assert (Hbeta : (2 <= beta)%Z).
{ destruct beta as (beta_val,beta_prop).
now apply Zle_bool_imp_le. }
assert (Hex' : ln_beta x = ex :> Z).
{ now apply ln_beta_unique;
assert (Hex' : mag x = ex :> Z).
{ now apply mag_unique;
rewrite Rabs_right; [|apply Rle_ge, Rlt_le]. }
assert (Hl2 : (ln_beta r2 <= fexp1 ex)%Z).
{ apply (ln_beta_le_bpow _ _ _ Nzr2).
assert (Hl2 : (mag r2 <= fexp1 ex)%Z).
{ apply (mag_le_bpow _ _ _ Nzr2).
replace r2 with (r2 - x + x) by ring.
apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)).
apply Rlt_le_trans with (/ 2 * bpow (cexp beta fexp2 x) + bpow ex);
......@@ -633,7 +633,7 @@ destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2].
rewrite Rmult_1_l; bpow_simplify.
simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r.
now change 2 with (Z2R 2); apply Z2R_le. }
assert (Hf1r2 : fexp1 (ln_beta r2) = fexp1 ex).
assert (Hf1r2 : fexp1 (mag r2) = fexp1 ex).
{ now apply (proj2 (Vfexp1 ex)); [omega|]. }
rewrite Hf1r2.
replace (bpow ex) with (/ 2 * (2 * bpow ex)) by field.
......@@ -667,7 +667,7 @@ Proof.
intros mx ex fexp Hmx.
unfold midp; rewrite ulp_neq_0.
unfold round, F2R, scaled_mantissa, cexp; simpl.
set (exf := fexp (ln_beta (Z2R mx * bpow ex))).
set (exf := fexp (mag (Z2R mx * bpow ex))).
set (mxf := Zfloor (Z2R mx * bpow ex * bpow (- exf))).
destruct (Zle_or_lt exf ex) as [Hm|Hm].
- (* exf <= ex *)
......@@ -744,10 +744,10 @@ apply neq_midpoint_beta_odd; try assumption.
- intro Hxy.
revert Fx Fy.
unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))).
set (ex := ln_beta x).
set (ey := ln_beta y).
set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
set (ex := mag x).
set (ey := mag y).
intros Fx Fy.
revert Hxy.
rewrite Fx, Fy.
......@@ -936,10 +936,10 @@ apply neq_midpoint_beta_odd; try assumption.
- intro Hxy.
revert Fx Fy.
unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))).
set (ex := ln_beta x).
set (ey := ln_beta y).
set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
set (ex := mag x).
set (ey := mag y).
intros Fx Fy.
revert Hxy.
rewrite Fx, Fy.
......@@ -1026,10 +1026,10 @@ apply neq_midpoint_beta_odd; try assumption.
- intro Hxy'.
revert Fx Fy.
unfold generic_format, F2R, scaled_mantissa, cexp; simpl.
set (mx := Ztrunc (x * bpow (- fexp1 (ln_beta x)))).
set (my := Ztrunc (y * bpow (- fexp1 (ln_beta y)))).
set (ex := ln_beta x).
set (ey := ln_beta y).
set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))).
set (my := Ztrunc (y * bpow (- fexp1 (mag y)))).
set (ex := mag x).
set (ey := mag y).
intros Fx Fy.
revert Hxy'.
rewrite Fx, Fy.
......@@ -1326,15 +1326,15 @@ revert Fx.
rewrite ulp_neq_0.
2: now apply Rgt_not_eq, sqrt_lt_R0.