Library Float.FnElem.FArgReduct2
FArgReduct2 file
Sylvie Boldo
This file explains an improvement of Cody & Waite argument reduction technique using the FMA (fused-multiply-and-add).
Sylvie Boldo
This file explains an improvement of Cody & Waite argument reduction technique using the FMA (fused-multiply-and-add).
Require Export FArgReduct.
Section Reduct.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Section Reduct.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variables prec q : nat.
Variables k N : Z.
Variables alpha gamma x zH : float.
Variable zL : R.
Various bounds
Let bmoinsq :=
Bound
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - q)))))
(dExp b).
Let bzH :=
Bound
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat radix (Zabs_nat (Zsucc (k + N)))))))
(dExp b).
Let b1 :=
Bound
(P_of_succ_nat
(pred
(Zabs_nat (Zpower_nat radix (prec - q + Zabs_nat (Zsucc (k + N)))))))
(dExp b).
All the hypotheses
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded b x.
alpha (the constant, such as pi) and gamma (its inverse)
Hypothesis gammaInvalpha : Closest bmoinsq radix (/ alpha) gamma.
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 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
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 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
zH, the approximation of x*alpha
Hypothesis zHNormal : Fnormal radix bzH zH.
Hypothesis zHDef : (Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R.
Hypothesis zLDef : zL = (x * alpha - zH)%R.
Hypothesis NDef : N = (- Fexp zH)%Z.
Hypothesis zHPos : (0 <= zH)%R.
Hypothesis zHDef : (Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R.
Hypothesis zLDef : zL = (x * alpha - zH)%R.
Hypothesis NDef : N = (- Fexp zH)%Z.
Hypothesis zHPos : (0 <= zH)%R.
Various precisions: gamma on p-q bits and zH on k+N+1
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis preczH_Less_Than_Prec : (Zsucc (k + N) <= Zpred prec)%Z.
Hypothesis preczH_Pos : (0 <= Zsucc (k + N))%Z.
Hypothesis preczH_Greater_Than_One : 1 < Zabs_nat (Zsucc (k + N)).
Hypothesis q_enough : (2 <= q)%Z.
Hypothesis q_not_too_big : (q <= Zsucc (k + N))%Z.
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis preczH_Less_Than_Prec : (Zsucc (k + N) <= Zpred prec)%Z.
Hypothesis preczH_Pos : (0 <= Zsucc (k + N))%Z.
Hypothesis preczH_Greater_Than_One : 1 < Zabs_nat (Zsucc (k + N)).
Hypothesis q_enough : (2 <= q)%Z.
Hypothesis q_not_too_big : (q <= Zsucc (k + N))%Z.
No underflow
Hypothesis
exp_alpha_enough : (- dExp b <= Zsucc q + - (Fexp alpha + (prec + prec)))%Z.
Hypothesis exp_gamma_enough : (- dExp b <= Fexp zH + Fexp gamma)%Z.
exp_alpha_enough : (- dExp b <= Zsucc q + - (Fexp alpha + (prec + prec)))%Z.
Hypothesis exp_gamma_enough : (- dExp b <= Fexp zH + Fexp gamma)%Z.
A few lemmas
Theorem minus_Zminus_precq : (prec - q)%Z = prec - q.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.
Theorem vNum_eq_Zpower :
forall n : nat,
Zpos
(vNum
(Bound (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix n))))
(dExp b))) = Zpower_nat radix n.
intros n; unfold vNum in |- *.
apply
trans_eq
with
(Z_of_nat
(nat_of_P
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix n)))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
cut (Zabs (Zpower_nat radix n) = Zpower_nat radix n).
intros H; pattern (Zpower_nat radix n) at 2 in |- *; rewrite <- H.
rewrite Zabs_absolu.
rewrite <- (S_pred (Zabs_nat (Zpower_nat radix n)) 0); auto with arith zarith.
apply lt_Zlt_inv; simpl in |- *; auto with zarith arith.
rewrite <- Zabs_absolu; rewrite H; auto with arith zarith.
apply Zabs_eq; auto with arith zarith.
Qed.
Theorem vNum_eq_Zpower_bmoinsq :
Zpos (vNum bmoinsq) = Zpower_nat radix (prec - q).
unfold bmoinsq in |- *; apply vNum_eq_Zpower.
Qed.
Theorem vNum_eq_Zpower_bzH :
Zpos (vNum bzH) = Zpower_nat radix (Zabs_nat (Zsucc (k + N))).
unfold bzH in |- *; apply vNum_eq_Zpower.
Qed.
Theorem vNum_eq_Zpower_bzH2 :
powerRZ radix (Zsucc (k + N)) = Zpos (vNum bzH).
rewrite vNum_eq_Zpower_bzH.
rewrite Zpower_nat_powerRZ_absolu; auto with arith zarith.
Qed.
Theorem vNum_eq_Zpower_b1 :
Zpos (vNum b1) =
Zpower_nat radix (prec - q + Zabs_nat (Zsucc (k + N))).
unfold b1 in |- *; apply vNum_eq_Zpower.
Qed.
Theorem vNum_eq_Zpower_b1bis :
powerRZ radix (prec - q + Zsucc (k + N)) = Zpos (vNum b1).
rewrite vNum_eq_Zpower_b1.
rewrite Zpower_nat_Z_powerRZ; auto with arith zarith.
replace (prec - q + Zsucc (k + N))%Z with
(Z_of_nat (prec - q + Zabs_nat (Zsucc (k + N))));
auto with real zarith.
rewrite inj_plus; rewrite <- minus_Zminus_precq; auto with arith zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
Qed.
Theorem prec1_Greater_Than_One : 1 < prec - q + Zabs_nat (Zsucc (k + N)).
auto with arith zarith.
Qed.
Hint Resolve vNum_eq_Zpower_b1 vNum_eq_Zpower_b1bis prec1_Greater_Than_One
vNum_eq_Zpower_bzH vNum_eq_Zpower_bzH2 vNum_eq_Zpower
vNum_eq_Zpower_bmoinsq minus_Zminus_precq: zarith.
First results
Theorem gamma_exp : Fexp gamma = (Zsucc q + - (Fexp alpha + (prec + prec)))%Z.
rewrite <- FcanonicFnormalizeEq with radix bmoinsq (prec - q) gamma;
auto with zarith real.
2: left; auto.
apply boundedNorMinGivesExp; auto with arith zarith.
elim gammaNormal; auto.
apply
RleBoundRoundl with bmoinsq (prec - q) (Closest bmoinsq radix) (/ alpha)%R;
auto with float zarith arith real.
apply ClosestRoundedModeP with (prec - q); auto with arith zarith.
split; auto with zarith.
simpl
(Fnum
(Float (nNormMin radix (prec - q))
(Zsucc q + - (Fexp alpha + (prec + prec)))))
in |- *.
rewrite Zabs_eq; auto with zarith float.
apply ZltNormMinVnum; auto with arith zarith.
unfold nNormMin in |- *; auto with zarith arith.
apply
Rle_trans
with
(nNormMin radix (prec - q) *
powerRZ radix (Zsucc q + - (Fexp alpha + (prec + prec))))%R.
right; unfold FtoR in |- *; simpl in |- *; ring.
unfold nNormMin in |- *.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with zarith real.
rewrite inj_pred; auto with arith zarith.
rewrite <- minus_Zminus_precq.
unfold Zpred, Zsucc in |- *.
replace (prec - q + -1 + (q + 1 + - (Fexp alpha + (prec + prec))))%Z
with (- (prec + Fexp alpha))%Z; [ idtac | unfold Zpred in |- *; ring ].
rewrite <- Rinv_powerRZ; auto with real zarith.
apply Rle_Rinv; auto with real zarith.
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR in |- *; simpl in |- *.
apply Rmult_le_compat_r; auto with real zarith.
elim alphaNormal; intros V1 V2; elim V1; intros V3 V4.
apply Rle_trans with (Zabs (Fnum alpha)); auto with real zarith.
apply Rle_trans with (Zpos (vNum b)); auto with zarith real.
rewrite pGivesBound; auto with real zarith.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite <-
FPredSuc
with
bmoinsq
radix
(prec - q)
(Float (pPred (vNum bmoinsq))
(Zsucc q + - (Fexp alpha + (prec + prec))));
auto with zarith arith.
2: left; apply FnormalPpred with (prec - q); auto with zarith.
apply FPredProp; auto with zarith.
left; auto.
apply FSuccCanonic; auto with zarith.
left; apply FnormalPpred with (prec - q); auto with zarith.
cut
(FtoR radix
(FSucc bmoinsq radix (prec - q)
(Float (pPred (vNum bmoinsq))
(Zsucc q + - (Fexp alpha + (prec + prec))))) =
powerRZ radix (- Zpred (Fexp alpha + prec))); [ intros W | idtac ].
cut
(FtoR radix gamma <=
FtoR radix
(FSucc bmoinsq radix (prec - q)
(Float (pPred (vNum bmoinsq))
(Zsucc q + - (Fexp alpha + (prec + prec))))))%R;
[ intros V | idtac ].
case V; auto with real.
intros V1; Contradict V1; rewrite W; apply gamma_not_pow_2.
apply
RleBoundRoundr with bmoinsq (prec - q) (Closest bmoinsq radix) (/ alpha)%R;
auto with float zarith arith real.
apply ClosestRoundedModeP with (prec - q); auto with arith zarith.
apply FBoundedSuc; auto with zarith.
cut
(Fnormal radix bmoinsq
(Float (pPred (vNum bmoinsq)) (Zsucc q + - (Fexp alpha + (prec + prec)))));
[ intros V; elim V; auto | idtac ].
apply FnormalPpred with (prec - q); auto with zarith.
rewrite W.
rewrite <- Rinv_powerRZ; auto with real zarith.
apply Rle_Rinv; auto with real zarith.
unfold FtoRradix, FtoR in |- *; simpl in |- *.
replace (Zpred (Fexp alpha + prec)) with (Zpred prec + Fexp alpha)%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
elim alphaNormal; intros V1 V2; clear V1.
apply Rmult_le_reg_l with radix; auto with zarith real.
apply Rle_trans with (Zpos (vNum b)); [ right | idtac ].
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ;
pattern (IZR radix) at 1 in |- *; replace (IZR radix) with (powerRZ 2 1);
auto with real zarith.
rewrite <- powerRZ_add; unfold Zpred in |- *; auto with real zarith.
ring_simplify (1 + (prec + -1))%Z; auto with real.
rewrite <- Rmult_IZR.
rewrite <- (Zabs_eq (radix * Fnum alpha)); auto with real zarith.
cut (0 <= Fnum alpha)%Z; [ idtac | apply LeR0Fnum with radix ];
auto with real zarith.
rewrite FSuccSimpl1; auto.
unfold FtoR, nNormMin in |- *.
simpl
(Fnum
(Float (Zpower_nat radix (pred (prec - q)))
(Zsucc
(Fexp
(Float (pPred (vNum bmoinsq))
(Zsucc q + - (Fexp alpha + (prec + prec))))))))
in |- *.
replace
(Fexp
(Float (Zpower_nat radix (pred (prec - q)))
(Zsucc
(Fexp
(Float (pPred (vNum bmoinsq))
(Zsucc q + - (Fexp alpha + (prec + prec)))))))) with
(Zsucc (Zsucc q + - (Fexp alpha + (prec + prec))));
[ idtac | simpl in |- *; auto with zarith ].
rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with zarith real.
replace
(pred (prec - q) + Zsucc (Zsucc q + - (Fexp alpha + (prec + prec))))%Z with
(- Zpred (Fexp alpha + prec))%Z; auto with real.
rewrite inj_pred; auto with zarith arith.
rewrite <- minus_Zminus_precq.
unfold Zsucc, Zpred in |- *; ring.
Qed.
Theorem delta_inf : (Rabs (1 - alpha * gamma) <= powerRZ radix (q - prec))%R.
apply Rmult_le_reg_l with (Rabs (/ alpha)); auto with real.
rewrite Rabs_right; auto with real.
apply Rle_ge; auto with real.
rewrite <- Rabs_mult.
replace (/ alpha * (1 - alpha * gamma))%R with (/alpha-gamma)%R;
[idtac|field; auto with real].
apply Rmult_le_reg_l with (INR 2); auto with arith real.
apply Rle_trans with (Fulp bmoinsq radix (prec - q) gamma).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith.
2: left; auto.
unfold FtoR in |- *; simpl (Fnum (Float 1%nat (Fexp gamma))) in |- *;
simpl (Fexp (Float 1%nat (Fexp gamma))) in |- *.
apply Rle_trans with (powerRZ radix (Fexp gamma));
[right; simpl; ring|idtac].
rewrite gamma_exp; auto.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
apply Rmult_le_reg_l with (FtoRradix alpha); auto with real.
apply Rle_trans with (alpha * / alpha * 2%nat * powerRZ radix (q - prec))%R;
[ idtac | right; ring ].
rewrite Rinv_r; auto with real.
ring_simplify (1 * 2%nat * powerRZ radix (q - prec))%R.
replace (INR 2) with (powerRZ radix 1); [ idtac | simpl in |- *; ring ].
rewrite <- powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR in |- *.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith;
unfold Zsucc in |- *.
replace (Fexp alpha + (q + 1 + - (Fexp alpha + (prec + prec))))%Z
with (q-2*prec+1)%Z by ring.
apply Rmult_le_reg_l with (powerRZ radix (- (1 + (-2 * prec + q))));
auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- powerRZ_add;
auto with real zarith; unfold Zsucc in |- *.
replace (q - 2 * prec + 1 + - (1 + (-2 * prec + q)))%Z with 0%Z by ring.
replace (- (1 + (-2 * prec + q)) + (1 + (q - prec)))%Z with
(Z_of_nat prec) by ring.
apply Rle_trans with (Fnum alpha); [ right; simpl in |- *; ring | idtac ].
apply Rle_trans with (Zabs (Fnum alpha)); auto with real zarith.
apply Rle_trans with (Zpos (vNum b)); auto with zarith real.
elim alphaNormal; intros V1 V2; elim V1; auto with zarith real.
rewrite pGivesBound; auto with real zarith.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
Qed.
Theorem zL_over_zH : (Rabs (zL / zH) <= powerRZ radix (- Zsucc (k + N)))%R.
unfold Rdiv in |- *; rewrite Rabs_mult.
apply Rle_trans with (Rabs zL * powerRZ radix (- k))%R.
apply Rmult_le_compat_l; auto with real zarith.
rewrite Rabs_Rinv.
rewrite <- Rinv_powerRZ; auto with real zarith.
apply Rle_Rinv; auto with real.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with real zarith.
apply
Rle_trans
with
(Zpos (vNum bzH) * FtoR radix (Float 1%nat (Zpred (Fexp zH))))%R.
2: apply FnormalBoundAbs2 with (Zabs_nat (Zsucc (k+N))); auto with zarith.
rewrite <- vNum_eq_Zpower_bzH2; unfold FtoR in |- *; simpl in |- *; right;
ring_simplify.
rewrite <- powerRZ_add; auto with real zarith; rewrite NDef;
unfold Zsucc, Zpred in |- *.
ring_simplify (k + - Fexp zH + 1 + (Fexp zH + -1))%Z; auto with real.
cut (~ is_Fzero zH);
[ unfold is_Fzero in |- * | apply FnormalNotZero with radix bzH; auto ].
intros V; unfold FtoRradix, FtoR in |- *; apply Rmult_integral_contrapositive;
auto with real zarith.
replace (- Zsucc (k + N))%Z with (Zpred (- N) + - k)%Z;
[ idtac | unfold Zsucc, Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
rewrite zLDef; auto with real.
Qed.
Theorem x_over_zHgamma_eq :
(x / (zH * gamma))%R = ((1 + zL / zH) / (1 + (alpha * gamma - 1)))%R.
cut (FtoRradix zH <> 0%R); [ intros V | idtac ].
rewrite zLDef; unfold Rdiv in |- *; field.
repeat (split; auto with real).
ring_simplify (1 + (alpha * gamma -1))%R; auto with real.
cut (~ is_Fzero zH);
[ unfold is_Fzero in |- * | apply FnormalNotZero with radix bzH; auto ].
intros V; unfold FtoRradix, FtoR in |- *; apply Rmult_integral_contrapositive;
auto with real zarith.
Qed.
Theorem SterbenzApprox3 :
forall (rho : R) (x y : float) (b1 b2: Fbound) (prec1 prec2: nat),
1 < prec1 -> 1 < prec2
-> Zpos (vNum b1) = Zpower_nat radix prec1
-> Zpos (vNum b2) = Zpower_nat radix prec2 ->
(0 < rho)%R ->
IZR (Zpos (vNum b1)) = (rho * Zpos (vNum b2))%R ->
(- dExp b2 <= - dExp b1)%Z ->
Fbounded b1 x ->
Fbounded b1 y ->
(/ (1 + / rho) * y <= x)%R ->
(x <= (1 + / rho) * y)%R ->
Fbounded b2
(Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y))
/\ (Rabs (x-y) <= /rho*Rmin x y)%R.
intros; split.
apply SterbenzApprox2 with rho; auto with zarith.
assert (0 <(1 + / rho))%R.
apply Rlt_trans with (1+0)%R; auto with real.
apply Rlt_le_trans with 1%R; auto with real.
case (Rle_or_lt x0 y); intros.
rewrite Rmin_1; auto.
rewrite Rabs_left1; auto with real.
apply Rplus_le_reg_l with x0; apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
apply Rle_trans with (/ (1 + / rho) * y)%R;[right; ring|idtac].
apply Rle_trans with (1:=H8); right; field; split; auto with real.
assert (0 < rho+1)%R; auto with real.
apply Rplus_le_reg_l with y; apply Rle_trans with x0;[right; ring|idtac].
apply Rle_trans with y; auto with real.
rewrite Rmin_2; auto with real.
rewrite Rabs_right; auto with real.
apply Rplus_le_reg_l with y.
apply Rle_trans with x0;[right; ring|idtac].
apply Rle_trans with (1:=H9); right; ring.
apply Rle_ge; apply Rplus_le_reg_l with y; apply Rle_trans with y;[right; ring|idtac].
apply Rle_trans with x0; auto with real.
Qed.
Main theorem
Theorem Fmac_arg_reduct_correct1_aux :
ex (fun u : float => FtoRradix u = (x - zH * gamma)%R /\ Fbounded b u)
/\ (Rabs (x-zH*gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
case zHPos; intros H.
cut (exists u : float, FtoRradix u = (x - zH * gamma)%R /\ Fbounded b u /\
(Rabs (x - zH * gamma) < powerRZ radix (prec - N + Fexp gamma))%R).
intros T; elim T; intros u (L1,(L2,L3)); clear T.
split; auto; exists u; split; auto.
exists
(Fminus radix (Fnormalize radix b1 (prec - q + Zabs_nat (Zsucc (k + N))) x)
(Fnormalize radix b1 (prec - q + Zabs_nat (Zsucc (k + N)))
(Fmult zH gamma))).
cut (Fbounded b1 x); [ intros V1 | idtac ].
cut (Fbounded b1 (Fmult zH gamma)); [ intros V2 | idtac ].
split.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
rewrite Fmult_correct; auto with zarith real.
2: unfold Fmult in |- *; split.
2: rewrite vNum_eq_Zpower_b1; simpl in |- *; rewrite Zpower_nat_is_exp;
rewrite Zabs_Zmult; rewrite Zmult_comm.
2: apply
Zlt_le_trans
with (Zabs (Fnum gamma) * Zpower_nat radix (Zabs_nat (Zsucc (k + N))))%Z.
2: apply Zmult_gt_0_lt_compat_l.
2: apply Zlt_gt.
2: replace (Zabs (Fnum gamma)) with (Fnum (Fabs gamma));
[ idtac | simpl in |- *; auto with zarith ].
2: apply LtR0Fnum with radix; auto with real zarith.
2: rewrite Fabs_correct; fold FtoRradix in |- *; auto with real zarith.
2: rewrite Rabs_right; auto with real; apply Rle_ge; auto with real.
2: apply Zlt_le_trans with (Zpos (vNum bzH)); auto with zarith float.
2: elim zHNormal; auto with float zarith.
2: apply Zle_Zmult_comp_r; auto with zarith.
2: apply Zlt_le_weak; apply Zlt_le_trans with (Zpos (vNum bmoinsq));
auto with zarith.
2: elim gammaNormal; auto with float zarith.
2: simpl in |- *; auto with zarith.
2: split; [ apply Zlt_le_trans with (Zpos (vNum b)) | simpl in |- * ];
auto with float zarith.
2: rewrite pGivesBound; rewrite vNum_eq_Zpower_b1; auto with zarith.
2: apply Zpower_nat_monotone_le; auto with zarith.
2: apply ZleLe; idtac; rewrite inj_plus; rewrite <- minus_Zminus_precq.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
assert (Fbounded b
(Fminus radix
(Fnormalize radix b1 (prec - q + Zabs_nat (Zsucc (k + N))) x)
(Fnormalize radix b1 (prec - q + Zabs_nat (Zsucc (k + N)))
(Fmult zH gamma))) /\
(Rabs (x - Fmult zH gamma) <=
/(powerRZ radix (Zsucc (k + N) - q))*Rmin x (Fmult zH gamma))%R).
unfold FtoRradix; apply SterbenzApprox3 with prec; auto with zarith real.
rewrite <- vNum_eq_Zpower_b1bis; rewrite pGivesBound;
rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (prec - q + Zsucc (k + N))%Z with (Zsucc (k + N) - q + prec)%Z; ring.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *.
apply Rmult_le_reg_l with (/ (zH * gamma))%R; auto with real.
apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real.
apply
Rle_trans
with
(/ (1 + / powerRZ radix (Zsucc (k + N) - q)) *
(zH * gamma * / (zH * gamma)))%R; [ right; ring | idtac ].
rewrite Rinv_r; auto with real.
replace (/ (zH * gamma) * x)%R with (x / (zH * gamma))%R;
[ rewrite x_over_zHgamma_eq | unfold Rdiv in |- *; ring ].
rewrite Rinv_powerRZ; auto with real zarith.
cut (0 < 1 + powerRZ radix (- (Zsucc (k + N) - q)))%R; [ intros V3 | idtac ].
2: apply Rlt_trans with (1 + 0)%R; auto with real zarith; ring_simplify (1 + 0)%R;
auto with real.
apply Rmult_le_reg_l with (1 + powerRZ radix (- (Zsucc (k + N) - q)))%R;
auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith.
cut (0 < alpha * gamma)%R;
[ intros V4 | apply Rmult_lt_0_compat; auto with real ].
ring_simplify (1 + (alpha * gamma - 1))%R; apply Rmult_le_reg_l with (alpha * gamma)%R;
auto with real.
replace (alpha * gamma * (1 * 1))%R with (alpha*gamma)%R;[idtac|ring].
apply
Rle_trans
with
(alpha * gamma * / ( alpha*gamma) *
((1 + powerRZ radix (- (Zsucc (k + N) - q))) * (1 + zL / zH)))%R;
[ idtac | right; unfold Rdiv in |- *; ring ].
rewrite Rinv_r; auto with real.
apply Rle_trans with (Rabs (alpha * gamma)); auto with real.
rewrite Rabs_right; auto with real; apply Rle_ge; auto with real.
replace (alpha * gamma)%R with (1 + - (1 - alpha * gamma))%R;
[ idtac | ring ].
apply Rle_trans with (Rabs 1 + Rabs (- (1 - alpha * gamma)))%R.
apply Rabs_triang.
rewrite Rabs_R1; rewrite Rabs_Ropp.
apply Rle_trans with (1 + powerRZ radix (q - prec))%R.
apply Rplus_le_compat_l; apply delta_inf.
apply
Rle_trans
with
(1 *
((1 + powerRZ radix (- (Zsucc (k + N) - q))) *
(1 - powerRZ radix (- Zsucc (k + N)))))%R.
apply Rle_trans with (1 + (powerRZ radix (- (Zsucc (k + N) - q))
- powerRZ radix (- Zsucc (k + N)) -
powerRZ radix (- (Zsucc (k + N) - q))*powerRZ radix (- Zsucc (k + N))))%R;
[idtac|right; ring].
apply Rplus_le_compat_l.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_trans with (powerRZ radix (q - Zsucc (Zsucc (k + N)))).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus in |- *; apply Zplus_le_compat_l; apply Zle_Zopp;
auto with zarith.
apply Zle_n_Zpred; rewrite Zpred_succ; auto with zarith.
apply Rmult_le_reg_l with (powerRZ radix (Zsucc (k + N)));
auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
ring_simplify.
repeat rewrite <- powerRZ_add; auto with real zarith.
unfold Zsucc in |- *.
replace (k + N + 1 + (q - (k + N + 1 + 1)))%Z with (q-1)%Z by ring.
ring_simplify (k + N + 1 + - (k + N + 1 - q))%Z.
ring_simplify (k + N + 1 + - (k + N + 1))%Z.
ring_simplify (k + N + 1 + (- (k + N + 1 - q) + - (k + N + 1)))%Z.
pattern (Z_of_nat q) at 2 in |- *; replace (Z_of_nat q) with (1 + (q-1))%Z;
[ idtac | ring ].
rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
apply Rplus_le_reg_l with (- powerRZ radix (q-1))%R.
ring_simplify (- powerRZ radix (q-1) + powerRZ radix (q -1))%R.
simpl (powerRZ radix 1) in |- *.
simpl (powerRZ radix 0) in |- *.
replace (- powerRZ radix (q -1) +
(2 * 1 * powerRZ radix (q -1) - 1 -
powerRZ radix (- k - N + q -1)))%R with
(powerRZ radix (q -1) - 1 -
powerRZ radix (- k - N + q -1))%R by ring.
apply
Rle_trans with (powerRZ radix (q -1) - 1- powerRZ radix (q-2) )%R;
[ idtac | unfold Rminus; apply Rplus_le_compat_l ].
replace (q -1)%Z with (1 + (q -2))%Z; [ idtac | ring ].
rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
simpl (powerRZ radix 1) in |- *.
apply Rplus_le_reg_l with 1%R.
ring_simplify.
apply Rle_trans with (powerRZ radix 0)%R;
[ simpl in |- * ; right; ring| idtac ].
apply Rle_powerRZ; auto with real zarith.
apply Ropp_le_contravar.
apply Rle_powerRZ; auto with real zarith.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold Rminus in |- *; apply Rplus_le_compat_l.
apply Rle_trans with (- Rabs (zL / zH))%R; auto with real.
apply Ropp_le_contravar; apply zL_over_zH.
case (Rcase_abs (zL / zH)); intros V5.
rewrite Rabs_left; auto with real.
rewrite Rabs_right; auto with real.
apply Rle_trans with 0%R; auto with real.
unfold FtoRradix;rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *.
apply Rmult_le_reg_l with (/ (zH * gamma))%R; auto with real.
apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real.
apply
Rle_trans
with
((1 + / powerRZ radix (Zsucc (k + N) - q)) *
(zH * gamma * / (zH * gamma)))%R; [ idtac | right; ring ].
rewrite Rinv_r; auto with real.
replace (/ (zH * gamma) * x)%R with (x / (zH * gamma))%R;
[ rewrite x_over_zHgamma_eq | unfold Rdiv in |- *; ring ].
rewrite Rinv_powerRZ; auto with real zarith.
replace (1 + (alpha * gamma - 1))%R with (alpha * gamma)%R; [ idtac | ring ].
cut (0 < alpha * gamma)%R;
[ intros V4 | apply Rmult_lt_0_compat; auto with real ].
apply Rmult_le_reg_l with (alpha * gamma)%R; auto with real.
apply Rle_trans with (alpha * gamma * / (alpha * gamma) * (1 + zL / zH))%R;
[ right; unfold Rdiv in |- *; ring | idtac ].
rewrite Rinv_r; auto with real.
apply Rle_trans with (1 + zL / zH)%R; [ right; ring | idtac ].
apply Rle_trans with (1 + Rabs (zL / zH))%R;
[ apply Rplus_le_compat_l; apply RRle_abs | idtac ].
apply Rle_trans with (1 + powerRZ radix (- Zsucc (k + N)))%R;
[ apply Rplus_le_compat_l; apply zL_over_zH | idtac ].
apply
Rle_trans
with
((1 - powerRZ radix (q - prec)) *
((1 + powerRZ radix (- (Zsucc (k + N) - q))) * 1))%R.
apply Rle_trans with (1 +(- powerRZ radix (q - prec) +
powerRZ radix (- (Zsucc (k + N) - q)) -
powerRZ radix (q - prec) * powerRZ radix (- (Zsucc (k + N) - q))))%R;
[idtac|right; ring].
rewrite <- powerRZ_add; auto with real zarith.
apply Rplus_le_compat_l.
apply Rmult_le_reg_l with (powerRZ radix (Zsucc (k + N)));
auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (Zsucc (k + N) + - Zsucc (k + N))%Z.
ring_simplify.
rewrite Ropp_mult_distr_l_reverse.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (k + N + 1 + - (k + N + 1 - q))%Z.
ring_simplify (k + N + 1 + (q - prec + - (k + N + 1 - q)))%Z.
replace (powerRZ radix 0) with 1%R; [ idtac | simpl in |- *; ring ].
apply
Rle_trans
with
(- powerRZ radix (q + -1) +powerRZ radix q
- powerRZ radix (2*q+-1 * prec))%R;
[ idtac | unfold Rminus;
repeat apply Rplus_le_compat_r; apply Ropp_le_contravar; apply Rle_powerRZ;
auto with real zarith ].
2: apply Zplus_le_reg_r with (prec + - q)%Z.
2: ring_simplify; auto with zarith.
pattern (Z_of_nat q) at 2 in |- *; replace (Z_of_nat q) with (1 + (q + -1))%Z;
[ idtac | ring ].
rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
simpl (powerRZ radix 1) in |- *.
ring_simplify.
apply
Rle_trans with (powerRZ radix (q + -1) + - powerRZ radix (-1 + (q + -1)))%R;
[ idtac | unfold Rminus; apply Rplus_le_compat_l ].
2: apply Ropp_le_contravar; apply Rle_powerRZ; auto with real zarith.
pattern (q + -1)%Z at 1 in |- *;
replace (q + -1)%Z with (1 + (-1 + (q + -1)))%Z; [ idtac | ring ].
rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
simpl (powerRZ radix 1) in |- *.
ring_simplify.
replace 1%R with (powerRZ radix 0); [ apply Rle_powerRZ | simpl in |- * ];
auto with real zarith.
apply Rmult_le_compat_r.
apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (1 + 0)%R; auto with real zarith; ring_simplify (1 + 0)%R;
auto with real zarith.
apply Rle_trans with (1 + - (1 - alpha * gamma))%R;
[ unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar
| right; ring ].
fold Rminus in |- *; apply Rle_trans with (Rabs (1 - alpha * gamma));
[ apply RRle_abs | apply delta_inf ].
elim H0; intros T1 T2; clear H0; split; auto.
unfold FtoRradix; rewrite <- Fmult_correct; auto with zarith; fold FtoRradix.
apply Rle_lt_trans with (1:=T2).
rewrite <- powerRZ_Zopp; auto with real zarith.
replace (prec - N + Fexp gamma)%Z with
((- (Zsucc (k + N) - q))+((prec-q+Zsucc (k +N))+(-N+Fexp gamma)))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (Fmult zH gamma); auto with real.
unfold Rmin; case (Rle_dec x (Fmult zH gamma)); auto with real.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
replace (Fexp (Fmult zH gamma)) with (-N+Fexp gamma)%Z;
[idtac|unfold Fmult; simpl; auto with zarith].
apply Rmult_lt_compat_r; auto with real zarith.
elim V2; intros.
apply Rle_lt_trans with (Rabs (Fnum (Fmult zH gamma)));
[apply RRle_abs|rewrite Rabs_Zabs].
rewrite vNum_eq_Zpower_b1bis; auto with real zarith.
split.
exists x; split; auto with real.
rewrite <- H; ring.
replace (x-zH*gamma)%R with (FtoRradix x);[idtac|rewrite <- H; ring].
apply Rmult_lt_reg_l with alpha; auto.
apply Rle_lt_trans with (Rabs (x*alpha-zH)).
right; replace (x*alpha-zH)%R with (x*alpha)%R; auto with real.
rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real.
rewrite <- H; ring.
apply Rle_lt_trans with (1:=zHDef).
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
((-q-2+prec) +Fexp alpha)%Z;[idtac|rewrite gamma_exp; unfold Zsucc; ring].
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;ring_simplify.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith; 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.
Qed.
End Reduct.
Section Reduct2.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variables prec q : nat.
Variables k N : Z.
Variables alpha gamma x zH : float.
Variable zL : R.
Various bounds
Let bmoinsq :=
Bound
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - q)))))
(dExp b).
Let bzH :=
Bound
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat radix (Zabs_nat (Zsucc (k + N)))))))
(dExp b).
Let b1 :=
Bound
(P_of_succ_nat
(pred
(Zabs_nat (Zpower_nat radix (prec - q + Zabs_nat (Zsucc (k + N)))))))
(dExp b).
All the hypotheses
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded b x.
Hypothesis alphaNormal : Fnormal radix b alpha.
Hypothesis gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
Hypothesis q_enough : (2 <= q)%Z.
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis gammaInvalpha : Closest bmoinsq radix (/ alpha) gamma.
Hypothesis
gamma_not_pow_2 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
Hypothesis zHPos : (0 <= zH)%R.
Hypothesis zHDef : (Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R.
Hypothesis zLDef : zL = (x * alpha - zH)%R.
Hypothesis preczH_Less_Than_Prec : (Zsucc (k + N) <= Zpred prec)%Z.
Hypothesis preczH_Pos : (2 <= Zsucc (k + N))%Z.
Hypothesis NDef : N = (- Fexp zH)%Z.
Hypothesis zHNormal : Fnormal radix bzH zH.
Hypothesis q_not_too_big : (q <= Zsucc (k + N))%Z.
Hypothesis gamma_ge: (powerRZ radix (-dExp b+prec -q +(Zmax 1 (N-1)))<= gamma)%R.
Same as previous, but with an inequality for gamma for the
no-unverflow
Theorem Fmac_arg_reduct_correct1_aux2 :
ex (fun u : float => FtoRradix u = (x - zH * gamma)%R /\ Fbounded b u)
/\ (Rabs (x-zH*gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
cut (- dExp b <= Zsucc q + - (Fexp alpha + (prec + prec)))%Z.
intros V.
apply Fmac_arg_reduct_correct1_aux with q k alpha zL; auto with zarith.
assert (1 < Zabs_nat (Zsucc (k + N)))%Z; auto with zarith.
rewrite <- Zabs_absolu; auto with zarith.
rewrite Zabs_eq; auto with zarith.
assert (- dExp b + prec -q + N - 1 < prec-q + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec -q + Zmax 1 (N - 1))%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.
rewrite minus_Zminus_precq; auto with real zarith.
assert (prec-1+Fexp alpha <= dExp b+q-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 + q - prec))); auto with real.
intros V.
absurd (powerRZ radix (- dExp b + prec - q+1) <= gamma)%R.
apply Rlt_not_le.
assert (exists f:float, Fbounded bmoinsq f /\
(FtoRradix f= powerRZ radix (- dExp b+prec-q))%R).
exists (Float 1 (-dExp b+prec-q)).
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-q)
(Closest bmoinsq radix) (/alpha)%R; auto with real zarith float.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
apply ClosestRoundedModeP with (prec-q); auto with zarith.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
fold FtoRradix; rewrite I2.
apply Rle_trans with (/(powerRZ radix (dExp b + q - prec)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (dExp b + q - prec))%Z with (- dExp b + prec - q)%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.
Qed.
End Reduct2.
Section Reduct3.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variables prec q : nat.
Variables k N : Z.
Variables alpha gamma x zH : float.
Variable zL : R.
Various bounds
Let bmoinsq :=
Bound
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - q)))))
(dExp b).
Let bzH :=
Bound
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat radix (Zabs_nat (Zsucc (k + N)))))))
(dExp b).
Let b1 :=
Bound
(P_of_succ_nat
(pred
(Zabs_nat (Zpower_nat radix (prec - q + Zabs_nat (Zsucc (k + N)))))))
(dExp b).
All the hypotheses
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded 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 gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
q such that gamma is on prec-q bits
Hypothesis q_enough : (2 <= q)%Z.
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis gammaInvalpha : Closest bmoinsq radix (/ alpha) gamma.
Hypothesis
gamma_not_pow_2 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis gammaInvalpha : Closest bmoinsq radix (/ alpha) gamma.
Hypothesis
gamma_not_pow_2 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
zH, the approximation of x*alpha
Hypothesis zHDef : (Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R.
Hypothesis zLDef : zL = (x * alpha - zH)%R.
Hypothesis preczH_Less_Than_Prec : (Zsucc (k + N) <= Zpred prec)%Z.
Hypothesis preczH_Pos : (2 <= Zsucc (k + N))%Z.
Hypothesis NDef : N = (- Fexp zH)%Z.
Hypothesis zHNormal : Fnormal radix bzH zH.
Hypothesis q_not_too_big : (q <= Zsucc (k + N))%Z.
Hypothesis zLDef : zL = (x * alpha - zH)%R.
Hypothesis preczH_Less_Than_Prec : (Zsucc (k + N) <= Zpred prec)%Z.
Hypothesis preczH_Pos : (2 <= Zsucc (k + N))%Z.
Hypothesis NDef : N = (- Fexp zH)%Z.
Hypothesis zHNormal : Fnormal radix bzH zH.
Hypothesis q_not_too_big : (q <= Zsucc (k + N))%Z.
No underflow
Main result, works fine except when z=2^(-N)
Theorem Fmac_arg_reduct_correct1 :
ex (fun u : float => FtoRradix u = (x - zH * gamma)%R /\ Fbounded b u)
/\ (Rabs (x-zH*gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
case (Rle_or_lt 0 zH); intros.
apply Fmac_arg_reduct_correct1_aux2 with q k alpha zL; auto.
elim Fmac_arg_reduct_correct1_aux2 with b prec q k N alpha gamma
(Fopp x) (Fopp zH) (-zL)%R; auto.
intros M1 M2; elim M1;intros u T; elim T; intros; clear T M1.
split.
exists (Fopp u); split.
unfold FtoRradix; rewrite Fopp_correct; unfold radix; rewrite H0.
repeat rewrite Fopp_correct; ring.
apply oppBounded; auto.
generalize M2; repeat rewrite Fopp_correct; auto.
fold radix; fold FtoRradix; intros.
replace (x-zH*gamma)%R with (-(-x-(-zH*gamma)))%R;
[rewrite Rabs_Ropp; auto with real|ring].
apply oppBounded; auto.
rewrite Fopp_correct; auto with real.
apply Rle_trans with (Rabs (x * alpha - zH)); auto with real.
repeat rewrite Fopp_correct.
replace (- FtoR 2 x * FtoR 2 alpha - - FtoR 2 zH)%R with (-(x * alpha - zH))%R.
rewrite Rabs_Ropp; auto with real.
unfold FtoRradix, radix; ring.
rewrite zLDef.
repeat rewrite Fopp_correct; unfold FtoRradix, radix; ring.
apply FnormalFop; auto.
Qed.
End Reduct3.
Section Algo.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variable prec : nat.
Variable N : Z.
Variables alpha x u zH1 : float.
Let bzH (k : Z) :=
Bound
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat radix (Zabs_nat (Zsucc (k + N)))))))
(dExp b).
All the hypotheses
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis precMoreThanOne : 1 < prec.
Hypothesis Fboundedx : Fbounded b x.
Hypothesis alphaNormal : Fnormal radix b alpha.
Hypothesis alphaPos : (0 < alpha)%R.
Algorithm to compute 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 p_enough : (3 < prec)%Z.
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 p_enough : (3 < prec)%Z.
Hypothesis N_not_too_big : (N <= dExp b)%Z.
As before, zH shall no be 2^(-N)
And x must not be 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.
A few lemmas
Theorem vNum_eq_Zpower_bzH_fn :
forall k : Z,
Zpos (vNum (bzH k)) = Zpower_nat radix (Zabs_nat (Zsucc (k + N))).
intros k; unfold bzH in |- *; apply vNum_eq_Zpower.
Qed.
Theorem vNum_eq_Zpower_bzH2_fn :
forall k : Z,
(0 <= Zsucc (k + N))%Z ->
powerRZ radix (Zsucc (k + N)) = Zpos (vNum (bzH k)).
intros k H; rewrite vNum_eq_Zpower_bzH_fn.
rewrite Zpower_nat_powerRZ_absolu; auto with arith zarith.
Qed.
Hint Resolve vNum_eq_Zpower_bzH_fn vNum_eq_Zpower_bzH2_fn: zarith.
Theorem zH1Pos : (0 <= x)%R -> (0 <= zH1)%R.
intros L.
unfold FtoRradix in |- *;
apply
RleRoundedR0
with
b
prec
(Closest b radix)
(u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
replace (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R with
(FtoRradix (Float 3%nat (Zpred (Zpred (prec - N)))));
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply
Rplus_le_reg_l with (FtoRradix (Float 3%nat (Zpred (Zpred (prec - N))))).
ring_simplify.
unfold FtoRradix in |- *;
apply
RleBoundRoundl
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
apply Zle_trans with (- N)%Z; auto with zarith arith.
apply Zplus_le_reg_r with (N + 2)%Z; unfold Zpred in |- *.
ring_simplify; auto with arith zarith.
replace (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))) with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + 0)%R;
[ auto with real | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply Rplus_le_compat_l; apply Rmult_le_pos; auto with real.
Qed.
Theorem zH1Neg : (x <= 0)%R -> (zH1 <= 0)%R.
intros L.
unfold FtoRradix in |- *;
apply
RleRoundedLessR0
with
b
prec
(Closest b radix)
(u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
replace (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R with
(FtoRradix (Float 3%nat (Zpred (Zpred (prec - N)))));
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply
Rplus_le_reg_l with (FtoRradix (Float 3%nat (Zpred (Zpred (prec - N))))).
ring_simplify.
unfold FtoRradix in |- *;
apply
RleBoundRoundr
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
apply Zle_trans with (- N)%Z; auto with zarith arith.
apply Zplus_le_reg_r with (N + 2)%Z; unfold Zpred in |- *.
ring_simplify; auto with arith zarith.
replace (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))) with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + 0)%R;
[ auto with real | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply Rplus_le_compat_l; auto with real.
apply Rle_trans with (0*alpha)%R; auto with real.
Qed.
First computation correct
Theorem zH1_eq :
FtoRradix zH1 = (u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
cut (- dExp b <= Zpred (Zpred (prec - N)))%Z; [ intros V | idtac ].
2: apply Zle_trans with (- N)%Z; auto with zarith arith.
2: apply Zplus_le_reg_r with (N + 2)%Z; unfold Zpred in |- *.
2: ring_simplify; auto with arith zarith.
replace (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R with
(FtoRradix (Float 3%nat (Zpred (Zpred (prec - N)))));
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with zarith.
apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix);
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
2: replace (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))) with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
2: rewrite Fminus_correct; auto with zarith real.
apply Sterbenz; auto with zarith.
apply
RoundedModeBounded
with
radix
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
apply Rle_trans with (FtoR radix (Float 2%nat (Zpred (Zpred (prec - N))))).
unfold FtoRradix, FtoR; simpl.
rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (/2*(2+1+1))%R; auto with real.
right; field.
apply
RleBoundRoundl
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
replace (FtoR radix (Float 2%nat (Zpred (Zpred (prec - N))))) with
(2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
[ auto with real | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply Rplus_le_reg_l with (-x*alpha
- 2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
simpl; ring_simplify.
apply Rle_trans with (-(x*alpha))%R; auto with real.
apply Rle_trans with (Rabs (-(x*alpha)));[apply RRle_abs|idtac].
rewrite Rabs_Ropp; apply Rle_trans with (1:=xalpha_small).
simpl; unfold Rminus; apply Rle_trans with
(powerRZ radix (Zpred (Zpred (prec - N))) +-0)%R; auto with real zarith.
unfold radix; simpl; right; ring.
cut
(FtoR radix (Float 2%nat (Zpred (prec - N))) =
(4%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R);
[ intros W | idtac ].
apply Rle_trans with (FtoR radix (Float 2%nat (Zpred (prec - N)))).
apply
RleBoundRoundr
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
apply
Rle_trans
with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
powerRZ radix (Zpred (Zpred (prec - N))))%R; auto with real.
apply Rplus_le_compat_l.
apply Rle_trans with (Rabs (x*alpha));[apply RRle_abs|idtac].
apply Rle_trans with (1 := xalpha_small);
apply Rle_trans with (powerRZ radix (Zpred (Zpred (prec - N))) - 0)%R;
auto with real zarith; unfold Rminus in |- *; apply Rplus_le_compat_l;
auto with real zarith.
rewrite W; simpl in |- *; right; ring.
rewrite W; unfold FtoR in |- *.
simpl (Fexp (Float 3%nat (Zpred (Zpred (prec - N))))) in |- *.
rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (2%nat * 3%nat)%R; auto with zarith real.
rewrite <- mult_INR; auto with zarith real.
unfold FtoR in |- *; simpl in |- *.
pattern (Zpred (prec - N)) at 1 in |- *;
replace (Zpred (prec - N)) with (1 + Zpred (Zpred (prec - N)))%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith.
simpl (powerRZ 2 1) in |- *; ring.
Qed.
Theorem Normal_and_exp :
forall (f : float) (d : Fbound) (e : Z) (p : nat),
Zpos (vNum d) = Zpower_nat radix p ->
1 < p ->
Fbounded d f ->
(- dExp d <= e)%Z ->
(powerRZ radix (Zpred p + e) <= f)%R ->
(f < powerRZ radix (p + e))%R -> Fexp (Fnormalize radix d p f) = e.
intros f d e p H1 H2 H3 H4 H5 H6.
apply boundedNorMinGivesExp; auto with arith zarith.
fold FtoRradix in |- *; apply Rle_trans with (2 := H5).
right; unfold nNormMin, FtoRradix, FtoR in |- *; simpl in |- *.
rewrite Zpower_nat_Z_powerRZ; rewrite powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith arith real.
apply Rle_trans with (FPred d radix p (Float (nNormMin radix p) (Zsucc e))).
unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix d p f;
auto with zarith.
apply FPredProp; auto with zarith arith float.
left; apply FnormalNnormMin; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix in |- *; apply Rlt_le_trans with (1 := H6);
unfold FtoRradix, FtoR, nNormMin in |- *; simpl in |- *.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
right; rewrite inj_pred; auto with zarith arith real.
replace (Zpred p + Zsucc e)%Z with (p + e)%Z;
[ idtac | unfold Zsucc, Zpred in |- * ]; ring.
right; rewrite FPredSimpl2; auto with zarith; fold FtoRradix in |- *;
simpl in |- *.
replace (Zpred (Zsucc e)) with e;
[ auto with real | unfold Zsucc, Zpred in |- *; ring ].
cut (- dExp d < Zsucc e)%Z; auto with zarith.
Qed.
Theorem Fexp_u : Fexp (Fnormalize radix b prec u) = (- N)%Z.
apply Normal_and_exp; auto with zarith.
elim uDef; auto.
apply Rle_trans with (Float 1%nat (Zpred prec + - N));
[ right; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
unfold FtoRradix in |- *;
apply
RleBoundRoundl
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
auto with zarith arith.
apply Zle_trans with (- N)%Z; auto with zarith arith.
rewrite <- inj_pred; auto with zarith arith.
apply Rle_trans with (powerRZ radix (Zpred prec + - N))%R;
[ right; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
apply Rle_trans with (2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; right; field.
apply Rplus_le_reg_l with (-x*alpha-
2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R; simpl; ring_simplify.
apply Rle_trans with (-(x*alpha))%R; auto with real.
apply Rle_trans with (Rabs (-(x*alpha)))%R; try apply RRle_abs.
rewrite Rabs_Ropp;apply Rle_trans with (1:=xalpha_small).
unfold Rminus, radix; simpl.
apply Rle_trans with (powerRZ 2 (Zpred (Zpred (prec - N))) + - 0)%R; auto with real zarith.
right; ring.
apply Rle_lt_trans with (FtoRradix (Float (Zpower_nat radix prec - 1) (- N))).
unfold FtoRradix in |- *;
apply
RleBoundRoundr
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith arith.
apply
Rle_trans
with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
auto with real.
apply Rplus_le_compat_l; apply Rle_trans with (Rabs (x*alpha)); auto.
apply RRle_abs.
right; unfold FtoR in |- *; simpl in |- *.
rewrite <- Z_R_minus; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
rewrite <- powerRZ_add; auto with real zarith.
replace (- N + prec)%Z with (2 + Zpred (Zpred (prec - N)))%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith; simpl in |- *; ring.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite <- Z_R_minus;
rewrite Zpower_nat_Z_powerRZ.
ring_simplify ((powerRZ radix prec - 1%Z) * powerRZ 2 (- N))%R.
simpl in |- *; rewrite <- powerRZ_add; auto with real zarith;
rewrite Zplus_comm.
unfold Rminus; apply Rlt_le_trans with ( powerRZ 2 (- N+prec)+-0)%R;
auto with real zarith.
apply Rplus_lt_compat_l; apply Ropp_lt_contravar.
ring_simplify; auto with real zarith.
right; ring.
Qed.
Theorem Normal_and_exp2 :
forall (f : float) (d : Fbound) (e m : Z) (p : nat),
Zpos (vNum d) = Zpower_nat radix p ->
1 < p ->
(- dExp d <= e)%Z ->
f = Float m e :>R ->
(powerRZ radix (Zpred p + e) <= Rabs f)%R ->
(Rabs f < powerRZ radix (p + e))%R ->
ex (fun g : float => g = f :>R /\ Fnormal radix d g /\ Fexp g = e).
intros f d e m p H1 H2 H3 H4 H5 H6.
cut (Fbounded d (Float m e)); [ intros H7 | idtac ].
exists (Float m e).
split; auto with real; split; auto; split; auto.
rewrite H1; simpl (Fnum (Float m e)) in |- *.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
apply le_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite mult_IZR.
apply Rmult_le_reg_l with (powerRZ radix (Zpred e)); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
replace (Zpred e + p)%Z with (Zpred p + e)%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite <- Rabs_Zabs.
apply Rle_trans with (1 := H5); rewrite H4; unfold FtoRradix, FtoR in |- *;
simpl in |- *.
rewrite Rabs_mult; rewrite Rabs_right with (powerRZ 2 e);[idtac|
apply Rle_ge; auto with real zarith].
pattern e at 1 in |- *; replace e with (1 + Zpred e)%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with zarith real; simpl in |- *; right; ring.
split; auto with zarith.
rewrite H1; simpl (Fnum (Float m e)) in |- *.
apply lt_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_lt_reg_l with (powerRZ radix e); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Zplus_comm; apply Rle_lt_trans with (2 := H6); rewrite H4.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; simpl in |- *; right; ring.
Qed.
Theorem u_bounds :
(2%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
powerRZ radix (- N) <= u)%R /\
(u <= powerRZ radix (prec - N) - powerRZ radix (- N))%R.
split.
apply Rle_trans with (FtoRradix (Float (Zpower_nat radix (prec-1) + 1) (- N))).
right; unfold FtoRradix, FtoR in |- *; simpl in |- *.
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
rewrite <- powerRZ_add; auto with real zarith.
replace (- N + (prec-1)%nat)%Z with (1 + Zpred (Zpred (prec - N)))%Z.
rewrite powerRZ_add; auto with real zarith; simpl in |- *; ring.
apply trans_eq with (-N+pred prec)%Z; auto with zarith.
rewrite inj_pred; auto with zarith; unfold Zpred; ring.
unfold FtoRradix in |- *;
apply
RleBoundRoundl
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith arith.
apply Zlt_le_trans with (Zpower_nat radix (prec - 1)+Zpower_nat radix (prec - 1))%Z;
auto with zarith.
assert (1 < Zpower_nat radix (prec - 1))%Z; auto with zarith.
apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
pattern prec at 3; replace prec with (1+(prec-1))%nat; auto with zarith.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat radix 1) with 2%Z; auto with zarith.
apply
Rle_trans
with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) -
(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
auto with real.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite plus_IZR;
rewrite Zpower_nat_Z_powerRZ.
simpl; ring_simplify.
rewrite Rplus_comm; apply Rplus_le_compat_l.
replace (Z_of_nat (prec -1)%nat) with (prec -1)%Z; auto with zarith.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; right; field; auto with real.
apply trans_eq with (Z_of_nat (pred prec)); auto with zarith.
rewrite inj_pred; auto with zarith.
unfold Rminus; apply Rplus_le_compat_l.
apply Rle_trans with (-(-(x*alpha)))%R; auto with real.
apply Ropp_le_contravar.
apply Rle_trans with (Rabs (-(x*alpha))); try apply RRle_abs; rewrite Rabs_Ropp.
apply Rle_trans with (1:=xalpha_small); auto with real.
apply Rle_trans with (FtoRradix (Float (Zpower_nat radix prec - 1) (- N))).
unfold FtoRradix in |- *;
apply
RleBoundRoundr
with
b
prec
(Closest b radix)
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith arith.
apply
Rle_trans
with
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
auto with real.
apply Rplus_le_compat_l; apply Rle_trans with (Rabs (x*alpha)); auto.
apply RRle_abs.
right; unfold FtoR in |- *; simpl in |- *.
rewrite <- Z_R_minus; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
rewrite <- powerRZ_add; auto with real zarith.
replace (- N + prec)%Z with (2 + Zpred (Zpred (prec - N)))%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith; simpl in |- *; ring.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite <- Z_R_minus;
rewrite Zpower_nat_Z_powerRZ.
simpl (IZR 1).
ring_simplify ((powerRZ radix prec - 1) * powerRZ 2 (- N))%R.
simpl in |- *; rewrite <- powerRZ_add; auto with real zarith;
rewrite Zplus_comm.
Qed.
Theorem exists_k :
ex
(fun k : Z =>
(powerRZ radix k <= Rabs zH1)%R /\
(Rabs zH1 < powerRZ radix (Zsucc k))%R /\
(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
(0 <= Zsucc (k + N))%Z /\
1 < Zabs_nat (Zsucc (k + N)) /\ (2 <= Zsucc (k + N))%Z).
generalize u_bounds; intros T; elim T; intros H'1 H'2; clear T.
exists (pred (digit radix (Fnum zH1)) + Fexp zH1)%Z.
cut (powerRZ radix (pred (digit radix (Fnum zH1)) + Fexp zH1) <= Rabs zH1)%R;
[ intros H2 | idtac ].
cut
(Rabs zH1 < powerRZ radix (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1)))%R;
[ intros H3 | idtac ].
2: replace (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1)) with
(Zsucc (pred (digit radix (Fnum zH1))) + Fexp zH1)%Z;
[ idtac | unfold Zsucc in |- *; ring ].
2: rewrite powerRZ_add; auto with real zarith.
2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith; unfold Fabs, FtoR in |- *; simpl.
2: apply Rmult_lt_compat_r; auto with real zarith.
2: replace (Zsucc (pred (digit radix (Fnum zH1)))) with
(Z_of_nat (S (pred (digit radix (Fnum zH1)))));
auto with arith zarith.
2: replace 2%R with (IZR radix); auto with real zarith.
2: rewrite <- Zpower_nat_Z_powerRZ; apply Rlt_IZR.
2: apply Zlt_le_trans with (Zpower_nat radix (digit radix (Fnum zH1)));
auto with arith zarith.
2: unfold Zsucc in |- *; replace 1%Z with (Z_of_nat 1);
auto with arith zarith.
2: rewrite <- inj_plus; auto with arith zarith.
split; auto.
split; auto.
split.
apply Zgt_le_succ; apply Zlt_gt.
apply Zplus_lt_reg_r with (- N)%Z.
replace (pred (digit radix (Fnum zH1)) + Fexp zH1 + N + - N)%Z with
(pred (digit radix (Fnum zH1)) + Fexp zH1)%Z; [ idtac | ring ].
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1 := H2); rewrite zH1_eq.
unfold Rabs; case Rcase_abs; intros.
apply Rplus_lt_reg_r with (u-powerRZ radix (Zpred (Zpred prec) + - N))%R;
ring_simplify.
apply Rlt_le_trans with (2:=H'1).
apply Rle_lt_trans with (2%nat * powerRZ radix (Zpred (Zpred (prec - N)))
+ 0)%R;[right|auto with real zarith].
replace (Zpred (Zpred prec) + - N)%Z with (Zpred (Zpred (prec - N)));
[idtac|unfold Zpred]; simpl; ring.
apply
Rplus_lt_reg_r with (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
ring_simplify
(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
(u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N)))))%R.
apply Rle_lt_trans with (1 := H'2).
apply Rlt_le_trans with (powerRZ radix (prec - N) - 0)%R;
auto with real zarith.
unfold Rminus in |- *; apply Rplus_lt_compat_l; auto with real zarith.
right; replace (Zpred (Zpred prec) + - N)%Z with (Zpred (Zpred (prec - N)));
[ idtac | unfold Zpred in |- *; ring ].
pattern (prec - N)%Z at 1 in |- *;
replace (prec - N)%Z with (2 + Zpred (Zpred (prec - N)))%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith; simpl in |- *; ring.
cut (2 <= Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1 + N))%Z;
[ intros H4 | idtac ].
split; auto with zarith.
split; auto.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
replace (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1 + N)) with
(Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1) + N)%Z;
[ idtac | unfold Zsucc in |- *; ring ].
replace 2%Z with (Zsucc 1); [ idtac | unfold Zsucc in |- *; ring ].
apply Zgt_le_succ; apply Zlt_gt.
apply Zplus_lt_reg_l with (- N)%Z.
ring_simplify (- N + (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1) + N))%Z.
replace (- N + 1)%Z with (Zsucc (- N));
[ idtac | unfold Zsucc in |- *; ring ].
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (2 := H3).
apply Rle_trans with (2:=zH_not_too_small).
apply Rle_powerRZ; unfold Zsucc; auto with real zarith.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; rewrite powerRZ_add; auto with real zarith; simpl.
apply Rmult_le_compat_r; auto with real zarith.
replace 2%R with (IZR radix); auto with real zarith.
rewrite <- Zpower_nat_Z_powerRZ; apply Rle_IZR.
apply digitLess.
unfold not; intros.
Contradict zH_not_too_small.
apply Rlt_not_le; apply Rle_lt_trans with 0%R; auto with real.
replace (FtoRradix zH1) with 0%R.
rewrite Rabs_R0; auto with real.
unfold FtoRradix, FtoR; rewrite H; simpl; ring.
Qed.
Not very readable, I know, but those are the hypotheses I will
need to make things go right when calling the previous theorem.
This is the theorem stating the correctness of the algorithm
computing z.
Theorem arg_reduct_exists_k_zH :
ex
(fun k : Z =>
ex
(fun zH : float =>
zH1 = zH :>R /\
(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
(0 <= Zsucc (k + N))%Z /\
1 < Zabs_nat (Zsucc (k + N)) /\
N = (- Fexp zH)%Z /\
Fnormal radix (bzH k) zH /\
(Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R /\
(powerRZ radix k <= Rabs zH1)%R /\ (Rabs zH1 < powerRZ radix (Zsucc k))%R)).
generalize exists_k; intros T1.
elim T1; intros k T2; elim T2; intros H1 T3; elim T3; intros H2 T4; elim T4;
intros H3 T5; elim T5; intros H4 T6; elim T6; intros H5 H6;
clear T1 T2 T3 T4 T5 T6.
generalize
(Normal_and_exp2 zH1 (bzH k) (- N)
(Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec))) (
Zabs_nat (Zsucc (k + N)))); intros T.
lapply T; auto with zarith; intros T1; clear T.
lapply T1; auto with zarith; intros T; clear T1.
lapply T; auto with zarith; intros T1; clear T.
lapply T1; auto with zarith; [ intros T; clear T1 | idtac ].
lapply T; auto with zarith; [ intros T1; clear T | idtac ].
lapply T1; auto with zarith; [ intros T; clear T1 | idtac ].
elim T; intros zH T1.
elim T1; intros H9 T2; elim T2; intros H10 H11; clear T T1 T2.
exists k; exists zH.
split; auto with real.
split; auto with zarith.
split; auto.
split; auto.
split; auto with zarith.
split; auto.
split; auto.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: replace (Zsucc (k + N) + - N)%Z with (Zsucc k);
[ auto with real | unfold Zsucc in |- *; ring ].
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: replace (Zpred (Zsucc (k + N)) + - N)%Z with k;
[ auto with real | unfold Zsucc, Zpred in |- *; ring ].
2: rewrite zH1_eq; unfold FtoRradix in |- *;
rewrite <- FnormalizeCorrect with radix b prec u;
auto with zarith; unfold FtoR in |- *.
2: apply
trans_eq
with
((Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec)))%Z *
powerRZ radix (- N))%R; [ idtac | simpl in |- *; auto with real ].
2: rewrite Fexp_u; unfold Zminus in |- *; rewrite plus_IZR;
rewrite Ropp_Ropp_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
2: ring_simplify.
2: replace (Zpred (Zpred (prec + - N))) with (-N+ (pred (pred prec)))%Z.
2: rewrite powerRZ_add; auto with real zarith.
2: simpl; ring.
2: rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith.
2: unfold Zpred; ring.
rewrite H9; rewrite zH1_eq.
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 (INR 2); auto with arith real.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith.
unfold Fulp in |- *; rewrite Fexp_u.
pattern (- N)%Z at 1 in |- *; replace (- N)%Z with (1 + Zpred (- N))%Z;
[ idtac | unfold Zpred in |- *; ring ].
rewrite powerRZ_add; auto with real zarith; right; simpl in |- *; ring.
Qed.
End Algo.
Section Total.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables
Variable b : Fbound.
Variables prec q : nat.
Variable N : Z.
Variables alpha gamma x zH1 u : float.
Variable zL : R.
Let bmoinsq :=
Bound
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - q)))))
(dExp b).
All the hypotheses
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded 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 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
Hypothesis gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
Hypothesis
gamma_not_pow_2 : forall e : Z, FtoRradix gamma <> powerRZ radix e.
About q
Hypothesis pMoinsqGreaterThanOne : 1 < prec - q.
Hypothesis q_enough : (2 <= q)%Z.
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
Hypothesis gamma_ge: (powerRZ radix (-dExp b+prec -q +(Zmax 1 (N-1)))<= gamma)%R.
Lemma Sterbenzbis: forall (x y :float),
Fbounded b x ->
Fbounded b y ->
(/ S 1 * y <= x)%R ->
(x <= S 1 * y)%R ->
Fbounded b (Fminus radix x y) /\
(Rabs (x - y) <= y)%R.
intros; split.
apply Sterbenz; auto with zarith.
assert (0 <= y)%R.
case (Rle_or_lt 0 y); auto; intros.
absurd (y <= 4*y)%R.
apply Rlt_not_le.
apply Rle_lt_trans with (y+3*y)%R;[right; ring|idtac].
apply Rlt_le_trans with (y+0)%R;[apply Rplus_lt_compat_l; auto with real|right; ring].
apply Rlt_le_trans with (3*0)%R; auto with real.
apply Rmult_lt_compat_l; auto with real.
apply Rlt_trans with 2%R; auto with real.
apply Rmult_le_reg_l with (/(INR 2))%R; auto with real zarith.
apply Rle_trans with (1:=H1).
apply Rle_trans with (1:=H2); right; simpl; field; auto with real.
case (Rle_or_lt x0 y); intros.
rewrite Rabs_left1.
apply Rplus_le_reg_l with (x0-y)%R.
apply Rle_trans with 0%R;[right; ring|idtac].
apply Rle_trans with x0;[idtac| right; ring].
apply Rle_trans with (2:=H1); auto with real zarith.
apply Rle_trans with (0*y)%R;[right; ring|apply Rmult_le_compat_r; auto with real].
apply Rplus_le_reg_l with y; apply Rle_trans with x0; auto with real.
apply Rle_trans with y; auto with real.
rewrite Rabs_right.
apply Rplus_le_reg_l with y; apply Rle_trans with x0; auto with real.
apply Rle_trans with (1:=H2); right; simpl; ring.
apply Rle_ge; apply Rplus_le_reg_l with y; apply Rle_trans with y; auto with real.
apply Rle_trans with x0; auto with real.
Qed.
Lemma Sterbenzter: forall (x y :float),
Fbounded b x ->
Fbounded b y ->
(/ S 1 * Rabs y <= Rabs x)%R ->
(Rabs x <= S 1 * Rabs y)%R ->
(0 <= x*y)%R ->
Fbounded b (Fminus radix x y) /\
(Rabs (x - y) <= Rabs y)%R.
intros r1 r2; intros.
case (Rle_or_lt 0 r1); case (Rle_or_lt 0 r2); intros.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
apply Sterbenzbis; auto.
rewrite Rabs_right in H1; rewrite Rabs_right in H1; try apply Rle_ge; auto with real.
rewrite Rabs_right in H2; rewrite Rabs_right in H2; try apply Rle_ge; auto with real.
case H5; intros.
Contradict H3; auto with real.
apply Rlt_not_le; apply Rlt_le_trans with (r1*0)%R; auto with real.
assert (FtoRradix r2=0)%R.
assert (Rabs r2=0)%R; auto with real.
assert (Rabs r2 <=0)%R; auto with real.
apply Rmult_le_reg_l with (/2%nat)%R; auto with real zarith.
apply Rle_trans with (1:=H1); rewrite <- H6; rewrite Rabs_R0; right; ring.
case (Req_dec r2 0); auto.
intros; Contradict H7; apply Rabs_no_R0; auto.
rewrite (Rabs_right r2).
apply Sterbenzbis; auto.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; rewrite H7; auto with real.
rewrite H7; auto with real.
case H4; intros.
Contradict H3; auto with real.
apply Rlt_not_le; apply Rlt_le_trans with (0*r2)%R; auto with real.
assert (FtoRradix r1=0)%R.
assert (Rabs r1=0)%R; auto with real.
assert (Rabs r1 <=0)%R; auto with real.
apply Rle_trans with (1:=H2); rewrite <- H6; rewrite Rabs_R0; right; ring.
case (Req_dec r1 0); auto.
intros; Contradict H7; apply Rabs_no_R0; auto.
rewrite (Rabs_right r2).
apply Sterbenzbis; auto.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; auto with real.
assert (Fbounded b (Fminus radix (Fopp r1) (Fopp r2))
/\ (Rabs (Fopp r1 - Fopp r2) <= (Fopp r2))%R).
apply Sterbenzbis; auto with zarith float.
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite Rabs_left1 in H1; rewrite Rabs_left1 in H1; auto with real.
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite Rabs_left1 in H2; rewrite Rabs_left1 in H2; auto with real.
elim H6; intros; split.
apply oppBoundedInv.
rewrite Fopp_Fminus_dist; auto with zarith float.
replace (r1-r2)%R with (-(Fopp r1-Fopp r2))%R.
rewrite Rabs_Ropp; apply Rle_trans with (1:=H8).
right; rewrite Rabs_left1; auto with real.
unfold FtoRradix; rewrite Fopp_correct; auto.
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
Qed.
Lemma Sterbenzbis: forall (x y :float),
Fbounded b x ->
Fbounded b y ->
(/ S 1 * y <= x)%R ->
(x <= S 1 * y)%R ->
Fbounded b (Fminus radix x y) /\
(Rabs (x - y) <= y)%R.
intros; split.
apply Sterbenz; auto with zarith.
assert (0 <= y)%R.
case (Rle_or_lt 0 y); auto; intros.
absurd (y <= 4*y)%R.
apply Rlt_not_le.
apply Rle_lt_trans with (y+3*y)%R;[right; ring|idtac].
apply Rlt_le_trans with (y+0)%R;[apply Rplus_lt_compat_l; auto with real|right; ring].
apply Rlt_le_trans with (3*0)%R; auto with real.
apply Rmult_lt_compat_l; auto with real.
apply Rlt_trans with 2%R; auto with real.
apply Rmult_le_reg_l with (/(INR 2))%R; auto with real zarith.
apply Rle_trans with (1:=H1).
apply Rle_trans with (1:=H2); right; simpl; field; auto with real.
case (Rle_or_lt x0 y); intros.
rewrite Rabs_left1.
apply Rplus_le_reg_l with (x0-y)%R.
apply Rle_trans with 0%R;[right; ring|idtac].
apply Rle_trans with x0;[idtac| right; ring].
apply Rle_trans with (2:=H1); auto with real zarith.
apply Rle_trans with (0*y)%R;[right; ring|apply Rmult_le_compat_r; auto with real].
apply Rplus_le_reg_l with y; apply Rle_trans with x0; auto with real.
apply Rle_trans with y; auto with real.
rewrite Rabs_right.
apply Rplus_le_reg_l with y; apply Rle_trans with x0; auto with real.
apply Rle_trans with (1:=H2); right; simpl; ring.
apply Rle_ge; apply Rplus_le_reg_l with y; apply Rle_trans with y; auto with real.
apply Rle_trans with x0; auto with real.
Qed.
Lemma Sterbenzter: forall (x y :float),
Fbounded b x ->
Fbounded b y ->
(/ S 1 * Rabs y <= Rabs x)%R ->
(Rabs x <= S 1 * Rabs y)%R ->
(0 <= x*y)%R ->
Fbounded b (Fminus radix x y) /\
(Rabs (x - y) <= Rabs y)%R.
intros r1 r2; intros.
case (Rle_or_lt 0 r1); case (Rle_or_lt 0 r2); intros.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
apply Sterbenzbis; auto.
rewrite Rabs_right in H1; rewrite Rabs_right in H1; try apply Rle_ge; auto with real.
rewrite Rabs_right in H2; rewrite Rabs_right in H2; try apply Rle_ge; auto with real.
case H5; intros.
Contradict H3; auto with real.
apply Rlt_not_le; apply Rlt_le_trans with (r1*0)%R; auto with real.
assert (FtoRradix r2=0)%R.
assert (Rabs r2=0)%R; auto with real.
assert (Rabs r2 <=0)%R; auto with real.
apply Rmult_le_reg_l with (/2%nat)%R; auto with real zarith.
apply Rle_trans with (1:=H1); rewrite <- H6; rewrite Rabs_R0; right; ring.
case (Req_dec r2 0); auto.
intros; Contradict H7; apply Rabs_no_R0; auto.
rewrite (Rabs_right r2).
apply Sterbenzbis; auto.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; rewrite H7; auto with real.
rewrite H7; auto with real.
case H4; intros.
Contradict H3; auto with real.
apply Rlt_not_le; apply Rlt_le_trans with (0*r2)%R; auto with real.
assert (FtoRradix r1=0)%R.
assert (Rabs r1=0)%R; auto with real.
assert (Rabs r1 <=0)%R; auto with real.
apply Rle_trans with (1:=H2); rewrite <- H6; rewrite Rabs_R0; right; ring.
case (Req_dec r1 0); auto.
intros; Contradict H7; apply Rabs_no_R0; auto.
rewrite (Rabs_right r2).
apply Sterbenzbis; auto.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; rewrite H7; auto with real.
rewrite <- H6; auto with real.
assert (Fbounded b (Fminus radix (Fopp r1) (Fopp r2))
/\ (Rabs (Fopp r1 - Fopp r2) <= (Fopp r2))%R).
apply Sterbenzbis; auto with zarith float.
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite Rabs_left1 in H1; rewrite Rabs_left1 in H1; auto with real.
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite Rabs_left1 in H2; rewrite Rabs_left1 in H2; auto with real.
elim H6; intros; split.
apply oppBoundedInv.
rewrite Fopp_Fminus_dist; auto with zarith float.
replace (r1-r2)%R with (-(Fopp r1-Fopp r2))%R.
rewrite Rabs_Ropp; apply Rle_trans with (1:=H8).
right; rewrite Rabs_left1; auto with real.
unfold FtoRradix; rewrite Fopp_correct; auto.
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
Qed.
Main result: q can be anything but we need alpha * gamma <= 1
Theorem Fmac_arg_reduct_correct2 :
(alpha * gamma <= 1)%R ->
ex (fun u : float => FtoRradix u = (x - zH1 * gamma)%R /\ Fbounded b u)
/\ (Rabs (x-zH1*gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
assert (J:(- dExp b <= Zsucc q + - (Fexp alpha + (prec + prec)))%Z).
assert (prec-1+Fexp alpha <= dExp b+q-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 + q - prec))); auto with real.
intros V.
absurd (powerRZ radix (- dExp b + prec - q+1) <= gamma)%R.
apply Rlt_not_le.
assert (exists f:float, Fbounded bmoinsq f /\
(FtoRradix f= powerRZ radix (- dExp b+prec-q))%R).
exists (Float 1 (-dExp b+prec-q)).
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-q)
(Closest bmoinsq radix) (/alpha)%R; auto with real zarith float.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
apply ClosestRoundedModeP with (prec-q); auto with zarith.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
fold FtoRradix; rewrite I2.
apply Rle_trans with (/(powerRZ radix (dExp b + q - prec)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (dExp b + q - prec))%Z with (- dExp b + prec - q)%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.
intros G.
case (Req_dec zH1 0); intros H1.
split.
exists 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.
ring_simplify (2*1)%R; 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
((-q-2+prec) +Fexp alpha)%Z;[idtac|
rewrite gamma_exp with b prec q alpha gamma;
auto with zarith; unfold Zsucc; ring].
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;ring_simplify.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith; 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.
case (Rle_or_lt (powerRZ radix (q - Zsucc N)) (Rabs zH1)); intros H'.
cut
(exists k : Z,
(exists 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 q k alpha (x * alpha - zH)%R;
auto with zarith real arith.
apply Zle_trans with (1 := H4); auto with zarith.
assert (1 < Zabs (Zsucc (k+N)))%Z; auto with zarith.
rewrite Zabs_absolu; auto with zarith.
rewrite Zabs_eq in H; auto with zarith.
apply Zplus_le_reg_l with (- Zsucc N)%Z.
replace (- Zsucc N + q)%Z with (q - 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.
fold radix FtoRradix in |- *; apply Rle_trans with (2 := H');
auto with real zarith.
apply Rle_powerRZ; unfold radix in |- *; auto with real zarith.
cut
(exists zH : float,
FtoRradix zH1 = zH /\
Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred q))%R /\ (0 < Rabs zH)%R).
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.
assert ((Fbounded b (Fminus radix x (Fmult zH gamma))
/\ (Rabs (x - (Fmult zH gamma)) <= Rabs (Fmult zH gamma))%R)).
apply Sterbenzter; auto with zarith.
split; unfold Fmult in |- *; simpl in |- *.
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs; rewrite Rmult_IZR;
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
replace (Z_of_nat prec) with (q + (prec - q)%nat)%Z;
[ rewrite powerRZ_add | rewrite inj_minus1 ];
auto with arith zarith real.
rewrite Rabs_mult; apply Rmult_le_0_lt_compat; auto with real.
rewrite Rabs_Zabs; apply Rlt_trans with (1 := H4);
auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum bmoinsq)));
auto with real zarith.
rewrite Faux.Rabsolu_Zabs; elim gammaNormal; intros T1 T2; elim T1;
intros T3 T4; auto with real zarith.
right; unfold bmoinsq in |- *; rewrite vNum_eq_Zpower_bmoinsq;
auto with real zarith.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
assert (- dExp b + prec -q + N - 1 < prec-q + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec -q + Zmax 1 (N - 1))%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.
rewrite minus_Zminus_precq; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *;
apply Rmult_le_reg_l with alpha; auto with real.
rewrite Rabs_mult; rewrite Rabs_right with gamma; try apply Rle_ge; auto with real.
apply Rle_trans with (/ 2%nat * Rabs zH * (alpha * gamma))%R;
[ right; ring | idtac ].
apply Rle_trans with (/ 2%nat * Rabs zH * 1)%R;
[ apply Rmult_le_compat_l; auto | idtac ].
apply Rmult_le_pos; auto with real zarith arith real.
apply Rplus_le_reg_l with (/ 2%nat * Rabs zH - alpha * Rabs x)%R.
ring_simplify.
apply Rle_trans with (Rabs zH - Rabs x * alpha)%R; [ right | idtac ].
simpl; field; auto with real.
replace (Rabs x*alpha)%R with (Rabs (x*alpha));[idtac|rewrite Rabs_mult;
rewrite Rabs_right with alpha; try apply Rle_ge; auto with real].
apply Rle_trans with (Rabs (zH - x * alpha)); [ apply Rabs_triang_inv | idtac ].
rewrite <- H2; unfold FtoRradix, radix in |- *;
rewrite zH1_eq with b prec N alpha x u zH1; auto with real zarith.
fold radix FtoRradix in |- *; rewrite <- Rabs_Ropp.
replace
(- (u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))) - x * alpha))%R
with (3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha - u)%R;
[ idtac | ring ].
apply Rmult_le_reg_l with (INR 2); auto with real arith.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith.
unfold Fulp, radix in |- *; rewrite Fexp_u with b prec N alpha x u;
auto with real zarith.
unfold FtoRradix, radix in |- *;
rewrite <- zH1_eq with b prec N alpha x u zH1; auto with real zarith.
fold radix FtoRradix in |- *; rewrite H2; rewrite <- H3; fold radix in |- *;
unfold FtoRradix, FtoR in |- *; auto with real zarith.
apply Rle_trans with (1 * (1 * powerRZ radix (Fexp zH)))%R;
[ right; ring | idtac ].
rewrite Rabs_mult.
rewrite Rabs_right with (powerRZ radix (Fexp zH)); try apply Rle_ge; auto with real zarith.
apply Rmult_le_compat_l; auto with real; apply Rmult_le_compat_r;
auto with real zarith.
rewrite Rabs_Zabs.
cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
apply Zlt_le_trans with (Fnum (Fabs (zH))); auto with zarith.
apply LtR0Fnum with radix; auto with real zarith.
rewrite Fabs_correct; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *;
apply Rmult_le_reg_l with alpha; auto with real.
apply Rplus_le_reg_l with (- Rabs zH)%R.
replace (alpha*Rabs x)%R with (Rabs (x*alpha));[idtac|
rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real].
apply Rle_trans with (Rabs (x * alpha) - Rabs zH)%R; [ right; ring | idtac ].
apply Rle_trans with (Rabs (x * alpha - zH)); [ apply Rabs_triang_inv | idtac ].
pattern (FtoRradix zH) at 1 in |- *; rewrite <- H2.
unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with real zarith.
fold radix FtoRradix in |- *.
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 (INR 2); auto with real arith.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith real.
unfold Fulp, radix in |- *; rewrite Fexp_u with b prec N alpha x u;
auto with real zarith; fold radix in |- *.
apply Rle_trans with (2%nat * Rabs zH * (2%nat * (alpha * gamma) - 1))%R;
[ idtac | rewrite Rabs_mult; rewrite (Rabs_right gamma); try apply Rle_ge; auto with real;
right; ring ].
apply
Rle_trans
with (powerRZ radix (- N) * (2%nat * (2%nat * (alpha * gamma) - 1)))%R.
apply Rle_trans with (powerRZ radix (- N) * 1)%R; auto with real.
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_reg_l with (/ INR 2)%R; auto with real arith.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real arith.
ring_simplify.
apply Rplus_le_reg_l with 1%R.
apply Rmult_le_reg_l with (/ INR 2)%R; auto with real arith.
apply Rle_trans with (/ 2%nat * 2%nat * (alpha * gamma))%R;
[ idtac | right; ring ].
rewrite Rinv_l; auto with real arith.
apply Rplus_le_reg_l with (-1)%R.
apply Rle_trans with (- (1 - alpha * gamma))%R; [ idtac | right; ring ].
apply Rle_trans with (- powerRZ radix (-2))%R.
right; simpl in |- *; field; auto with real arith zarith.
apply Ropp_le_contravar.
apply Rle_trans with (Rabs (1 - alpha * gamma)); [ apply RRle_abs | idtac ].
apply Rle_trans with (powerRZ radix (q - prec)).
unfold FtoRradix, radix in |- *; apply delta_inf with b; auto with zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (Rabs zH * (2%nat * (2%nat * (alpha * gamma) - 1)))%R;
[ apply Rmult_le_compat_r | right; ring ].
apply Rmult_le_pos; auto with real arith zarith.
apply Rplus_le_reg_l with (-1)%R.
ring_simplify (-1 + 0)%R; apply Rle_trans with (- (2 * (1 - alpha * gamma)))%R;
[ idtac | right; simpl in |- *; ring ].
apply Ropp_le_contravar; apply Rmult_le_reg_l with (/ 2)%R; auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
apply Rle_trans with (1 - alpha * gamma)%R; auto with real.
apply Rle_trans with (Rabs (1 - alpha * gamma)); [ apply RRle_abs | idtac ].
apply Rle_trans with (powerRZ radix (q - prec)).
unfold FtoRradix, radix in |- *; apply delta_inf with b; auto with zarith.
apply Rle_trans with (powerRZ radix (-1));
[ apply Rle_powerRZ; auto with real zarith | idtac ].
right; simpl in |- *; field; auto with real zarith.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; simpl; rewrite <- H3.
apply Rle_trans with (1 * powerRZ 2 (Fexp zH))%R; [ right; simpl ; ring | idtac ].
apply Rmult_le_compat_r; auto with real zarith.
cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith.
apply LtR0Fnum with radix; auto with real zarith.
rewrite Fabs_correct; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; 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; auto with real.
rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
apply Rle_trans with (x*0)%R; auto with real.
assert (zH <= 0)%R; auto with real.
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 Rle_trans with ((-x)*0)%R; auto with real.
elim H; intros; split.
exists (Fminus radix x (Fmult zH gamma)).
split;
[ rewrite H2; unfold FtoRradix in |- *; rewrite Fminus_correct;
auto with zarith; rewrite Fmult_correct; auto with zarith;
ring
| auto ].
rewrite H2; unfold FtoRradix; rewrite <- Fmult_correct; auto with zarith.
apply Rle_lt_trans with (1:=H6).
unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
fold FtoRradix; rewrite Rabs_mult; rewrite (Rabs_right gamma).
2: apply Rle_ge; auto with real.
apply Rlt_le_trans with (powerRZ radix (q-Zsucc N)*powerRZ radix ((prec-q)+Fexp gamma))%R.
apply Rlt_le_trans with (powerRZ radix (q - Zsucc N)* gamma)%R.
apply Rmult_lt_compat_r; auto with real.
fold FtoRradix; rewrite <- H2; exact H'.
apply Rmult_le_compat_l; auto with real zarith.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
elim gammaNormal; intros T1 T2; elim T1; intros T3 T4.
apply Rle_trans with (Rabs (Fnum gamma));[apply RRle_abs|rewrite Rabs_Zabs].
apply Rle_trans with (Zpos (vNum bmoinsq)); auto with real zarith float.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_minus1; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
exists
(Float
(Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec))) (
- N)).
cut
(zH1 =
Float
(Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec))) (
- N) :>R); [ intros V | idtac ].
split; [ auto | idtac ].
split; [ simpl in |- *; auto | idtac ].
split.
apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
apply Rle_lt_trans with (Rabs (FtoRradix zH1)).
right; rewrite V; unfold FtoRradix, Fabs, FtoR.
apply trans_eq with (Rabs ((Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec)))%Z*powerRZ radix (-N))); auto with real.
rewrite Rabs_mult.
rewrite Rabs_right with (powerRZ radix (-N)); try apply Rle_ge; auto with real zarith.
rewrite Rabs_Zabs; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
replace (- N + Zpred q)%Z with (q - Zsucc N)%Z; auto;
unfold Zsucc, Zpred in |- *; ring.
rewrite <- V.
assert (0 <= Rabs zH1)%R; auto with real.
case H; auto; intros.
absurd (Rabs zH1 =0)%R; auto with real.
apply Rabs_no_R0; auto with real.
unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with zarith.
rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;
unfold FtoR in |- *.
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 ].
unfold Zminus in |- *; rewrite plus_IZR; rewrite Ropp_Ropp_IZR;
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
rewrite Fexp_u with b prec N alpha x u; auto with zarith.
replace (Zpred (Zpred (prec + - N))) with (-N + pred (pred prec))%Z.
rewrite powerRZ_add; auto with real zarith.
simpl; ring.
rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith.
unfold Zpred; ring.
Qed.
End Total.
(alpha * gamma <= 1)%R ->
ex (fun u : float => FtoRradix u = (x - zH1 * gamma)%R /\ Fbounded b u)
/\ (Rabs (x-zH1*gamma) < powerRZ radix (prec-N+Fexp gamma))%R.
assert (J:(- dExp b <= Zsucc q + - (Fexp alpha + (prec + prec)))%Z).
assert (prec-1+Fexp alpha <= dExp b+q-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 + q - prec))); auto with real.
intros V.
absurd (powerRZ radix (- dExp b + prec - q+1) <= gamma)%R.
apply Rlt_not_le.
assert (exists f:float, Fbounded bmoinsq f /\
(FtoRradix f= powerRZ radix (- dExp b+prec-q))%R).
exists (Float 1 (-dExp b+prec-q)).
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-q)
(Closest bmoinsq radix) (/alpha)%R; auto with real zarith float.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
apply ClosestRoundedModeP with (prec-q); auto with zarith.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq; auto.
fold FtoRradix; rewrite I2.
apply Rle_trans with (/(powerRZ radix (dExp b + q - prec)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (dExp b + q - prec))%Z with (- dExp b + prec - q)%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.
intros G.
case (Req_dec zH1 0); intros H1.
split.
exists 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.
ring_simplify (2*1)%R; 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
((-q-2+prec) +Fexp alpha)%Z;[idtac|
rewrite gamma_exp with b prec q alpha gamma;
auto with zarith; unfold Zsucc; ring].
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;ring_simplify.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith; 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.
case (Rle_or_lt (powerRZ radix (q - Zsucc N)) (Rabs zH1)); intros H'.
cut
(exists k : Z,
(exists 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 q k alpha (x * alpha - zH)%R;
auto with zarith real arith.
apply Zle_trans with (1 := H4); auto with zarith.
assert (1 < Zabs (Zsucc (k+N)))%Z; auto with zarith.
rewrite Zabs_absolu; auto with zarith.
rewrite Zabs_eq in H; auto with zarith.
apply Zplus_le_reg_l with (- Zsucc N)%Z.
replace (- Zsucc N + q)%Z with (q - 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.
fold radix FtoRradix in |- *; apply Rle_trans with (2 := H');
auto with real zarith.
apply Rle_powerRZ; unfold radix in |- *; auto with real zarith.
cut
(exists zH : float,
FtoRradix zH1 = zH /\
Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred q))%R /\ (0 < Rabs zH)%R).
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.
assert ((Fbounded b (Fminus radix x (Fmult zH gamma))
/\ (Rabs (x - (Fmult zH gamma)) <= Rabs (Fmult zH gamma))%R)).
apply Sterbenzter; auto with zarith.
split; unfold Fmult in |- *; simpl in |- *.
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs; rewrite Rmult_IZR;
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
replace (Z_of_nat prec) with (q + (prec - q)%nat)%Z;
[ rewrite powerRZ_add | rewrite inj_minus1 ];
auto with arith zarith real.
rewrite Rabs_mult; apply Rmult_le_0_lt_compat; auto with real.
rewrite Rabs_Zabs; apply Rlt_trans with (1 := H4);
auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum bmoinsq)));
auto with real zarith.
rewrite Faux.Rabsolu_Zabs; elim gammaNormal; intros T1 T2; elim T1;
intros T3 T4; auto with real zarith.
right; unfold bmoinsq in |- *; rewrite vNum_eq_Zpower_bmoinsq;
auto with real zarith.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
assert (- dExp b + prec -q + N - 1 < prec-q + Fexp gamma)%Z; auto with zarith.
apply Zle_lt_trans with (- dExp b + prec -q + Zmax 1 (N - 1))%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.
rewrite minus_Zminus_precq; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *;
apply Rmult_le_reg_l with alpha; auto with real.
rewrite Rabs_mult; rewrite Rabs_right with gamma; try apply Rle_ge; auto with real.
apply Rle_trans with (/ 2%nat * Rabs zH * (alpha * gamma))%R;
[ right; ring | idtac ].
apply Rle_trans with (/ 2%nat * Rabs zH * 1)%R;
[ apply Rmult_le_compat_l; auto | idtac ].
apply Rmult_le_pos; auto with real zarith arith real.
apply Rplus_le_reg_l with (/ 2%nat * Rabs zH - alpha * Rabs x)%R.
ring_simplify.
apply Rle_trans with (Rabs zH - Rabs x * alpha)%R; [ right | idtac ].
simpl; field; auto with real.
replace (Rabs x*alpha)%R with (Rabs (x*alpha));[idtac|rewrite Rabs_mult;
rewrite Rabs_right with alpha; try apply Rle_ge; auto with real].
apply Rle_trans with (Rabs (zH - x * alpha)); [ apply Rabs_triang_inv | idtac ].
rewrite <- H2; unfold FtoRradix, radix in |- *;
rewrite zH1_eq with b prec N alpha x u zH1; auto with real zarith.
fold radix FtoRradix in |- *; rewrite <- Rabs_Ropp.
replace
(- (u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))) - x * alpha))%R
with (3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha - u)%R;
[ idtac | ring ].
apply Rmult_le_reg_l with (INR 2); auto with real arith.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith.
unfold Fulp, radix in |- *; rewrite Fexp_u with b prec N alpha x u;
auto with real zarith.
unfold FtoRradix, radix in |- *;
rewrite <- zH1_eq with b prec N alpha x u zH1; auto with real zarith.
fold radix FtoRradix in |- *; rewrite H2; rewrite <- H3; fold radix in |- *;
unfold FtoRradix, FtoR in |- *; auto with real zarith.
apply Rle_trans with (1 * (1 * powerRZ radix (Fexp zH)))%R;
[ right; ring | idtac ].
rewrite Rabs_mult.
rewrite Rabs_right with (powerRZ radix (Fexp zH)); try apply Rle_ge; auto with real zarith.
apply Rmult_le_compat_l; auto with real; apply Rmult_le_compat_r;
auto with real zarith.
rewrite Rabs_Zabs.
cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
apply Zlt_le_trans with (Fnum (Fabs (zH))); auto with zarith.
apply LtR0Fnum with radix; auto with real zarith.
rewrite Fabs_correct; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in |- *;
apply Rmult_le_reg_l with alpha; auto with real.
apply Rplus_le_reg_l with (- Rabs zH)%R.
replace (alpha*Rabs x)%R with (Rabs (x*alpha));[idtac|
rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real].
apply Rle_trans with (Rabs (x * alpha) - Rabs zH)%R; [ right; ring | idtac ].
apply Rle_trans with (Rabs (x * alpha - zH)); [ apply Rabs_triang_inv | idtac ].
pattern (FtoRradix zH) at 1 in |- *; rewrite <- H2.
unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with real zarith.
fold radix FtoRradix in |- *.
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 (INR 2); auto with real arith.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith real.
unfold Fulp, radix in |- *; rewrite Fexp_u with b prec N alpha x u;
auto with real zarith; fold radix in |- *.
apply Rle_trans with (2%nat * Rabs zH * (2%nat * (alpha * gamma) - 1))%R;
[ idtac | rewrite Rabs_mult; rewrite (Rabs_right gamma); try apply Rle_ge; auto with real;
right; ring ].
apply
Rle_trans
with (powerRZ radix (- N) * (2%nat * (2%nat * (alpha * gamma) - 1)))%R.
apply Rle_trans with (powerRZ radix (- N) * 1)%R; auto with real.
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_reg_l with (/ INR 2)%R; auto with real arith.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real arith.
ring_simplify.
apply Rplus_le_reg_l with 1%R.
apply Rmult_le_reg_l with (/ INR 2)%R; auto with real arith.
apply Rle_trans with (/ 2%nat * 2%nat * (alpha * gamma))%R;
[ idtac | right; ring ].
rewrite Rinv_l; auto with real arith.
apply Rplus_le_reg_l with (-1)%R.
apply Rle_trans with (- (1 - alpha * gamma))%R; [ idtac | right; ring ].
apply Rle_trans with (- powerRZ radix (-2))%R.
right; simpl in |- *; field; auto with real arith zarith.
apply Ropp_le_contravar.
apply Rle_trans with (Rabs (1 - alpha * gamma)); [ apply RRle_abs | idtac ].
apply Rle_trans with (powerRZ radix (q - prec)).
unfold FtoRradix, radix in |- *; apply delta_inf with b; auto with zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (Rabs zH * (2%nat * (2%nat * (alpha * gamma) - 1)))%R;
[ apply Rmult_le_compat_r | right; ring ].
apply Rmult_le_pos; auto with real arith zarith.
apply Rplus_le_reg_l with (-1)%R.
ring_simplify (-1 + 0)%R; apply Rle_trans with (- (2 * (1 - alpha * gamma)))%R;
[ idtac | right; simpl in |- *; ring ].
apply Ropp_le_contravar; apply Rmult_le_reg_l with (/ 2)%R; auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
apply Rle_trans with (1 - alpha * gamma)%R; auto with real.
apply Rle_trans with (Rabs (1 - alpha * gamma)); [ apply RRle_abs | idtac ].
apply Rle_trans with (powerRZ radix (q - prec)).
unfold FtoRradix, radix in |- *; apply delta_inf with b; auto with zarith.
apply Rle_trans with (powerRZ radix (-1));
[ apply Rle_powerRZ; auto with real zarith | idtac ].
right; simpl in |- *; field; auto with real zarith.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; simpl; rewrite <- H3.
apply Rle_trans with (1 * powerRZ 2 (Fexp zH))%R; [ right; simpl ; ring | idtac ].
apply Rmult_le_compat_r; auto with real zarith.
cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith.
apply LtR0Fnum with radix; auto with real zarith.
rewrite Fabs_correct; auto with real zarith.
unfold FtoRradix; rewrite Fmult_correct; auto with zarith; 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; auto with real.
rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
apply Rle_trans with (x*0)%R; auto with real.
assert (zH <= 0)%R; auto with real.
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 Rle_trans with ((-x)*0)%R; auto with real.
elim H; intros; split.
exists (Fminus radix x (Fmult zH gamma)).
split;
[ rewrite H2; unfold FtoRradix in |- *; rewrite Fminus_correct;
auto with zarith; rewrite Fmult_correct; auto with zarith;
ring
| auto ].
rewrite H2; unfold FtoRradix; rewrite <- Fmult_correct; auto with zarith.
apply Rle_lt_trans with (1:=H6).
unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
fold FtoRradix; rewrite Rabs_mult; rewrite (Rabs_right gamma).
2: apply Rle_ge; auto with real.
apply Rlt_le_trans with (powerRZ radix (q-Zsucc N)*powerRZ radix ((prec-q)+Fexp gamma))%R.
apply Rlt_le_trans with (powerRZ radix (q - Zsucc N)* gamma)%R.
apply Rmult_lt_compat_r; auto with real.
fold FtoRradix; rewrite <- H2; exact H'.
apply Rmult_le_compat_l; auto with real zarith.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
elim gammaNormal; intros T1 T2; elim T1; intros T3 T4.
apply Rle_trans with (Rabs (Fnum gamma));[apply RRle_abs|rewrite Rabs_Zabs].
apply Rle_trans with (Zpos (vNum bmoinsq)); auto with real zarith float.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_minus1; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
exists
(Float
(Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec))) (
- N)).
cut
(zH1 =
Float
(Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec))) (
- N) :>R); [ intros V | idtac ].
split; [ auto | idtac ].
split; [ simpl in |- *; auto | idtac ].
split.
apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
apply Rle_lt_trans with (Rabs (FtoRradix zH1)).
right; rewrite V; unfold FtoRradix, Fabs, FtoR.
apply trans_eq with (Rabs ((Fnum (Fnormalize radix b prec u) -
3%nat * Zpower_nat radix (pred (pred prec)))%Z*powerRZ radix (-N))); auto with real.
rewrite Rabs_mult.
rewrite Rabs_right with (powerRZ radix (-N)); try apply Rle_ge; auto with real zarith.
rewrite Rabs_Zabs; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
replace (- N + Zpred q)%Z with (q - Zsucc N)%Z; auto;
unfold Zsucc, Zpred in |- *; ring.
rewrite <- V.
assert (0 <= Rabs zH1)%R; auto with real.
case H; auto; intros.
absurd (Rabs zH1 =0)%R; auto with real.
apply Rabs_no_R0; auto with real.
unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with zarith.
rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;
unfold FtoR in |- *.
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 ].
unfold Zminus in |- *; rewrite plus_IZR; rewrite Ropp_Ropp_IZR;
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
rewrite Fexp_u with b prec N alpha x u; auto with zarith.
replace (Zpred (Zpred (prec + - N))) with (-N + pred (pred prec))%Z.
rewrite powerRZ_add; auto with real zarith.
simpl; ring.
rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith.
unfold Zpred; ring.
Qed.
End Total.