Library Float.FnElem.FArgReduct3
FArgReduct3 file
Sylvie Boldo
This file explains an improvement of Cody & Waite argument
reduction technique using the FMA (fused-multiply-and-add).
Require Export FArgReduct2.
Section Total.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Section Total.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variables prec : nat.
Variable N : Z.
Variables alpha gamma x zH1 u : float.
Variable zL : R.
Various bounds
All the hypotheses
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded b x.
Hypothesis xCanonic : Fcanonic radix b x.
alpha (the constant, such as pi) and gamma (its inverse)
Hypothesis alphaNormal : Fnormal radix b alpha.
Hypothesis gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
Hypothesis
gamma_not_pow_2 : ∀ e : Z, FtoRradix gamma ≠ powerRZ radix e.
Hypothesis gammaDef : Closest bmoinsq radix (/ alpha) gamma.
Hypothesis gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
Hypothesis
gamma_not_pow_2 : ∀ e : Z, FtoRradix gamma ≠ powerRZ radix e.
Hypothesis gammaDef : Closest bmoinsq radix (/ alpha) gamma.
About the computation of z
Hypothesis
uDef :
Closest b radix
(3%nat × powerRZ radix (Zpred (Zpred (prec - N))) + x × alpha) u.
Hypothesis
zH1Def :
Closest b radix (u - 3%nat × powerRZ radix (Zpred (Zpred (prec - N))))
zH1.
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis N_not_too_big : (N ≤ dExp b)%Z.
uDef :
Closest b radix
(3%nat × powerRZ radix (Zpred (Zpred (prec - N))) + x × alpha) u.
Hypothesis
zH1Def :
Closest b radix (u - 3%nat × powerRZ radix (Zpred (Zpred (prec - N))))
zH1.
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis N_not_too_big : (N ≤ dExp b)%Z.
x not too big
Hypothesis
xalpha_small :
(Rabs (x × alpha) ≤
powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
xalpha_small :
(Rabs (x × alpha) ≤
powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
No underflow
A few lemmas
Theorem gamma_ge2: (powerRZ radix (-dExp b+prec -2 +(Zmax 1 (N-1)))≤ gamma)%R.
apply Rle_trans with (2:=gamma_ge).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc;
repeat apply Zplus_le_compat_l; auto with zarith.
fold (Zminus N 1); fold (Zminus N 3).
case (Zle_or_lt 1 (N-1)); intros.
rewrite Zmax_le2; auto.
apply Zle_trans with N; auto with zarith.
rewrite Zmax_le1; auto with zarith.
Qed.
Theorem exp_gamma_enough2: (- dExp b ≤ Zpred (Zpred (Fexp gamma)))%Z.
assert (- dExp b + prec-1 < prec-2 + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec + Zmax (-1) N)%Z; auto with zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc;
repeat apply Zplus_le_compat_l; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=gamma_ge).
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum gamma)); auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum (bmoinsq))).
elim gammaNormal; intros I1 I2; elim I1; intros; auto with zarith real.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
unfold radix; replace (Z_of_nat ((prec-2)%nat)) with (prec-2)%Z; auto with zarith real.
replace 2%Z with (Z_of_nat 2); auto with zarith.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.
Theorem exp_alpha_le: (- dExp b ≤ 3 + - (Fexp alpha + (prec + prec)))%Z.
assert (prec-1+Fexp alpha ≤ dExp b+2-prec)%Z; unfold Zsucc; auto with zarith.
apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with alpha.
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith.
elim alphaNormal; intros.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (Zpos (vNum b)).
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
right; unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (2×1)%R; field; auto with real.
apply Rle_trans with ( Zabs (radix × Fnum alpha)); auto with real zarith.
rewrite Zabs_eq; auto with real zarith.
rewrite mult_IZR; auto with real.
assert (0 < Fnum alpha)%Z; auto with zarith real float.
apply LtR0Fnum with radix; auto with real zarith.
case (Rle_or_lt alpha (powerRZ radix (dExp b + 2 - prec))); auto with real.
intros V.
absurd (powerRZ radix (- dExp b + prec - 1) ≤ gamma)%R.
apply Rlt_not_le.
assert (∃ f:float, Fbounded bmoinsq f ∧
(FtoRradix f= powerRZ radix (- dExp b+prec-2))%R).
∃ (Float 1 (-dExp b+prec-2)).
split;[split|idtac].
apply Zle_lt_trans with (Zabs 1); auto with zarith.
rewrite Zabs_eq; auto with zarith.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq; auto with zarith.
apply Zle_lt_trans with (Zpower_nat 2 0); auto with zarith.
simpl; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
elim H; intros f H'; elim H'; intros I1 I2; clear H H'.
apply Rle_lt_trans with (FtoRradix f).
unfold FtoRradix; apply RleBoundRoundr with bmoinsq (prec-2)
(Closest bmoinsq radix) (/alpha)%R; auto with real zarith float.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
apply ClosestRoundedModeP with (prec-2); auto with zarith.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
fold FtoRradix; rewrite I2.
apply Rle_trans with (/(powerRZ radix (dExp b + 2 - prec)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (dExp b + 2 - prec))%Z with (- dExp b + prec - 2)%Z; auto with real zarith.
rewrite I2; auto with real zarith.
apply Rle_trans with (2:=gamma_ge).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc.
repeat apply Zplus_le_compat_l; auto with zarith.
Qed.
Theorem exp_gamma_enough3: (- dExp b ≤ Fexp gamma - N-3)%Z.
assert (- dExp b + prec +N< prec-2 + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec + Zmax (-1) N)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=gamma_ge).
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum gamma)); auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum (bmoinsq))).
elim gammaNormal; intros I1 I2; elim I1; intros; auto with zarith real.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
unfold radix; replace (Z_of_nat ((prec-2)%nat)) with (prec-2)%Z; auto with zarith real.
replace 2%Z with (Z_of_nat 2); auto with zarith.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.
Theorem gamma_p:
ex (fun gam2 : float ⇒ FtoRradix gam2 = gamma ∧ Fnormal radix b gam2 ∧ (Fexp gam2=Zpred (Zpred (Fexp gamma))) ∧
((powerRZ radix (Zpred prec))+4 ≤Fnum gam2)%R ∧ (Fnum gam2 ≤ (powerRZ radix prec)-4)%R).
assert (0 < (Fnum gamma))%Z;[apply LtR0Fnum with radix ;auto with real zarith|idtac].
∃ (Float ((Fnum gamma)*radix×radix)%Z (Zpred (Zpred (Fexp gamma)))).
split.
unfold FtoRradix, FtoR;simpl.
pattern (Fexp gamma)%Z at 2; replace (Fexp gamma)%Z with (2+(Zpred (Zpred (Fexp gamma))))%Z;
[idtac|unfold Zpred;ring].
rewrite mult_IZR;rewrite mult_IZR.
rewrite powerRZ_add; auto with real zarith; simpl;ring.
cut ((powerRZ radix (Zpred prec))+4 ≤ (Fnum gamma × radix × radix)%Z)%R;[intros V1|idtac].
cut ((Fnum gamma × radix × radix)%Z ≤ (powerRZ radix prec)-4)%R;[intros V2|idtac].
split;[idtac|split;auto].
split;[split|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; apply Rle_lt_trans with (powerRZ radix prec - 4)%R;auto with real.
rewrite Zabs_eq; auto with real zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R;[unfold Rminus; apply Rplus_lt_compat_l|right;ring].
apply Ropp_lt_contravar;apply Rlt_le_trans with 1%R;auto with real;apply Rle_trans with 2%R;auto with real.
simpl;auto with zarith.
apply exp_gamma_enough2.
apply Zle_Rle;rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
rewrite Zabs_eq; auto with zarith.
apply Rle_trans with (radix*( (powerRZ radix (Zpred prec) + 4)))%R;auto with real zarith.
apply Rle_trans with (radix × (powerRZ radix (Zpred prec)))%R;[idtac|apply Rmult_le_compat_l;auto with real zarith].
right; unfold Zpred; rewrite powerRZ_add; auto with real zarith;simpl; field.
apply Rle_trans with (powerRZ radix (Zpred prec) + 0)%R;[right;ring| apply Rplus_le_compat_l].
apply Rle_trans with 1%R; auto with real.
apply Rle_trans with 2%R; auto with real.
rewrite mult_IZR; apply Rmult_le_compat_l;auto with real zarith.
apply Zle_trans with (radix× (Fnum gamma × radix × radix))%Z;auto with zarith.
rewrite mult_IZR;rewrite mult_IZR.
apply Rle_trans with ((powerRZ radix (Zminus prec 2)- 1)*radix×radix)%R.
apply Rmult_le_compat_r;auto with real zarith.
apply Rmult_le_compat_r;auto with real zarith.
rewrite <- (Zabs_eq (Fnum gamma)); auto with zarith.
apply Rle_trans with (Zpred (Zpos (vNum bmoinsq))).
cut ((Zabs (Fnum gamma) < (Zpos (vNum bmoinsq))))%Z;auto with zarith real float.
elim gammaNormal; auto with zarith float.
unfold bmoinsq;rewrite vNum_eq_Zpower_bmoinsq; unfold Zpred;simpl.
rewrite plus_IZR;rewrite Zpower_nat_Z_powerRZ;right.
rewrite <- minus_Zminus_precq with prec 2;auto with zarith real.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; right;field.
apply Rle_trans with (radix*((powerRZ radix (Zpred (Zpred prec)) + 2)))%R.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with zarith real; simpl; field; auto with real.
apply Rle_trans with ((radix × (Zpower_nat radix (pred (pred prec)) + 2)))%Z.
rewrite <- inj_pred;auto with zarith;rewrite <- inj_pred;auto with zarith.
rewrite mult_IZR;rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ;auto with real zarith.
apply Rle_IZR.
apply Zle_trans with (radix × (radix × (Fnum gamma)))%Z;[idtac|apply Zeq_le;ring].
apply Zmult_le_compat_l;auto with zarith.
apply Zle_trans with (radix*(Zsucc (Zpower_nat radix (pred (pred (pred prec))))))%Z.
pattern (pred (pred prec)) at 1;replace (pred (pred prec)) with (1+(pred (pred (pred prec))))%nat.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat radix 1)%Z with radix;[unfold Zsucc, radix; apply Zeq_le; ring|unfold Zpower_nat;simpl;auto with zarith].
auto with zarith.
apply Zmult_le_compat_l;auto with zarith.
apply Zlt_le_succ.
cut ((Zpower_nat radix (pred (pred (pred prec))) ≤ Fnum gamma)%Z);[intros H2|idtac].
cut (~((Zpower_nat radix (pred (pred (pred prec))) = Fnum gamma)%Z));[intros H3;auto with zarith|idtac].
Contradict gamma_not_pow_2.
apply
ex_not_not_all
with
(U := Z)
(P := fun t : Z ⇒ FtoRradix gamma ≠ powerRZ radix t).
∃ ((Fexp gamma)+(pred (pred (pred prec))))%Z.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
rewrite <- gamma_not_pow_2; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt;auto with zarith.
apply Zle_trans with (Zpos (vNum bmoinsq)).
apply Zeq_le;unfold bmoinsq;rewrite vNum_eq_Zpower_bmoinsq.
replace (prec-2)%nat with (1 + (pred (pred (pred prec))))%nat.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat 2 1)%Z with radix;[unfold radix;ring|unfold Zpower_nat;simpl;auto with zarith].
auto with zarith.
rewrite <- (Zabs_eq ( Fnum gamma × radix)%Z);auto with zarith.
elim gammaNormal; rewrite Zmult_comm; auto with zarith.
Qed.
apply Rle_trans with (2:=gamma_ge).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc;
repeat apply Zplus_le_compat_l; auto with zarith.
fold (Zminus N 1); fold (Zminus N 3).
case (Zle_or_lt 1 (N-1)); intros.
rewrite Zmax_le2; auto.
apply Zle_trans with N; auto with zarith.
rewrite Zmax_le1; auto with zarith.
Qed.
Theorem exp_gamma_enough2: (- dExp b ≤ Zpred (Zpred (Fexp gamma)))%Z.
assert (- dExp b + prec-1 < prec-2 + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec + Zmax (-1) N)%Z; auto with zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc;
repeat apply Zplus_le_compat_l; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=gamma_ge).
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum gamma)); auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum (bmoinsq))).
elim gammaNormal; intros I1 I2; elim I1; intros; auto with zarith real.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
unfold radix; replace (Z_of_nat ((prec-2)%nat)) with (prec-2)%Z; auto with zarith real.
replace 2%Z with (Z_of_nat 2); auto with zarith.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.
Theorem exp_alpha_le: (- dExp b ≤ 3 + - (Fexp alpha + (prec + prec)))%Z.
assert (prec-1+Fexp alpha ≤ dExp b+2-prec)%Z; unfold Zsucc; auto with zarith.
apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with alpha.
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith.
elim alphaNormal; intros.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (Zpos (vNum b)).
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
right; unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (2×1)%R; field; auto with real.
apply Rle_trans with ( Zabs (radix × Fnum alpha)); auto with real zarith.
rewrite Zabs_eq; auto with real zarith.
rewrite mult_IZR; auto with real.
assert (0 < Fnum alpha)%Z; auto with zarith real float.
apply LtR0Fnum with radix; auto with real zarith.
case (Rle_or_lt alpha (powerRZ radix (dExp b + 2 - prec))); auto with real.
intros V.
absurd (powerRZ radix (- dExp b + prec - 1) ≤ gamma)%R.
apply Rlt_not_le.
assert (∃ f:float, Fbounded bmoinsq f ∧
(FtoRradix f= powerRZ radix (- dExp b+prec-2))%R).
∃ (Float 1 (-dExp b+prec-2)).
split;[split|idtac].
apply Zle_lt_trans with (Zabs 1); auto with zarith.
rewrite Zabs_eq; auto with zarith.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq; auto with zarith.
apply Zle_lt_trans with (Zpower_nat 2 0); auto with zarith.
simpl; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
elim H; intros f H'; elim H'; intros I1 I2; clear H H'.
apply Rle_lt_trans with (FtoRradix f).
unfold FtoRradix; apply RleBoundRoundr with bmoinsq (prec-2)
(Closest bmoinsq radix) (/alpha)%R; auto with real zarith float.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
apply ClosestRoundedModeP with (prec-2); auto with zarith.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
fold FtoRradix; rewrite I2.
apply Rle_trans with (/(powerRZ radix (dExp b + 2 - prec)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (dExp b + 2 - prec))%Z with (- dExp b + prec - 2)%Z; auto with real zarith.
rewrite I2; auto with real zarith.
apply Rle_trans with (2:=gamma_ge).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite <- Zplus_assoc.
repeat apply Zplus_le_compat_l; auto with zarith.
Qed.
Theorem exp_gamma_enough3: (- dExp b ≤ Fexp gamma - N-3)%Z.
assert (- dExp b + prec +N< prec-2 + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec + Zmax (-1) N)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=gamma_ge).
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum gamma)); auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum (bmoinsq))).
elim gammaNormal; intros I1 I2; elim I1; intros; auto with zarith real.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
unfold radix; replace (Z_of_nat ((prec-2)%nat)) with (prec-2)%Z; auto with zarith real.
replace 2%Z with (Z_of_nat 2); auto with zarith.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.
Theorem gamma_p:
ex (fun gam2 : float ⇒ FtoRradix gam2 = gamma ∧ Fnormal radix b gam2 ∧ (Fexp gam2=Zpred (Zpred (Fexp gamma))) ∧
((powerRZ radix (Zpred prec))+4 ≤Fnum gam2)%R ∧ (Fnum gam2 ≤ (powerRZ radix prec)-4)%R).
assert (0 < (Fnum gamma))%Z;[apply LtR0Fnum with radix ;auto with real zarith|idtac].
∃ (Float ((Fnum gamma)*radix×radix)%Z (Zpred (Zpred (Fexp gamma)))).
split.
unfold FtoRradix, FtoR;simpl.
pattern (Fexp gamma)%Z at 2; replace (Fexp gamma)%Z with (2+(Zpred (Zpred (Fexp gamma))))%Z;
[idtac|unfold Zpred;ring].
rewrite mult_IZR;rewrite mult_IZR.
rewrite powerRZ_add; auto with real zarith; simpl;ring.
cut ((powerRZ radix (Zpred prec))+4 ≤ (Fnum gamma × radix × radix)%Z)%R;[intros V1|idtac].
cut ((Fnum gamma × radix × radix)%Z ≤ (powerRZ radix prec)-4)%R;[intros V2|idtac].
split;[idtac|split;auto].
split;[split|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; apply Rle_lt_trans with (powerRZ radix prec - 4)%R;auto with real.
rewrite Zabs_eq; auto with real zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R;[unfold Rminus; apply Rplus_lt_compat_l|right;ring].
apply Ropp_lt_contravar;apply Rlt_le_trans with 1%R;auto with real;apply Rle_trans with 2%R;auto with real.
simpl;auto with zarith.
apply exp_gamma_enough2.
apply Zle_Rle;rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
rewrite Zabs_eq; auto with zarith.
apply Rle_trans with (radix*( (powerRZ radix (Zpred prec) + 4)))%R;auto with real zarith.
apply Rle_trans with (radix × (powerRZ radix (Zpred prec)))%R;[idtac|apply Rmult_le_compat_l;auto with real zarith].
right; unfold Zpred; rewrite powerRZ_add; auto with real zarith;simpl; field.
apply Rle_trans with (powerRZ radix (Zpred prec) + 0)%R;[right;ring| apply Rplus_le_compat_l].
apply Rle_trans with 1%R; auto with real.
apply Rle_trans with 2%R; auto with real.
rewrite mult_IZR; apply Rmult_le_compat_l;auto with real zarith.
apply Zle_trans with (radix× (Fnum gamma × radix × radix))%Z;auto with zarith.
rewrite mult_IZR;rewrite mult_IZR.
apply Rle_trans with ((powerRZ radix (Zminus prec 2)- 1)*radix×radix)%R.
apply Rmult_le_compat_r;auto with real zarith.
apply Rmult_le_compat_r;auto with real zarith.
rewrite <- (Zabs_eq (Fnum gamma)); auto with zarith.
apply Rle_trans with (Zpred (Zpos (vNum bmoinsq))).
cut ((Zabs (Fnum gamma) < (Zpos (vNum bmoinsq))))%Z;auto with zarith real float.
elim gammaNormal; auto with zarith float.
unfold bmoinsq;rewrite vNum_eq_Zpower_bmoinsq; unfold Zpred;simpl.
rewrite plus_IZR;rewrite Zpower_nat_Z_powerRZ;right.
rewrite <- minus_Zminus_precq with prec 2;auto with zarith real.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; right;field.
apply Rle_trans with (radix*((powerRZ radix (Zpred (Zpred prec)) + 2)))%R.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with zarith real; simpl; field; auto with real.
apply Rle_trans with ((radix × (Zpower_nat radix (pred (pred prec)) + 2)))%Z.
rewrite <- inj_pred;auto with zarith;rewrite <- inj_pred;auto with zarith.
rewrite mult_IZR;rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ;auto with real zarith.
apply Rle_IZR.
apply Zle_trans with (radix × (radix × (Fnum gamma)))%Z;[idtac|apply Zeq_le;ring].
apply Zmult_le_compat_l;auto with zarith.
apply Zle_trans with (radix*(Zsucc (Zpower_nat radix (pred (pred (pred prec))))))%Z.
pattern (pred (pred prec)) at 1;replace (pred (pred prec)) with (1+(pred (pred (pred prec))))%nat.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat radix 1)%Z with radix;[unfold Zsucc, radix; apply Zeq_le; ring|unfold Zpower_nat;simpl;auto with zarith].
auto with zarith.
apply Zmult_le_compat_l;auto with zarith.
apply Zlt_le_succ.
cut ((Zpower_nat radix (pred (pred (pred prec))) ≤ Fnum gamma)%Z);[intros H2|idtac].
cut (~((Zpower_nat radix (pred (pred (pred prec))) = Fnum gamma)%Z));[intros H3;auto with zarith|idtac].
Contradict gamma_not_pow_2.
apply
ex_not_not_all
with
(U := Z)
(P := fun t : Z ⇒ FtoRradix gamma ≠ powerRZ radix t).
∃ ((Fexp gamma)+(pred (pred (pred prec))))%Z.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
rewrite <- gamma_not_pow_2; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt;auto with zarith.
apply Zle_trans with (Zpos (vNum bmoinsq)).
apply Zeq_le;unfold bmoinsq;rewrite vNum_eq_Zpower_bmoinsq.
replace (prec-2)%nat with (1 + (pred (pred (pred prec))))%nat.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat 2 1)%Z with radix;[unfold radix;ring|unfold Zpower_nat;simpl;auto with zarith].
auto with zarith.
rewrite <- (Zabs_eq ( Fnum gamma × radix)%Z);auto with zarith.
elim gammaNormal; rewrite Zmult_comm; auto with zarith.
Qed.
Main result: q=2
Theorem Fmac_arg_reduct_correct3 :
ex (fun u : float ⇒ FtoRradix u = (x - zH1 × gamma)%R ∧ Fbounded b u)
∧ (Rabs (x-zH1×gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
case (Req_dec zH1 0); intros H1.
split.
∃ x; split; auto with real.
rewrite H1; ring.
replace (x-zH1×gamma)%R with (FtoRradix x);[idtac|rewrite H1; ring].
apply Rmult_lt_reg_l with alpha; auto.
apply Rle_lt_trans with (Rabs (x×alpha-zH1)).
right; replace (x×alpha-zH1)%R with (x×alpha)%R; auto with real.
rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real.
rewrite H1; ring.
apply Rle_lt_trans with (powerRZ radix (Zpred (-N))).
replace (x×alpha-zH1)%R with
((S 2 × powerRZ radix (Zpred (Zpred (prec - N))) + x × alpha)-u)%R.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
unfold Fulp,radix; rewrite Fexp_u with b prec N alpha x u; auto with zarith.
unfold Zpred; rewrite powerRZ_add; auto with real zarith; right.
simpl; field; auto with real.
unfold FtoRradix, radix;rewrite zH1_eq with b prec N alpha x u zH1; auto with real zarith.
ring.
replace (Zpred (-N)) with ((-Fexp gamma-1-prec)+(prec-N+Fexp gamma))%Z;
[idtac|unfold Zpred; ring].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
replace (- Fexp gamma - 1 - prec)%Z with
((-4+prec) +Fexp alpha)%Z.
apply Rlt_le_trans with (Zpos (vNum b) × (Float (S 0) (Zpred (Fexp alpha))))%R.
apply Rlt_le_trans with (powerRZ radix (prec+Fexp alpha-1)); auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
unfold FtoRradix, FtoR; simpl; right.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; ring.
apply Rle_trans with (Fabs alpha).
unfold FtoRradix; apply FnormalBoundAbs2 with prec; auto with zarith.
unfold FtoRradix; rewrite Fabs_correct; auto with zarith;
rewrite Rabs_right; try apply Rle_ge; auto with zarith real.
rewrite gamma_exp with b prec 2 alpha gamma; auto with zarith.
replace (Zsucc (S 1)) with 3%Z; ring; simpl; ring.
apply Zle_trans with (1:=exp_alpha_le).
replace (Zsucc (S 1)) with 3%Z; auto with zarith.
case (Rle_or_lt (powerRZ radix (2 - Zsucc N)) (Rabs zH1)); intros H'.
cut
(∃ k : Z,
(∃ zH : float,
FtoR 2 zH1 = FtoR 2 zH ∧
(Zsucc (k + N) ≤ Zpred (Zpred prec))%Z ∧
(0 ≤ Zsucc (k + N))%Z ∧
1 < Zabs_nat (Zsucc (k + N)) ∧
N = (- Fexp zH)%Z ∧
Fnormal 2
((fun k0 : Z ⇒
Bound
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat 2 (Zabs_nat (Zsucc (k0 + N)))))))
(dExp b)) k) zH ∧
(Rabs (FtoR 2 x × FtoR 2 alpha - FtoR 2 zH) ≤
powerRZ 2%Z (Zpred (- N)))%R ∧
(powerRZ 2%Z k ≤ (Rabs (FtoR 2 zH1)) < powerRZ 2%Z (Zsucc k))%R)).
2: apply arg_reduct_exists_k_zH with u; auto with real zarith.
fold radix FtoRradix in |- ×.
intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H3 T4;
elim T4; intros H4 T5; elim T5; intros H5 T6; elim T6;
intros H6 T7; elim T7; intros H7 T8; elim T8; intros H8 T9;
elim T9; intros H9 T10; elim T10; intros H10 H11;
clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10.
rewrite H3.
apply Fmac_arg_reduct_correct1 with 2 k alpha (x × alpha - zH)%R;
auto with zarith real arith.
apply Zplus_le_reg_l with (- Zsucc N)%Z.
replace (- Zsucc N + 2)%Z with (2 - Zsucc N)%Z; [ idtac | ring ];
replace (- Zsucc N + Zsucc (k + N))%Z with k;
[ idtac | unfold Zsucc in |- *; ring ].
apply Zgt_succ_le; apply Zlt_gt.
apply Zlt_powerRZ with radix; auto with zarith real;
apply Rle_lt_trans with (1 := H'); auto.
apply Zplus_le_reg_l with (- Zsucc N)%Z.
replace (- Zsucc N + 2%nat)%Z with (2 - Zsucc N)%Z; [ idtac | ring ];
replace (- Zsucc N + Zsucc (k + N))%Z with k;
[ idtac | unfold Zsucc in |- *; ring ].
apply Zgt_succ_le; apply Zlt_gt.
apply Zlt_powerRZ with radix; auto with zarith real;
apply Rle_lt_trans with (1 := H'); auto.
apply gamma_ge2.
cut (zH1 = Float
(Fnum (Fnormalize radix b prec u) -
3%nat × Zpower_nat radix (pred (pred prec))) (
- N) :>R); [ intros H'1 | idtac ].
2:unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with zarith.
2:rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;
unfold FtoR in |- ×.
2:apply
trans_eq
with
((Fnum (Fnormalize 2 b prec u) - 3%nat × Zpower_nat 2 (pred (pred prec)))%Z ×
powerRZ 2%Z (- N))%R; [ idtac | simpl in |- *; auto with zarith real ].
2:unfold Zminus in |- *; rewrite plus_IZR; rewrite Ropp_Ropp_IZR;
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
2:rewrite Fexp_u with b prec N alpha x u; auto with zarith.
2: replace (Zpred (Zpred (prec + - N))) with (- N + pred (pred prec))%Z.
2: rewrite powerRZ_add; auto with real zarith; simpl; ring.
2: rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith;
unfold Zpred; ring.
cut
(∃ zH : float,
FtoRradix zH1 = zH ∧
Fexp zH = (- N)%Z ∧ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R ∧ (0 < Rabs zH)%R).
2:∃
(Float
(Fnum (Fnormalize radix b prec u) -
3%nat × Zpower_nat radix (pred (pred prec))) (
- N)).
2:split; [ auto | idtac ].
2:split; [ simpl in |- *; auto | idtac ].
2:split.
2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
2:apply Rle_lt_trans with (Rabs (FtoRradix zH1)).
2: right; rewrite H'1; unfold FtoRradix, FtoR; simpl.
2: rewrite Rabs_mult; rewrite Rabs_Zabs.
2: rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
2:rewrite <- powerRZ_add; auto with real zarith.
2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
unfold Zsucc, Zpred in |- *; ring.
2:rewrite <- H'1; cut (0 ≤ Rabs zH1)%R; auto with real.
2:intros H''; case H''; auto with real; intros H2.
2:absurd (Rabs zH1=0); auto with real.
2: apply Rabs_no_R0; auto.
intros V; elim V; intros zH V1; elim V1; intros H2 V2; elim V2; intros H3 V3;
elim V3; intros H4 H5; clear V V1 V2 V3.
cut (Zabs (Fnum zH)=1)%Z;[intros H6|idtac].
2: cut (0 < (Zabs (Fnum zH)))%Z;[intros H'3|
apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
apply LtR0Fnum with radix];auto with real zarith.
2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4|idtac];auto with real zarith.
2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
2: rewrite Fabs_correct; auto with real zarith.
cut ((((powerRZ radix (Zpred (-N))) ≤ (Rabs x)*alpha)%R) ∧ (((Rabs x)*alpha ≤3*(powerRZ radix (Zpred (-N))))%R)).
intros T;elim T; intros W1 W2;clear T.
case (Rle_or_lt (/2%nat*(Rabs (Fmult zH gamma))) (Rabs x));intros H7.
assert (Fbounded b (Fminus 2 x (Fmult zH gamma)) ∧
(Rabs (x - (Fmult zH gamma))
≤ Rabs (Fmult zH gamma))%R).
unfold FtoRradix; apply Sterbenzter; auto with zarith.
split; simpl in |- *;auto with zarith.
rewrite Zabs_Zmult; rewrite H6.
apply Zle_lt_trans with (Zabs (Fnum gamma)); auto with zarith.
apply Zlt_trans with (Zpos (vNum bmoinsq)).
elim gammaNormal;intros W;elim W;auto.
rewrite pGivesBound;unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq;auto with zarith.
apply Zle_trans with (1:=exp_gamma_enough3); auto with zarith.
fold FtoRradix; apply Rmult_le_reg_l with alpha;auto with real.
rewrite Rmult_comm;apply Rle_trans with (1:=W2).
apply Rle_trans with (((alpha×gamma)*4)*(powerRZ radix (Zpred (-N))))%R.
apply Rmult_le_compat_r;auto with real zarith.
apply Rle_trans with ((1-(powerRZ radix (2-prec)))*4)%R.
apply Rplus_le_reg_l with (-3+4*(powerRZ radix (2 - prec)))%R.
apply Rle_trans with (4*(powerRZ radix (2 - prec)))%R;[right;ring|idtac].
apply Rle_trans with (powerRZ radix (2+(2 - prec)));[right;rewrite powerRZ_add;auto with real zarith;simpl;ring|idtac].
apply Rle_trans with (powerRZ radix 0)%R;[idtac|simpl;right;ring].
apply Rle_powerRZ;auto with real zarith.
apply Rmult_le_compat_r;auto with real.
apply Rle_trans with 1%R;auto with real.
apply Rle_trans with 2%R;auto with real.
apply Rplus_le_reg_l with ((powerRZ radix (2 - prec))- alpha × gamma)%R.
apply Rle_trans with (1-alpha×gamma)%R;[right;ring|idtac].
apply Rle_trans with (powerRZ radix (2 - prec));[idtac|right;ring].
apply Rle_trans with (Rabs (1 - FtoR 2 alpha × FtoR 2 gamma)).
fold radix FtoRradix; apply RRle_abs.
replace (2-prec)%Z with (2%nat-prec)%Z;auto with zarith.
apply delta_inf with b;auto with zarith.
apply exp_alpha_le.
rewrite Fmult_correct; auto with zarith; rewrite Rabs_mult.
replace (Rabs (FtoR 2 zH) ) with (powerRZ radix (-N)).
rewrite Rabs_right.
unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith.
fold radix; fold FtoRradix; simpl; right; field; auto with real.
apply Rle_ge; auto with real.
rewrite <- Fabs_correct; auto with zarith;unfold FtoR, Fabs; simpl.
rewrite H6; rewrite H3; simpl; ring.
rewrite Fmult_correct; auto with zarith; fold radix; fold FtoRradix.
cut (0 ≤ x×zH)%R.
intros; rewrite <- Rmult_assoc; apply Rle_trans with (0×gamma)%R; auto with real.
case (Rle_or_lt 0 x); intros.
assert (0 ≤ zH)%R.
rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
apply Rle_trans with (0×zH)%R; auto with real.
assert (zH ≤ 0)%R.
rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith real.
apply Rle_trans with ((-x)*(-zH))%R; auto with real.
apply Rmult_le_pos; auto with real.
elim H; intros; split.
∃ (Fminus radix x (Fmult zH gamma));split; auto.
rewrite H2; unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite Fmult_correct; auto with zarith real.
replace (zH1 × gamma)%R with (FtoRradix (Fmult zH gamma)).
apply Rle_lt_trans with (1:=H8).
unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
rewrite Rabs_mult.
replace (prec-N+Fexp gamma)%Z with (-N+(prec+Fexp gamma))%Z;
[rewrite powerRZ_add; auto with real zarith|ring].
replace (Rabs (FtoR radix zH)) with (powerRZ radix (- N)).
apply Rmult_lt_compat_l; auto with real zarith.
rewrite <- Fabs_correct; auto with zarith; unfold FtoR, Fabs; simpl.
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
elim gammaNormal; intros T1 T2; elim T1; intros.
apply Rlt_le_trans with (Zpos (vNum bmoinsq)); auto with real zarith.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq;
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite <- Fabs_correct; auto with zarith; unfold FtoR, Fabs; simpl.
rewrite H3; rewrite H6; simpl; ring.
rewrite H2; unfold FtoRradix; rewrite Fmult_correct; auto with real zarith.
generalize gamma_p; intros T1; elim T1; intros gam2 T2;elim T2; intros W3 T3;elim T3; intros W4 T4;
elim T4; intros W5 T5; elim T5; intros W6 W7; clear T1 T2 T3 T4 T5.
rewrite H2; rewrite <- W3.
cut (0 < (1 + powerRZ radix (2 - prec)))%R;[intros W8|idtac].
2: apply Rlt_trans with 1%R; auto with real zarith.
2: apply Rle_lt_trans with (1+0)%R; auto with real zarith.
cut ((powerRZ radix (Zpred (-N)))*gamma/(1+(powerRZ radix (Zminus 2 prec))) ≤ Rabs x)%R;[intros H9|idtac].
cut ((Fexp x)=(Fexp gam2)-N-1)%Z;[intros H8|idtac].
assert (Rabs (x - zH × gam2) < powerRZ radix (Fexp gam2 - N - 1) × Zpos (vNum b))%R.
apply Rle_lt_trans with (- Rabs x+Rabs zH×gam2)%R.
assert (∀ (r1 r2:R), ((0 ≤ r1)%R → (0 ≤ r2)%R)
→ ((r1≤0)%R → (r2 ≤ 0)%R) → (Rabs r1 ≤ Rabs r2)%R
→ (Rabs (r1-r2) = - Rabs r1 + Rabs r2)%R).
intros r1 r2 L1 L2; case (Rle_or_lt 0 r1); intros L3.
rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
intros; rewrite Rabs_left1; auto with real.
ring.
apply Rplus_le_reg_l with r2; ring_simplify; auto with real.
rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
intros; rewrite Rabs_right; auto with real.
ring.
apply Rle_ge; apply Rplus_le_reg_l with (-r1)%R; ring_simplify; auto with real.
rewrite H; auto.
rewrite Rabs_mult; rewrite (Rabs_right gam2); auto with real.
apply Rle_ge; rewrite W3; auto with real.
intros; assert (0 ≤ zH)%R.
rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
apply Rmult_le_pos; auto with real.
rewrite W3; auto with real.
intros; assert (zH ≤ 0)%R.
rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith.
assert (0 < gam2)%R;[rewrite W3|idtac]; auto with real.
apply Rle_trans with (0×gam2)%R; auto with real.
apply Rlt_le; apply Rlt_le_trans with (1:=H7).
apply Rle_trans with (1×Rabs (Fmult zH gamma))%R.
apply Rmult_le_compat_r; auto with real zarith.
simpl; apply Rmult_le_reg_l with 2%R; auto with real;apply Rle_trans with 1%R;[right;field|idtac];auto with real.
rewrite W3; unfold FtoRradix; rewrite Fmult_correct; auto with zarith real.
apply Rle_lt_trans with (- (powerRZ radix (Zpred (- N)) × gamma / (1 + powerRZ radix (2 - prec)))+Rabs zH×gam2)%R;auto with real.
rewrite <- W3; apply Rmult_lt_reg_l with (1 + powerRZ radix (2 - prec))%R; auto with real zarith.
apply Rle_lt_trans with ((1 + powerRZ radix (2 - prec)) × gam2 × Rabs zH
- (powerRZ radix (Zpred (- N)) × gam2))%R.
right; field; auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
replace (Rabs zH) with (powerRZ radix (-N))%R.
apply Rle_lt_trans with (gam2*(powerRZ radix (-N-1))*(1+(powerRZ radix (3-prec))))%R;[right|idtac].
pattern (-N)%Z at 1; replace (-N)%Z with (1+(-N-1))%Z; [rewrite powerRZ_add; auto with real zarith|ring].
replace (2%nat-prec)%Z with (2-prec)%Z;auto with zarith.
replace (Zpred (-N))%Z with (-N-1)%Z;[idtac|unfold Zpred;ring].
replace (3-prec)%Z with (1+(2-prec))%Z; [rewrite powerRZ_add; auto with real zarith|ring].
simpl;ring.
unfold FtoRradix, FtoR.
apply Rle_lt_trans with ((powerRZ radix prec - 4) × powerRZ radix (Fexp gam2) × powerRZ radix (- N - 1) ×
(1 + powerRZ radix (3 - prec)))%R.
apply Rmult_le_compat_r;auto with real.
apply Rle_trans with (1+0)%R; auto with real zarith;apply Rle_trans with 1%R;auto with real.
apply Rle_lt_trans with ( (powerRZ radix (Fexp gam2) ×
powerRZ radix (- N - 1)) × ((powerRZ radix prec - 4) × (1 + powerRZ radix (3 - prec))))%R;[right;ring|idtac].
rewrite <- powerRZ_add;auto with real zarith.
replace (Fexp gam2 + (- N - 1))%Z with (Fexp gam2-N-1)%Z;[idtac|ring].
apply Rlt_le_trans with (powerRZ radix (Fexp gam2 - N - 1) ×
((1 + powerRZ radix (2 - prec)) × powerRZ radix prec))%R;[idtac|right;ring].
apply Rmult_lt_compat_l;auto with real zarith.
replace (2-prec)%Z with (2-prec)%Z; auto with zarith.
apply Rle_lt_trans with ( ((powerRZ radix prec)+4)-(powerRZ radix (5-prec)))%R;[right;ring_simplify|idtac].
rewrite <- powerRZ_add; auto with real zarith; ring_simplify (prec + (3 - prec))%Z.
replace (powerRZ radix (5 - prec))%R with (4*(powerRZ radix (3 - prec)))%R;[simpl;ring|idtac].
replace (5-prec)%Z with (2+(3-prec))%Z;[rewrite powerRZ_add;auto with real zarith|ring];simpl;ring.
apply Rlt_le_trans with ((powerRZ radix prec + 4) - 0)%R; auto with real zarith.
unfold Rminus; apply Rplus_lt_compat_l.
apply Ropp_lt_contravar;auto with real zarith.
right;ring_simplify; rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (prec+(2-prec))%Z;simpl;ring.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl; rewrite H3; rewrite H6; simpl; ring.
split.
∃ (Fminus radix x (Fmult zH gam2));split.
unfold FtoRradix; rewrite Fminus_correct;auto with zarith; rewrite Fmult_correct;auto with real zarith.
split.
2:unfold Fmult, Fminus, Fopp, Fplus;simpl.
2:rewrite Zmin_le1;[idtac|rewrite H8; rewrite H3;auto with zarith].
2: auto with zarith float.
apply Zlt_Rlt;apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fminus radix x (Fmult zH gam2))));auto with real zarith.
apply Rle_lt_trans with (Rabs (Fminus radix x (Fmult zH gam2)));[right|idtac].
unfold FtoRradix; rewrite <- Fabs_correct;auto with zarith.
unfold Fabs, FtoR; simpl; ring.
unfold FtoRradix; rewrite Fminus_correct;auto with zarith; rewrite Fmult_correct;auto with real zarith;fold FtoRradix.
replace (Fexp (Fminus radix x (Fmult zH gam2))) with (Fexp gam2 - N - 1)%Z.
2:unfold Fmult, Fminus, Fopp, Fplus;simpl; rewrite Zmin_le1;[auto with zarith|rewrite H8; rewrite H3;auto with zarith].
auto.
apply Rlt_le_trans with (1:=H).
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite W5; unfold Zpred; auto with zarith.
cut ((Fexp gam2 - N - 1) ≤ Fexp x)%Z;[intros T1|idtac].
cut (Fexp x <=(Fexp gam2 - N - 1))%Z;[intros T2;auto with zarith|idtac].
apply Zle_powerRZ with radix; auto with zarith real.
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp x)))%R;[right; unfold FtoR;simpl;ring|idtac].
rewrite <- CanonicFulp with b radix prec x; auto with zarith.
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float (Fnum gam2) (Fexp gam2-N-1)))))%R;[idtac|right; unfold FtoR;simpl;ring].
cut (Fcanonic radix b (Float (Fnum gam2) (Fexp gam2-N-1)));[intros W'|idtac].
rewrite <- CanonicFulp with b radix prec (Float (Fnum gam2) (Fexp gam2-N-1)); auto with zarith.
rewrite FulpFabs; auto with zarith.
apply LeFulpPos; auto with real float zarith.
apply FcanonicBound with radix;auto.
rewrite Fabs_correct; auto with zarith real.
rewrite Fabs_correct; auto with zarith.
fold FtoRradix; apply Rlt_le; apply Rlt_le_trans with (1:=H7).
unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
fold FtoRradix; rewrite <- W3; rewrite Rabs_mult.
rewrite (Rabs_right gam2);[idtac|apply Rle_ge; rewrite W3; auto with real].
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
right; unfold FtoRradix, FtoR;simpl; unfold Zminus;repeat rewrite powerRZ_add;auto with real zarith.
rewrite H3; rewrite H6.
simpl; field;auto with real.
elim W4; intros T3 T2; elim T3; intros T4 T5.
left;split;simpl; auto with zarith.
split;simpl; auto with zarith.
rewrite W5; unfold Zpred; auto with zarith.
apply Zle_trans with (1:=exp_gamma_enough3); auto with zarith.
apply Zle_powerRZ with radix; auto with zarith real.
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp x)))%R;[idtac|right; unfold FtoR;simpl;ring].
rewrite <- CanonicFulp with b radix prec x; auto with zarith.
cut (Fcanonic radix b (Float ((Fnum gam2)-4) (Fexp gam2-N-1)));[intros W'|idtac].
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float ((Fnum gam2)-4) (Fexp gam2-N-1)))))%R;[right; unfold FtoR;simpl;ring|idtac].
cut (0 < FtoR radix (Float ((Fnum gam2)-4) (Fexp gam2 - N - 1)))%R; [intros W''|idtac].
rewrite <- CanonicFulp with b radix prec (Float ((Fnum gam2)-4) (Fexp gam2-N-1)); auto with zarith.
rewrite FulpFabs with b radix prec x; auto with zarith.
apply LeFulpPos; auto with real float zarith.
apply FcanonicBound with radix;auto.
rewrite Fabs_correct; auto with zarith.
fold FtoRradix; apply Rle_trans with (2:=H9).
fold FtoRradix; rewrite <- W3.
apply Rle_trans with (powerRZ radix (Zpred (- N))*(((Fnum gam2)-4)*(powerRZ radix (Fexp gam2))))%R.
right; unfold FtoRradix, FtoR;simpl; unfold Zminus, Zpred;repeat rewrite powerRZ_add; auto with real zarith.
rewrite plus_IZR; simpl;ring.
apply Rle_trans with (powerRZ radix (Zpred (- N)) × (gam2 × / (1 + powerRZ radix (2 - prec))))%R;[idtac|unfold Rdiv;right;ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R; auto with real.
apply Rle_trans with (FtoRradix gam2);[idtac|right;field;auto with real].
unfold FtoRradix, FtoR;rewrite <- Rmult_assoc.
apply Rmult_le_compat_r;auto with real zarith.
apply Rplus_le_reg_l with (-(Fnum gam2)+4+4*(powerRZ radix (2-prec)))%R.
replace (2-prec)%Z with (2-prec)%Z;auto with zarith.
ring_simplify.
apply Rle_trans with 4; auto with real zarith.
apply Rmult_le_reg_l with (powerRZ radix (prec-2));auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (2 - prec + (prec - 2))%Z.
apply Rle_trans with (Fnum gam2);[right;simpl;ring|idtac].
apply Rle_trans with (Zpos (vNum b))%R;auto with real zarith float.
elim W4; intros T1 T2; elim T1; intros T3 T4.
apply Rlt_le; rewrite <- (Zabs_eq (Fnum gam2));auto with real zarith.
apply LeR0Fnum with radix;auto with real zarith;fold FtoRradix; rewrite W3;auto with real.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ;right.
replace (powerRZ radix prec) with (powerRZ radix (2+(prec-2))%Z);
[rewrite powerRZ_add;auto with real zarith;simpl|ring_simplify (2+(prec-2))%Z];ring.
apply Rle_trans with (4×0+4)%R;[right;simpl;ring|idtac].
apply Rplus_le_compat_r;apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with 2%R; auto with real.
apply LtFnumZERO; simpl;auto with real zarith.
apply Zlt_Rlt; unfold Zminus; rewrite plus_IZR;simpl.
apply Rlt_le_trans with (powerRZ radix (Zpred prec));auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred prec) + 4)+- (2 + 1 + 1))%R;[right;ring|idtac];auto with real.
cut (0 < (Fnum gam2) - 4)%Z;[intros W'|apply Zlt_Rlt; unfold Zminus; rewrite plus_IZR;simpl].
2:apply Rlt_le_trans with (powerRZ radix (Zpred prec));auto with real zarith.
2:apply Rle_trans with ((powerRZ radix (Zpred prec) + 4)+- (2 + 1 + 1))%R;[right;ring|idtac];auto with real.
left;split;[split|idtac].
simpl;rewrite Zabs_eq; auto with zarith.
apply Zlt_trans with (Fnum gam2);auto with zarith.
rewrite <- (Zabs_eq (Fnum gam2)); auto with zarith float.
elim W4; intros T1 T2; elim T1;auto with zarith.
simpl;rewrite W5; apply Zle_trans with (1:=exp_gamma_enough3);unfold Zpred; auto with zarith.
apply Zle_trans with (Zabs (radix × (Fnum gam2 - 4)))%Z;auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zle_Rle; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ;unfold Zminus; rewrite mult_IZR;rewrite plus_IZR;simpl.
apply Rle_trans with (2 × (((powerRZ radix (Zpred prec) + 4 ) + - (2 + 1 + 1))))%R;auto with real.
right; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
field; auto with real.
apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R;auto with real.
apply Rle_trans with ((powerRZ radix (Zpred (- N)) × gamma))%R;[right;field;auto with real|idtac].
apply Rle_trans with ((Rabs x×alpha)*gamma)%R;auto with real.
apply Rle_trans with ((alpha×gamma)*Rabs x)%R;[right;ring|apply Rmult_le_compat_r;auto with real].
apply Rplus_le_reg_l with (-1)%R.
apply Rle_trans with (Rabs (-1 + alpha × gamma ))%R;[apply RRle_abs|idtac].
rewrite <- Rabs_Ropp.
replace (- (-1 + alpha × gamma))%R with (1-alpha×gamma)%R;[idtac|ring].
apply Rle_trans with (powerRZ radix (2 - prec));[idtac|right;ring].
replace (2-prec)%Z with (2%nat-prec)%Z;auto with zarith.
apply delta_inf with b;auto with zarith.
apply exp_alpha_le.
cut (Rabs (Rabs x×alpha-2*(powerRZ radix (Zpred (- N)))) ≤ (powerRZ radix (Zpred (- N))))%R;[intros H7|idtac].
split.
apply Rplus_le_reg_l with (- Rabs x×alpha+(powerRZ radix (Zpred (- N))))%R.
ring_simplify.
apply Rle_trans with (2:=H7).
rewrite <- (Rabs_Ropp (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N)))).
apply Rle_trans with (- (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N))))%R;
[right;ring|apply RRle_abs].
apply Rplus_le_reg_l with (-2*(powerRZ radix (Zpred (-N))))%R.
ring_simplify (-2 × powerRZ radix (Zpred (- N)) + 3 × powerRZ radix (Zpred (- N)))%R.
apply Rle_trans with (2:=H7).
apply Rle_trans with (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N)))%R;
[right;ring|apply RRle_abs].
replace (2 × powerRZ radix (Zpred (- N)))%R with (Rabs zH).
2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
2: unfold Fabs, FtoR; simpl; rewrite H3; rewrite H6.
2: simpl; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
2: field; auto with real.
assert (∀ (r1 r2 C:R), ((0 ≤ r1)%R → (0 ≤ r2)%R)
→ ((r1≤0)%R → (r2 ≤ 0)%R)
→ (Rabs (Rabs r1×C- Rabs r2) = Rabs (r1×C- r2))%R).
intros r1 r2 C L1 L2; case (Rle_or_lt 0 r1); intros L3.
rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
replace (-r1×C-(-r2))%R with (-(r1×C-r2))%R;
[apply Rabs_Ropp| ring].
rewrite H.
2: intros; rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
2: intros; rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith.
rewrite <- H2; unfold FtoRradix, radix.
rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
fold radix; fold FtoRradix.
replace (x × alpha - (u - 3%nat × powerRZ radix (Zpred (Zpred (prec - N)))))%R with
(((3%nat × powerRZ radix (Zpred (Zpred (prec - N))))+x×alpha)-u)%R;[idtac|ring].
apply Rmult_le_reg_l with 2%nat;auto with real.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix;apply ClosestUlp; auto with zarith.
right; simpl; unfold Fulp, radix.
rewrite Fexp_u with b prec N alpha x u;auto with zarith.
unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
field; auto with real.
Qed.
End Total.