Commit b5e185da authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean trailing whitespaces.

parent 356e1d0c
......@@ -78,7 +78,7 @@ apply Zle_trans with (1:=H3).
apply Zle_succ.
Qed.
Lemma FLT_format_half: forall u,
Lemma FLT_format_half: forall u,
format u -> bpow (prec+emin) <= Rabs u -> format (u/2).
Proof with auto with typeclass_instances.
intros u Fu H.
......@@ -108,7 +108,7 @@ now apply IZR_lt.
now apply Zlt_le_weak.
Qed.
Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z ->
Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z ->
round_flt (z/2)= round_flt z /2.
Proof with auto with typeclass_instances.
intros z Hz.
......@@ -252,7 +252,7 @@ apply bpow_le; omega.
Qed.
Lemma round_plus_small_id_aux: forall f h, format f -> (bpow (prec+emin) <= f) -> 0 < f
Lemma round_plus_small_id_aux: forall f h, format f -> (bpow (prec+emin) <= f) -> 0 < f
-> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
Proof with auto with typeclass_instances.
intros f h Ff H1 H2 Hh.
......@@ -309,8 +309,8 @@ 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
assert (T1:(ulp_flt (pred_flt f) = ulp_flt f)
\/ ( ulp_flt (pred_flt f) = /2* ulp_flt f
/\ 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.
......@@ -407,7 +407,7 @@ unfold cexp, FLT_exp.
rewrite Z.max_l.
reflexivity.
omega.
assert (T: (ulp_flt (pred_flt f) = ulp_flt f \/
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 (mag radix2 f - 1) /\
......@@ -583,7 +583,7 @@ rewrite T3.
field.
Qed.
Lemma round_plus_small_id: forall f h, format f -> (bpow (prec+emin) <= Rabs f)
Lemma round_plus_small_id: forall f h, format f -> (bpow (prec+emin) <= Rabs f)
-> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
intros f h Ff H1 H2.
case (Rle_or_lt 0 f); intros V.
......@@ -849,7 +849,7 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
......@@ -1092,7 +1092,7 @@ now apply FLT_format_double.
Qed.
Lemma avg_half_sub_no_underflow_aux_aux: forall z:Z, (0 < z)%Z ->
Lemma avg_half_sub_no_underflow_aux_aux: forall z:Z, (0 < z)%Z ->
(ZnearestE (IZR z / 2) < z)%Z.
Proof.
intros z H1.
......@@ -1186,7 +1186,7 @@ omega.
Qed.
Lemma avg_half_sub_no_underflow_aux2: forall u v, format u -> format v ->
Lemma avg_half_sub_no_underflow_aux2: forall u v, format u -> format v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
u <= v ->
(bpow emin) <= Rabs ((u+v)/2) -> avg_half_sub u v <> 0.
......@@ -1241,7 +1241,7 @@ rewrite <- H1; assumption.
lra.
Qed.
Lemma avg_half_sub_no_underflow_aux3: forall u v, format u -> format v ->
Lemma avg_half_sub_no_underflow_aux3: forall u v, format u -> format v ->
(0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) ->
(bpow emin) <= Rabs ((u+v)/2) -> avg_half_sub u v <> 0.
Proof with auto with typeclass_instances.
......@@ -1266,7 +1266,7 @@ unfold Rdiv; ring.
Qed.
Lemma avg_half_sub_no_underflow:
Lemma avg_half_sub_no_underflow:
(0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) ->
(bpow emin) <= Rabs a -> av <> 0.
Proof with auto with typeclass_instances.
......@@ -1297,7 +1297,7 @@ change (bpow (-(1))) with (/2).
field.
assert (Z.abs (nu+nv) = 1)%Z.
assert (0 < Z.abs (nu+nv) < 2)%Z;[idtac|omega].
split; apply lt_IZR; simpl; rewrite abs_IZR;
split; apply lt_IZR; simpl; rewrite abs_IZR;
apply Rmult_lt_reg_l with (bpow (emin-1)); try apply bpow_gt_0.
rewrite Rmult_0_r.
apply Rlt_le_trans with (1:=H1).
......@@ -1637,7 +1637,7 @@ 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 *)
Lemma avg_half_sub_correct: (0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) ->
Rabs (av-a) <= 3/2 * ulp_flt a.
......@@ -1684,17 +1684,17 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
Definition average (x y : R) :=
Definition average (x y : R) :=
let samesign := match (Rle_bool 0 x), (Rle_bool 0 y) with
true , true => true
| false , false => true
| _,_ => false
end in
if samesign then
if samesign then
match (Rle_bool (Rabs x) (Rabs y)) with
true => avg_half_sub emin prec x y
| false => avg_half_sub emin prec y x
......@@ -1724,11 +1724,11 @@ intros; replace u with v; trivial; auto with real.
intros H1 H2; contradict H1; auto with real.
Qed.
Lemma average_symmetry_Ropp: forall u v, format u -> format v ->
Lemma average_symmetry_Ropp: forall u v, format u -> format v ->
average (-u) (-v) = - average u v.
Proof with auto with typeclass_instances.
(* first: nonnegative u *)
assert (forall u v, 0 <= u -> format u -> format v ->
assert (forall u v, 0 <= u -> format u -> format v ->
average (-u) (-v) = - average u v).
intros u v Hu Fu Fv; unfold average.
rewrite 2!Rabs_Ropp.
......
......@@ -567,7 +567,7 @@ destruct (Rle_or_lt x (midp beta fexp1 x)) as [H1|H1].
as [H2|H2].
* (* midp fexp1 x + / 2 * ulp beta fexp2 x < x *)
now apply round_round_gt_mid_further_place; [| | |omega| |rewrite Hm].
* (* x <= midp fexp1 x + / 2 * ulp beta fexp2 x *)
* (* x <= midp fexp1 x + / 2 * ulp beta fexp2 x *)
now apply neq_midpoint_beta_odd_aux2; [| | | |split].
Qed.
......@@ -1433,7 +1433,7 @@ destruct (Req_dec r 0) as [Zr|Nzr].
apply (Zodd_not_Zeven 1); [now simpl|].
rewrite <- H.
now apply Zeven_mult_Zeven_l. }
(* 0 < r *)
(* 0 < r *)
assert (Pr : 0 < r) by lra.
destruct (Zle_or_lt exx (2 * exsx)) as [H1|H1].
- (* exx <= 2 * exsx *)
......@@ -1842,7 +1842,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
apply Rplus_le_le_0_compat.
+ now apply Rlt_le.
+ apply Rmult_le_pos; [lra|].
apply bpow_ge_0.
apply bpow_ge_0.
- apply (Rmult_lt_reg_r (bpow (mag x))); [now apply bpow_gt_0|].
rewrite Rmult_1_l; bpow_simplify.
apply Rlt_le_trans with (/ 2 * (2 * u)).
......@@ -1900,7 +1900,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
{ rewrite Hlr.
rewrite <- Ztrunc_floor.
- apply generic_format_round; [exact Vfexp1|].
apply valid_rnd_DN.
apply valid_rnd_DN.
- now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]. }
change (bpow (fexp1 _)) with u in Hx2_3.
rewrite <- Xmid' in Hx2_3.
......@@ -2034,7 +2034,7 @@ destruct (Req_dec rd 0) as [Zrd|Nzrd].
apply Rmult_lt_0_compat; [lra|apply bpow_gt_0].
+ rewrite plus_IZR; apply Rplus_le_compat_l; simpl.
unfold u, ulp, cexp; fold f1; bpow_simplify; lra.
Qed.
Qed.
Lemma round_round_eq_mid_beta_odd_rna_aux2 :
forall (fexp1 fexp2 : Z -> Z),
......
......@@ -1117,7 +1117,7 @@ Qed.
Lemma round_flx_sqr_sqrt_snd_deg:
Lemma round_flx_sqr_sqrt_snd_deg:
(((radix_val beta=5)%Z /\ (3 < prec)%Z) \/ (5 < radix_val beta)%Z) ->
sqrt (IZR beta) + / 4 * bpow (3 - prec) <=
IZR beta * (2 - bpow (1 - prec)) / (2 * (2 + bpow (1 - prec))).
......@@ -1821,7 +1821,7 @@ Proof with auto with typeclass_instances.
intros x y Fx.
assert (Y:Valid_exp (FLX_exp prec)).
apply FLX_exp_valid; unfold Prec_gt_0; omega.
assert (H: ((radix_val beta=5)%Z -> (3 < prec)%Z) \/
assert (H: ((radix_val beta=5)%Z -> (3 < prec)%Z) \/
((radix_val beta=5)%Z /\ (prec=3)%Z)).
case (Zle_lt_or_eq 3 prec); omega.
case H; intros H'; clear H.
......
......@@ -98,7 +98,7 @@ apply round_NE_pt...
Qed.
Lemma FLXN_le_exp: forall f1 f2:float beta,
Lemma FLXN_le_exp: forall f1 f2:float beta,
((Zpower beta (prec - 1) <= Zabs (Fnum f1) < Zpower beta prec)%Z) ->
((Zpower beta (prec - 1) <= Zabs (Fnum f2) < Zpower beta prec))%Z ->
0 <= F2R f1 -> F2R f1 <= F2R f2 -> (Fexp f1 <= Fexp f2)%Z.
......@@ -215,8 +215,8 @@ Qed.
Lemma t4_exact_aux: forall (f:float beta) g,
(Z.abs (Fnum f) < Zpower beta prec)%Z
-> (0 <= g <= F2R f)%R
-> (exists n:Z, (g=IZR n*bpow (Fexp f))%R)
-> (0 <= g <= F2R f)%R
-> (exists n:Z, (g=IZR n*bpow (Fexp f))%R)
-> format g.
Proof with auto with typeclass_instances.
intros f g Hf (Hg1,Hg2) (n,Hg3).
......@@ -271,7 +271,7 @@ apply FLXN_format_generic in Fa...
destruct Fa as [fa Hfa1 Hfa2].
apply FLXN_format_generic in Fb...
destruct Fb as [fb Hfb1 Hfb2].
exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc)
exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc)
-Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z.
rewrite Hfa1, Hfb1, Hfc1; unfold F2R; simpl.
rewrite 2!minus_IZR.
......@@ -399,14 +399,14 @@ now apply Rplus_le_le_0_compat.
Qed.
Lemma err_add2: forall x x2 y2 e2, err x2 y2 e2
-> 0 <= e2 -> 0 <= y2 <= x
Lemma err_add2: forall x x2 y2 e2, err x2 y2 e2
-> 0 <= e2 -> 0 <= y2 <= x
-> err (round_flx (x+x2)) (x+y2) (eps*(1+e2)+e2/2).
Proof with auto with typeclass_instances.
intros x x2 y2 e2 H2 H (Y1,Y2).
replace (round_flx (x+x2) - (x+y2)) with ((round_flx (x+x2)-(x+x2))+(x2 - y2)) by ring.
apply Rle_trans with (1:=Rabs_triang _ _).
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_r.
apply Rplus_le_compat.
apply Rle_trans with (eps*Rabs (x+x2)).
apply err_init.
......@@ -415,7 +415,7 @@ apply Rmult_le_compat_l.
apply epsPos.
replace (x+x2) with ((x + y2) +(x2-y2)) by ring.
apply Rle_trans with (1:=Rabs_triang _ _).
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_r.
rewrite Rmult_1_l.
apply Rplus_le_compat_l.
apply Rle_trans with (1:=H2).
......@@ -445,7 +445,7 @@ Qed.
Lemma err_mult: forall x1 y1 e1 x2 y2 e2, err x1 y1 e1 -> err x2 y2 e2
Lemma err_mult: forall x1 y1 e1 x2 y2 e2, err x1 y1 e1 -> err x2 y2 e2
-> err (round_flx (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2)).
Proof with auto with typeclass_instances.
intros x1 y1 e1 x2 y2 e2 H1 H2.
......@@ -513,7 +513,7 @@ Qed.
Lemma sqrt_var_maj_2: forall h : R, Rabs h <= /2 ->
Lemma sqrt_var_maj_2: forall h : R, Rabs h <= /2 ->
Rabs (sqrt (1 + h) - 1) <= Rabs h / 2 + (Rabs h) * (Rabs h) / 4.
Proof.
intros h H1.
......@@ -560,7 +560,7 @@ Qed.
Lemma err_sqrt: forall x y e, 0 <= y -> e <= /2 -> err x y e
Lemma err_sqrt: forall x y e, 0 <= y -> e <= /2 -> err x y e
-> err (round_flx (sqrt x)) (sqrt y) (eps+(1+eps)*(/2*e+/4*e*e)).
Proof with auto with typeclass_instances.
intros x y e Hy He H.
......@@ -828,7 +828,7 @@ left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1; apply Rl
apply sqrt_pos.
Qed.
Lemma Delta_correct_2 : radix_val beta=2%Z ->
Lemma Delta_correct_2 : radix_val beta=2%Z ->
(Rabs (Delta - E_Delta) <= (19/4*eps+33*eps*eps) * E_Delta).
Proof with auto with typeclass_instances.
intros Hradix.
......@@ -1125,8 +1125,8 @@ Qed.
Lemma t4_exact_aux_: forall (f:float beta) g,
(Z.abs (Fnum f) < Zpower beta prec)%Z
-> (0 <= g <= F2R f)%R
-> (exists n:Z, (g=IZR n*bpow (Fexp f))%R)
-> (0 <= g <= F2R f)%R
-> (exists n:Z, (g=IZR n*bpow (Fexp f))%R)
-> (emin <= Fexp f)%Z
-> format g.
Proof with auto with typeclass_instances.
......@@ -1189,8 +1189,8 @@ destruct Fa as [fa Hfa1 Hfa2].
apply generic_format_FLX_FLT in Fb.
apply FLXN_format_generic in Fb...
destruct Fb as [fb Hfb1 Hfb2].
exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc)
-Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z.
exists (Fnum fc -(Fnum fa*Zpower beta (Fexp fa-Fexp fc)
-Fnum fb*Zpower beta (Fexp fb-Fexp fc)))%Z.
rewrite Hfa1, Hfb1, Hfc1; unfold F2R; simpl.
rewrite 2!minus_IZR.
rewrite 2!mult_IZR.
......@@ -1275,7 +1275,7 @@ destruct Fa as [fa Hfa1 Hfa2 Hfa3].
apply FLT_format_generic in Fb...
destruct Fb as [fb Hfb1 Hfb2 Hfb3].
rewrite Hgc2.
exists (Fnum gc -(Fnum fa*Zpower beta (Fexp fa-emin)
exists (Fnum gc -(Fnum fa*Zpower beta (Fexp fa-emin)
-Fnum fb*Zpower beta (Fexp fb -emin)))%Z.
rewrite Hfa1, Hfb1, Hgc1; unfold F2R; simpl.
rewrite Hgc2, 2!minus_IZR.
......@@ -1337,7 +1337,7 @@ Qed.
Notation err x y e := (Rabs (x - y) <= e * Rabs y).
Notation eps :=(/2*bpow (1-prec)).
Lemma err_add_no_err: forall x1 x2,
Lemma err_add_no_err: forall x1 x2,
format x1 -> format x2
-> err (round_flt (x1+x2)) (x1+x2) eps.
Proof with auto with typeclass_instances.
......@@ -1422,15 +1422,15 @@ repeat rewrite Rabs_right; try reflexivity; apply Rle_ge; try assumption.
now apply Rplus_le_le_0_compat.
Qed.
Lemma err_add2_: forall x x2 y2 e2, err x2 y2 e2
Lemma err_add2_: forall x x2 y2 e2, err x2 y2 e2
-> format x -> format x2
-> 0 <= e2 -> 0 <= y2 <= x
-> 0 <= e2 -> 0 <= y2 <= x
-> err (round_flt (x+x2)) (x+y2) (eps*(1+e2)+e2/2).
Proof with auto with typeclass_instances.
intros x x2 y2 e2 H2 Z1 Z2 H (Y1,Y2).
replace (round_flt (x+x2) - (x+y2)) with ((round_flt (x+x2)-(x+x2))+(x2 - y2)) by ring.
apply Rle_trans with (1:=Rabs_triang _ _).
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_r.
apply Rplus_le_compat.
apply Rle_trans with (eps*Rabs (x+x2)).
now apply err_add_no_err.
......@@ -1439,7 +1439,7 @@ apply Rmult_le_compat_l.
apply epsPos.
replace (x+x2) with ((x + y2) +(x2-y2)) by ring.
apply Rle_trans with (1:=Rabs_triang _ _).
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_r.
rewrite Rmult_1_l.
apply Rplus_le_compat_l.
apply Rle_trans with (1:=H2).
......@@ -1463,8 +1463,8 @@ rewrite <- Rmult_assoc, Rinv_r.
rewrite 2!Rabs_pos_eq ; lra.
Qed.
Lemma err_mult_aux: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2
-> err (round_flt (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2))
Lemma err_mult_aux: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2
-> err (round_flt (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2))
\/ (Rabs (round_flt (x1*x2)) <= bpow (emin+prec-1)).
Proof with auto with typeclass_instances.
intros x1 y1 e1 x2 y2 e2 Hx1 Hx2 H1 H2.
......@@ -1525,7 +1525,7 @@ apply Rmult_le_compat; try assumption; apply Rabs_pos.
rewrite Rabs_mult; right; ring.
Qed.
Lemma err_mult_: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2
Lemma err_mult_: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2
-> (bpow (emin+prec-1) < Rabs (round_flt (x1*x2)))
-> err (round_flt (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2)).
Proof.
......@@ -1580,7 +1580,7 @@ Qed.
Lemma err_sqrt_: forall x y e, 0 <= y -> e <= /2 -> err x y e ->
Lemma err_sqrt_: forall x y e, 0 <= y -> e <= /2 -> err x y e ->
bpow (emin+prec-1) < round_flt (sqrt x)
-> err (round_flt (sqrt x)) (sqrt y) (eps+(1+eps)*(/2*e+/4*e*e)).
Proof with auto with typeclass_instances.
......@@ -1688,7 +1688,7 @@ apply Rle_ge, Hy.
Qed.
Lemma subnormal_aux: forall x y, format x -> (Rabs x <= 1 -> Rabs y <= 1) -> bpow (emin+prec-1) < Rabs (round_flt (x*y))
Lemma subnormal_aux: forall x y, format x -> (Rabs x <= 1 -> Rabs y <= 1) -> bpow (emin+prec-1) < Rabs (round_flt (x*y))
-> bpow (emin+prec-1) < Rabs x.
Proof with auto with typeclass_instances.
intros x y Fx H1 H2.
......@@ -1874,7 +1874,7 @@ Qed.
(* argh, would be simpler in radix 2 Delta = /4 * round_flx (sqrt M) *)
Lemma Delta_correct_ :
Lemma Delta_correct_ :
/4 * bpow (Zceil ((IZR (emin+prec-1))/2)) < Delta ->
(Rabs (Delta - E_Delta) <= (23/4*eps+38*eps*eps) * E_Delta).
Proof with auto with typeclass_instances.
......@@ -2024,7 +2024,7 @@ apply sqrt_pos.
Qed.
Lemma Delta_correct_2_ : radix_val beta=2%Z ->
Lemma Delta_correct_2_ : radix_val beta=2%Z ->
bpow (Zceil ((IZR (emin+prec-1))/2) -2) < Delta ->
(Rabs (Delta - E_Delta) <= (19/4*eps+33*eps*eps) * E_Delta).
Proof with auto with typeclass_instances.
......
......@@ -322,7 +322,7 @@ rewrite <- mag_minus1; try assumption.
rewrite <- (mag_abs beta (x+y)).
(* . *)
assert (U:(Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R).
assert (V: forall x y, (Rabs y <= Rabs x)%R ->
assert (V: forall x y, (Rabs y <= Rabs x)%R ->
(Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R).
clear; intros x y.
case (Rle_or_lt 0 y); intros Hy.
......
......@@ -88,7 +88,7 @@ apply generic_format_abs_inv.
rewrite Hxy.
apply generic_format_bpow.
apply valid_exp.
case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2);
case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2);
rewrite H2; now apply mag_generic_gt.
Qed.
......
......@@ -162,7 +162,7 @@ rewrite Zabs2N.id_abs.
now apply Z.abs_neq.
Qed.
Lemma make_bound_p:
Lemma make_bound_p:
Zpos (vNum (make_bound))=(Zpower_nat beta (Zabs_nat p)).
Proof.
unfold make_bound, vNum; simpl.
......@@ -175,7 +175,7 @@ omega.
Qed.
Lemma FtoR_F2R: forall (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g -> Pff.Fexp f = Fexp g ->
Lemma FtoR_F2R: forall (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g -> Pff.Fexp f = Fexp g ->
FtoR beta f = F2R g.
Proof.
intros f g H1 H2; unfold FtoR, F2R.
......@@ -238,7 +238,7 @@ set (ex := cexp beta (FLT_exp (-dExp b) p) x).
set (mx := Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) x)).
intros Hx; repeat split ; simpl.
apply lt_IZR.
rewrite pGivesBound, IZR_Zpower_nat.
rewrite pGivesBound, IZR_Zpower_nat.
apply Rmult_lt_reg_r with (bpow beta ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
......@@ -501,7 +501,7 @@ apply pff_round_NE_is_round.
Qed.
Lemma pff_round_UP_is_round: forall (r:R),
FtoR beta (RND_Max b beta (Z.abs_nat p) r)
FtoR beta (RND_Max b beta (Z.abs_nat p) r)
= round beta (FLT_exp (- dExp b) p) Zceil r.
Proof with auto with typeclass_instances.
intros r.
......@@ -530,7 +530,7 @@ Qed.
Lemma pff_round_DN_is_round: forall (r:R),
FtoR beta (RND_Min b beta (Z.abs_nat p) r)
FtoR beta (RND_Min b beta (Z.abs_nat p) r)
= round beta (FLT_exp (- dExp b) p) Zfloor r.
Proof with auto with typeclass_instances.
intros r.
......@@ -627,7 +627,7 @@ apply pff_round_N_is_round.
Qed.
Lemma pff_round_is_round_N: forall r f, Closest b beta r f ->
exists (choice:Z->bool),
exists (choice:Z->bool),
FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r.
Proof with auto with typeclass_instances.
intros r f Hf.
......
......@@ -77,11 +77,11 @@ destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
(* *)
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f + FtoR radix2 g)).
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f - FtoR radix2 g)).
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
......@@ -211,11 +211,11 @@ destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
(* *)
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
pose (Iplus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f + FtoR radix2 g)).
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
pose (Iminus := fun (f g:Pff.float) => RND_Closest
(make_bound radix2 prec emin) radix2 (Zabs_nat prec) choice
(FtoR radix2 f - FtoR radix2 g)).
assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
clear -prec_gt_0_ precisionNotZero emin_neg; intros x y.
......@@ -379,7 +379,7 @@ assumption.
Qed.
Theorem Veltkamp_Even:
Theorem Veltkamp_Even:
(choice = fun z => negb (Z.even z)) ->
hx = round_flt_s x.
Proof with auto with typeclass_instances.
......@@ -391,25 +391,25 @@ destruct (format_is_pff_format beta (make_bound beta prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(x*(bpow s+1)))
as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(x-p))
as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
(q+p))
as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
(* *)
destruct VeltkampEven with beta (make_bound beta prec emin) (Zabs_nat s)
destruct VeltkampEven with beta (make_bound beta prec emin) (Zabs_nat s)
(Zabs_nat prec) fx fp fq fhx as (hx', (H1,H2)); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
......@@ -424,9 +424,9 @@ rewrite Hfx, Hfp'', <- Hchoice; assumption.
rewrite Hfp'', Hfq'', <- Hchoice; assumption.
(* *)
unfold hx; rewrite Hchoice, <- Hfhx'', <- H1.
apply trans_eq with (FtoR beta (RND_EvenClosest
apply trans_eq with (FtoR beta (RND_EvenClosest
(make_bound beta (prec-s) emin) beta (Zabs_nat (prec-s)) x)).
generalize (EvenClosestUniqueP (make_bound beta (prec-s) emin) beta
generalize (EvenClosestUniqueP (make_bound beta (prec-s) emin) beta
(Zabs_nat (prec-s))); unfold UniqueP; intros T.
apply T with x; clear T.
apply radix_gt_1.
......@@ -485,25 +485,25 @@ destruct (format_is_pff_format beta (make_bound beta prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x*(bpow s+1)))
as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x-p))
as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (q+p))
as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
(* *)
destruct Veltkamp with beta (make_bound beta prec emin) (Zabs_nat s)
destruct Veltkamp with beta (make_bound beta prec emin) (Zabs_nat s)
(Zabs_nat prec) fx fp fq fhx as (H1,(hx', (H2,(H3,H4)))); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
......@@ -558,31 +558,31 @@ destruct (format_is_pff_format beta (make_bound beta prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x*(bpow s+1)))
as (fp,(Hfp, (Hfp',Hfp''))).
rewrite make_bound_Emin in Hfp''; try assumption.
replace (--emin)%Z with emin in Hfp'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x-p))
as (fq,(Hfq, (Hfq',Hfq''))).
rewrite make_bound_Emin in Hfq''; try assumption.
replace (--emin)%Z with emin in Hfq'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (q+p))
as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x-hx))
as (ftx,(Hftx, (Hftx',Hftx''))).
rewrite make_bound_Emin in Hftx''; try assumption.
replace (--emin)%Z with emin in Hftx'' by omega.
(* *)
destruct Veltkamp_tail with beta (make_bound beta prec emin) (Zabs_nat s)
destruct Veltkamp_tail with beta (make_bound beta prec emin) (Zabs_nat s)
(Zabs_nat prec) fx fp fq fhx ftx as (tx', (H1,(H2,(H3,H4)))); try assumption.
apply radix_gt_1.
apply make_bound_p; omega.
......@@ -642,7 +642,7 @@ Lemma underf_mult_aux:
(e <= Pff.Fexp x + Pff.Fexp y)%Z.
Proof.
intros e x y Fx Fy H.
assert (HH: forall z, Fbounded b z
assert (HH: forall z, Fbounded b z
-> Rabs (FtoR beta z) < bpow beta (Pff.Fexp z + prec)).
clear -precisionGt1 pGivesBound; intros z Hz.
unfold FtoR; rewrite <- bpow_powerRZ.
......@@ -793,25 +793,25 @@ destruct (format_is_pff_format_can beta (make_bound beta prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x*(bpow s+1)))
as (fpx,(Hfpx, (Hfpx',Hfpx''))).
rewrite make_bound_Emin in Hfpx''; try assumption.
replace (--emin)%Z with emin in Hfpx'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x-px))
as (fqx,(Hfqx, (Hfqx',Hfqx''))).
rewrite make_bound_Emin in Hfqx''; try assumption.
replace (--emin)%Z with emin in Hfqx'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (qx+px))
as (fhx,(Hfhx, (Hfhx',Hfhx''))).
rewrite make_bound_Emin in Hfhx''; try assumption.
replace (--emin)%Z with emin in Hfhx'' by omega.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (x-hx))
as (ftx,(Hftx, (Hftx',Hftx''))).
rewrite make_bound_Emin in Hftx''; try assumption.
......@@ -823,81 +823,81 @@ destruct (format_is_pff_format_can beta (make_bound beta prec emin)
rewrite make_bound_Emin; try assumption.
replace (--emin)%Z with emin by omega; assumption.
destruct (round_N_is_pff_round beta (make_bound beta prec emin)
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero
choice (y*(bpow s+1)))
as (fpy,(Hfpy, (Hfpy',Hfpy''))).
rewrite make_bound_Emin in Hfpy''; try assumption.
replace (--emin)%Z with emin in Hfpy'' by omega.
destruct (ro