Library Float.FnElem.FIA64elem
Require Export AllFloat.
Section FulpRinv.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Theorem Fabs_Fexp : ∀ f : float, Fexp f = Fexp (Fabs f).
intros f; unfold Fabs in |- *; simpl in |- *; auto.
Qed.
Theorem Fulp_pow :
∀ (f : float) (n : Z),
(- dExp b ≤ n + Zsucc (- precision))%Z →
Fbounded b f →
Rabs f = powerRZ radix n :>R →
Fulp b radix precision f = powerRZ radix (n + Zsucc (- precision)).
intros f n H1 H2 H3; unfold Fulp in |- ×.
rewrite Fabs_Fexp.
replace (Fabs (Fnormalize radix b precision f)) with
(Float (Zpower_nat radix (pred precision)) (n + Zsucc (- precision)));
[ simpl in |- *; auto with real | idtac ].
apply FcanonicUnique with radix b precision; auto with zarith float.
unfold Fcanonic in |- *; left; split; [ split | idtac ]; simpl in |- *; auto.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
pattern precision at 1 in |- *; replace precision with (1 + pred precision);
auto with arith zarith.
rewrite Fabs_correct; auto with zarith.
rewrite FnormalizeCorrect; auto; fold FtoRradix in |- *; rewrite H3.
unfold FtoRradix, FtoR in |- *; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
unfold Zsucc in |- *; repeat rewrite <- Zplus_assoc.
rewrite inj_pred; auto with zarith.
unfold Zpred.
ring_simplify (precision + -1 + (n + (- precision + 1)))%Z; auto with zarith.
Qed.
Theorem Fulp_R1 :
∀ f : float,
(- dExp b ≤ Zsucc (- precision))%Z →
Fbounded b f →
f = 1%R :>R →
Fulp b radix precision f = powerRZ radix (Zsucc (- precision)).
intros f H H' H1.
replace (Zsucc (- precision)) with (0 + Zsucc (- precision))%Z;
[ idtac | ring ].
apply Fulp_pow; auto with real zarith arith.
rewrite H1; rewrite Rabs_R1; auto with real zarith arith.
Qed.
Section FulpRinv.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Theorem Fabs_Fexp : ∀ f : float, Fexp f = Fexp (Fabs f).
intros f; unfold Fabs in |- *; simpl in |- *; auto.
Qed.
Theorem Fulp_pow :
∀ (f : float) (n : Z),
(- dExp b ≤ n + Zsucc (- precision))%Z →
Fbounded b f →
Rabs f = powerRZ radix n :>R →
Fulp b radix precision f = powerRZ radix (n + Zsucc (- precision)).
intros f n H1 H2 H3; unfold Fulp in |- ×.
rewrite Fabs_Fexp.
replace (Fabs (Fnormalize radix b precision f)) with
(Float (Zpower_nat radix (pred precision)) (n + Zsucc (- precision)));
[ simpl in |- *; auto with real | idtac ].
apply FcanonicUnique with radix b precision; auto with zarith float.
unfold Fcanonic in |- *; left; split; [ split | idtac ]; simpl in |- *; auto.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
pattern precision at 1 in |- *; replace precision with (1 + pred precision);
auto with arith zarith.
rewrite Fabs_correct; auto with zarith.
rewrite FnormalizeCorrect; auto; fold FtoRradix in |- *; rewrite H3.
unfold FtoRradix, FtoR in |- *; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
unfold Zsucc in |- *; repeat rewrite <- Zplus_assoc.
rewrite inj_pred; auto with zarith.
unfold Zpred.
ring_simplify (precision + -1 + (n + (- precision + 1)))%Z; auto with zarith.
Qed.
Theorem Fulp_R1 :
∀ f : float,
(- dExp b ≤ Zsucc (- precision))%Z →
Fbounded b f →
f = 1%R :>R →
Fulp b radix precision f = powerRZ radix (Zsucc (- precision)).
intros f H H' H1.
replace (Zsucc (- precision)) with (0 + Zsucc (- precision))%Z;
[ idtac | ring ].
apply Fulp_pow; auto with real zarith arith.
rewrite H1; rewrite Rabs_R1; auto with real zarith arith.
Qed.
Result to complete cases of Theorem 6.8 defined p. 92
Theorem FulpRinv_div :
∀ P (f u : float) (n : Z),
RoundedModeP b radix P →
Fbounded b f →
Fbounded b u →
P (/ f)%R u →
Rabs f = powerRZ radix n :>R →
(- dExp b + Zpred precision ≤ n)%Z →
(n ≤ dExp b + Zsucc (- precision))%Z →
(Fulp b radix precision f × Fulp b radix precision u)%R =
Rsqr (powerRZ radix (Zsucc (- precision))).
intros P f u n H1 Ff Fu H2 H3 H4 H5.
rewrite Fulp_pow with f n; auto.
rewrite Fulp_pow with u (- n)%Z; auto.
unfold Rsqr in |- *; repeat rewrite <- powerRZ_add; auto with real zarith.
replace (n + Zsucc (- precision) + (- n + Zsucc (- precision)))%Z with
(Zsucc (- precision) + Zsucc (- precision))%Z; auto with real;
ring.
replace (- n + Zsucc (- precision))%Z with (- (n + - Zsucc (- precision)))%Z;
[ auto with zarith | ring ].
cut (ProjectorP b radix P);
[ unfold ProjectorP in |- *; intros H' | apply RoundedProjector; auto ].
apply sym_eq; apply trans_eq with (FtoRradix (Float 1 (- n))).
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
case (Rle_or_lt 0 f); intros H6.
rewrite Rabs_right;
[ unfold FtoRradix in |- *; apply H' | apply Rle_ge; auto ].
repeat (split; simpl in |- *; auto with zarith).
rewrite pGivesBound; replace 1%Z with (Zpower_nat radix 0);
auto with zarith arith.
replace (FtoR radix (Float 1 (- n))) with (/ FtoRradix f)%R; auto.
rewrite <- (Rabs_right (FtoRradix f)); [ idtac | apply Rle_ge; auto ].
rewrite H3; rewrite Rinv_powerRZ; auto with zarith real.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
unfold FtoRradix in |- *;
apply RleRoundedR0 with b precision P (/ FtoRradix f)%R;
auto with real zarith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real.
case H6; auto with real.
intros H7; absurd (0%R = powerRZ radix n); auto with real zarith.
rewrite <- Rabs_R0; rewrite H7; auto.
rewrite Faux.Rabsolu_left1.
replace (FtoRradix u) with (- Float 1 (- n))%R; [ ring | idtac ].
unfold FtoRradix in |- *; rewrite <- Fopp_correct; apply H'; auto.
repeat (split; simpl in |- *; auto with zarith).
rewrite pGivesBound; replace 1%Z with (Zpower_nat radix 0);
auto with zarith arith.
replace (FtoR radix (Fopp (Float 1 (- n)))) with (/ FtoRradix f)%R; auto.
rewrite <- (Ropp_involutive (FtoRradix f));
rewrite <- (Rabs_left (FtoRradix f)); auto.
rewrite <- Ropp_inv_permute; [ idtac | apply Rabs_no_R0; auto with real ].
rewrite H3; rewrite Rinv_powerRZ; auto with zarith real.
rewrite Fopp_correct; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
unfold FtoRradix in |- *;
apply RleRoundedLessR0 with b precision P (/ FtoRradix f)%R;
auto with real zarith.
apply Zplus_le_reg_r with (Zpred precision); auto with zarith.
Qed.
Theorem boundedNorMinGivesExp2 :
∀ (x : Z) (p : float),
Fbounded b p →
(- dExp b ≤ x)%Z →
(Float (nNormMin radix precision) x ≤ Rabs p)%R →
(Rabs p ≤ Float (pPred (vNum b)) x)%R →
Fexp (Fnormalize radix b precision p) = x :>Z.
intros x p H1 H2 H3 H4.
case (Rle_or_lt 0 p); intros H5.
apply boundedNorMinGivesExp; auto with arith; fold FtoRradix in |- *;
rewrite <- (Rabs_right (FtoRradix p)); auto with real.
rewrite <- (Fopp_Fopp p); rewrite Fnormalize_Fopp; auto with arith.
apply trans_eq with (Fexp (Fnormalize radix b precision (Fopp p)));
auto with float.
apply boundedNorMinGivesExp; auto with arith float; rewrite Fopp_correct;
rewrite <- Rabs_left; auto with real.
Qed.
Theorem 6.9 defined p. 93, used for example p. 121 and p. 131
Theorem FulpRinv_div_not :
∀ P (f u : float),
RoundedModeP b radix P →
Fbounded b f →
Fbounded b u →
f ≠ 0%R :>R →
P (/ f)%R u →
(∀ n : Z, Rabs f ≠ powerRZ radix n :>R) →
Fnormal radix b f →
(- dExp b ≤ 1 + (- Fexp f + (- precision + - precision)))%Z →
(radix × (Fulp b radix precision f × Fulp b radix precision u))%R =
Rsqr (powerRZ radix (Zsucc (- precision))).
intros P f u H1 Ff Fu H0 H2 H3 Nf H'; unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith; [ idtac | left; auto ].
pattern (IZR radix) at 1 in |- *; replace (IZR radix) with (powerRZ radix 1);
auto with real.
unfold Rsqr in |- *; repeat rewrite <- powerRZ_add; auto with zarith real.
replace (1 + (Fexp f + Fexp (Fnormalize radix b precision u)))%Z with
(Zsucc (- precision) + Zsucc (- precision))%Z; auto with real.
replace (Fexp (Fnormalize radix b precision u)) with
(1 + (- Fexp f + (- precision + - precision)))%Z.
unfold Zsucc in |- *; ring; auto with zarith.
apply sym_eq; apply boundedNorMinGivesExp2; auto with zarith arith float real.
unfold FtoRradix in |- *;
apply RoundAbsMonotonel with b precision P (/ FtoRradix f)%R;
auto.
split; auto with zarith float.
simpl in |- ×.
rewrite Zabs_eq; auto with zarith float.
apply ZltNormMinVnum; auto with arith.
unfold nNormMin in |- *; auto with zarith arith.
apply Rle_trans with (powerRZ radix (- Fexp f + - precision)).
unfold nNormMin in |- ×.
unfold FtoRradix, FtoR in |- ×.
replace
(Fnum
(Float (Zpower_nat radix (pred precision))
(1 + (- Fexp f + (- precision + - precision))))) with
(Zpower_nat radix (pred precision)); auto.
replace
(Fexp
(Float (Zpower_nat radix (pred precision))
(1 + (- Fexp f + (- precision + - precision))))) with
(1 + (- Fexp f + (- precision + - precision)))%Z;
auto.
rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- powerRZ_add; auto with zarith real.
replace (pred precision + (1 + (- Fexp f + (- precision + - precision))))%Z
with (- Fexp f + - precision)%Z; auto with real.
replace (Z_of_nat (pred precision)) with (Zpred precision);
[ unfold Zpred in |- *; ring | idtac ].
apply sym_eq; apply inj_pred; auto with arith.
replace (- Fexp f + - precision)%Z with (- (Fexp f + precision))%Z;
[ idtac | ring ].
rewrite <- Rinv_powerRZ; auto with real zarith.
rewrite Rabs_Rinv; auto.
apply Rle_Rinv; auto with real.
apply Rabs_pos_lt; auto.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; simpl in |- *; rewrite powerRZ_add;
auto with real zarith.
rewrite Rmult_comm; apply Rmult_le_compat_l; auto with real zarith float.
apply Rle_trans with (IZR (Zpos (vNum b)));
auto with real zarith float.
right; rewrite pGivesBound; auto with real zarith float.
apply Zpower_nat_Z_powerRZ.
unfold FtoRradix in |- *;
apply RoundAbsMonotoner with b precision P (/ FtoRradix f)%R;
auto.
split; auto with zarith float.
simpl in |- ×.
rewrite Zabs_eq; auto with zarith float.
unfold pPred in |- ×.
auto with zarith.
auto with zarith arith float.
unfold pPred in |- ×.
auto with zarith arith float.
apply
Rle_trans
with (/ (Zsucc (nNormMin radix precision) × powerRZ radix (Fexp f)))%R.
rewrite Rabs_Rinv; auto.
apply Rle_Rinv; auto with real.
apply Rmult_lt_0_compat; auto with real zarith float.
unfold nNormMin in |- *; auto with real zarith float.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR in |- *; simpl in |- ×.
apply Rmult_le_compat_r; auto with real zarith.
elim Nf; intros H'1 H'2.
apply Rle_IZR.
apply Zlt_le_succ.
case (Zle_lt_or_eq (nNormMin radix precision) (Zabs (Fnum f)));
auto with zarith.
apply Zmult_le_reg_r with radix; auto with zarith.
replace (nNormMin radix precision × radix)%Z with (Zpos (vNum b)).
replace (Zabs (Fnum f) × radix)%Z with (Zabs (radix × Fnum f)); auto.
rewrite Zabs_Zmult; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zmult_comm; rewrite pGivesBound; unfold nNormMin in |- *;
auto with zarith arith.
replace precision with (S (pred precision)); auto with zarith arith.
intros H'3.
absurd (Rabs (FtoRradix f) = powerRZ radix (pred precision + Fexp f) :>R).
apply H3; auto.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs in |- *; simpl in |- ×.
rewrite powerRZ_add; auto with real zarith.
rewrite <- H'3; unfold nNormMin in |- *; auto with zarith real.
rewrite Zpower_nat_Z_powerRZ; auto with real.
unfold FtoR in |- ×.
replace
(Fnum
(Float (pPred (vNum b)) (1 + (- Fexp f + (- precision + - precision)))))
with (pPred (vNum b)); auto.
replace
(Fexp
(Float (pPred (vNum b)) (1 + (- Fexp f + (- precision + - precision)))))
with (1 + (- Fexp f + (- precision + - precision)))%Z;
auto.
cut (Zsucc (nNormMin radix precision) ≠ 0%R :>R);
[ intros H'1 | unfold nNormMin in |- *; auto with real zarith arith ].
rewrite Rinv_mult_distr; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (1 + (- Fexp f + (- precision + - precision)))%Z with
(- Fexp f + (1 + (- precision + - precision)))%Z;
[ idtac | ring ].
rewrite powerRZ_add; auto with real zarith.
rewrite Rmult_comm with (r1 := powerRZ radix (- Fexp f)).
rewrite <- Rmult_assoc.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with (IZR (Zsucc (nNormMin radix precision)));
auto with real zarith.
unfold nNormMin in |- *; auto with real zarith arith.
rewrite Rinv_r; auto.
unfold Zsucc in |- *; rewrite plus_IZR.
unfold nNormMin in |- *; rewrite Zpower_nat_Z_powerRZ.
unfold pPred in |- ×.
unfold Zpred in |- *; rewrite plus_IZR.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
replace (IZR 1) with 1%R; auto with real.
replace (IZR (-1)) with (-1)%R; auto with real.
ring_simplify.
repeat rewrite <- powerRZ_add; auto with zarith real.
replace (Z_of_nat (pred precision)) with (Zpred precision);
[ unfold Zpred in |- × | apply sym_eq; apply inj_pred; auto with arith ].
ring_simplify (precision + -1 + precision + (1 + (- precision + - precision)))%Z.
ring_simplify (precision + -1 + (1 + (- precision + - precision)))%Z.
ring_simplify (precision + (1 + (- precision + - precision)))%Z.
apply Rplus_le_reg_l with (-1)%R.
ring_simplify (-1 + 1)%R.
replace (powerRZ radix 0) with 1%R; auto.
ring_simplify.
apply
Rle_trans
with
(powerRZ radix (- precision) +
- powerRZ radix (1 + (- precision + - precision)))%R.
apply Rplus_le_reg_l with (powerRZ radix (1 + (- precision + - precision))).
ring_simplify.
auto with real zarith arith.
unfold Rminus;apply Rplus_le_compat_r.
replace (-1×precision)%Z with (-precision)%Z; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with ((radix + -1) × powerRZ radix (- precision))%R;
[ idtac | simpl in |- *; right; ring ].
apply Rle_trans with (1 × powerRZ radix (- precision))%R; auto with real.
apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with 1%R.
ring_simplify (1 + (radix + -1))%R; auto with real arith zarith.
replace 2%R with (IZR 2); auto with zarith real.
Qed.
End FulpRinv.