Library Float.FnElem.FArgReduct
IEEE754 : FArgReduct
Sylvie Boldo
Sylvie Boldo
Require Export FnormI.
Require Export Classical.
Section SterbenzApprox.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables (b1 : Fbound) (b2 : Fbound).
Variables (prec1 : nat) (prec2 : nat).
Hypothesis prec1MoreThanOne : 1 < prec1.
Hypothesis p1GivesBound : Zpos (vNum b1) = Zpower_nat radix prec1.
Hypothesis prec2MoreThanOne : 1 < prec2.
Hypothesis p2GivesBound : Zpos (vNum b2) = Zpower_nat radix prec2.
Theorem Rmin_1 : forall x y : R, (x <= y)%R -> Rmin x y = x.
intros x y H; unfold Rmin in |- *.
case (Rle_dec x y); auto with real.
Qed.
Theorem Rmin_2 : forall x y : R, (y <= x)%R -> Rmin x y = y.
intros x y H; unfold Rmin in |- *.
case (Rle_dec x y); auto with real.
Qed.
Theorem Rmin_eq : forall x : R, Rmin x x = x.
intros x; unfold Rmin in |- *.
case (Rle_dec x x); auto with real.
Qed.
Theorem Rdiv_Rle :
forall a b c d : R,
(0 < a)%R ->
(0 < b)%R ->
(0 < c)%R -> (0 < d)%R -> (a <= c)%R -> (d <= b)%R -> (a / b <= c / d)%R.
intros a b c d Ha Hb Hc Hd H1 H2; unfold Rdiv in |- *.
apply Rle_trans with (c * / b)%R; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rle_Rinv; auto with real.
Qed.
Theorem SterbenzApprox :
forall (rho : R) (x y : float),
(0 < rho)%R ->
IZR (Zpos (vNum b1)) = (rho * Zsucc (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 ->
exists u : float, u = (x - y)%R :>R /\ Fbounded b2 u.
intros rho x y Hrho Hrho' Hv0 Fx Fy H1 H2.
cut
(forall b : Fbound,
Z_of_nat
(vNumInf
(BoundI (pred (nat_of_P (vNum b))) (nat_of_P (vNum b))
(Zabs_nat (dExp b)))) = Zpred (Zpos (vNum b)));
[ intros V1 | idtac ].
2: intros b; apply trans_eq with (Z_of_nat (pred (nat_of_P (vNum b))));
[ simpl in |- *; auto | idtac ].
2: apply trans_eq with (Zpred (nat_of_P (vNum b)));
[ apply inj_pred; auto with zarith | idtac ].
2: rewrite inject_nat_convert with (Zpos (vNum b)) (vNum b);
auto with zarith arith.
cut
(forall b : Fbound,
Z_of_nat
(vNumSup
(BoundI (pred (nat_of_P (vNum b))) (nat_of_P (vNum b))
(Zabs_nat (dExp b)))) = Zpos (vNum b)); [ intros V2 | idtac ].
2: intros b; apply trans_eq with (Z_of_nat (nat_of_P (vNum b)));
[ simpl in |- *; auto | idtac ].
2: apply inject_nat_convert; auto with zarith arith.
elim
SterbenzApproxI_pos
with
radix
(BoundI (pred (nat_of_P (vNum b1))) (nat_of_P (vNum b1))
(Zabs_nat (dExp b1)))
(BoundI (pred (nat_of_P (vNum b2))) (nat_of_P (vNum b2))
(Zabs_nat (dExp b2)))
rho
x
y; auto with real zarith.
2: rewrite (V1 b1); rewrite (V1 b2); rewrite (V2 b1); rewrite (V2 b2).
2: repeat rewrite <- Zsucc_pred.
2: rewrite
Rmin_1
with
(x := (Zpos (vNum b1) / Zsucc (Zpos (vNum b2)))%R);
[ idtac | apply Rdiv_Rle; auto with real zarith ].
2: rewrite Rmin_2; [ rewrite Hrho' | idtac ].
2: unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_r;
auto with real zarith arith.
2: case
(Rle_or_lt (Zpos (vNum b1) / Zpos (vNum b2))
(Zsucc (Zpos (vNum b1)) / Zsucc (Zpos (vNum b2))));
intros H.
2: rewrite Rmin_1; auto with real; apply Rdiv_Rle; auto with real zarith.
2: rewrite Rmin_2; auto with real; apply Rdiv_Rle; auto with real zarith.
2: simpl; repeat rewrite <- Zabs_absolu.
2: repeat rewrite Zabs_eq; auto with zarith.
2: case (dExp b1); auto with zarith.
2: case (dExp b2); auto with zarith.
2: intros z Hz.
2: apply FoppBoundedI2 with (Zabs_nat (Zpower_nat radix (pred prec2)));
auto with zarith.
2: rewrite (V1 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: replace (radix * Zpower_nat radix (pred prec2))%Z with
(Zpower_nat radix prec2); auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
2: rewrite (V2 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
2: intros z Hz.
2: apply FoppBoundedI2 with (Zabs_nat (Zpower_nat radix (pred prec1)));
auto with zarith.
2: rewrite (V1 b1); rewrite p1GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: replace (radix * Zpower_nat radix (pred prec1))%Z with
(Zpower_nat radix prec1); auto with zarith arith.
2: pattern prec1 at 1 in |- *; replace prec1 with (1 + pred prec1);
auto with zarith arith.
2: rewrite (V2 b1); rewrite p1GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec1 at 1 in |- *; replace prec1 with (1 + pred prec1);
auto with zarith arith.
2: split; simpl in |- *; auto with zarith float.
2: split.
2: apply Zle_Zopp_Inv; rewrite Zopp_involutive;
apply Zle_trans with (Zabs (Fnum x)).
2: apply Zle_trans with (Zabs (- Fnum x)); auto with zarith.
2: rewrite Zabs_Zopp; auto with zarith.
2: rewrite inj_pred; auto with float zarith arith.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: apply Zle_trans with (Zabs (Fnum x)); auto with zarith float.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith float.
2: case (dExp b1); auto with zarith.
2: split; simpl in |- *; auto with zarith arith float.
2: split.
2: apply Zle_Zopp_Inv; rewrite Zopp_involutive;
apply Zle_trans with (Zabs (Fnum y)).
2: apply Zle_trans with (Zabs (- Fnum y)); auto with zarith float.
2: rewrite Zabs_Zopp; auto with zarith.
2: rewrite inj_pred; auto with float zarith arith.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: apply Zle_trans with (Zabs (Fnum y)); auto with zarith float.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith float.
2: case (dExp b1); auto with zarith.
intros u tmp; elim tmp; intros Hu1 Hu2; clear tmp.
elim
ReductRangeI
with
radix
(BoundI (pred (nat_of_P (vNum b2))) (nat_of_P (vNum b2))
(Zabs_nat (dExp b2)))
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))
(Zabs_nat (Zpower_nat radix (pred prec2)))
u; auto with real zarith.
2: rewrite (V2 b2);
apply trans_eq with (pred (nat_of_P (vNum b2)) + 1)%Z;
[ idtac | simpl in |- *; auto ].
2: rewrite inj_pred; auto with zarith.
2: rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith arith; unfold Zpred in |- *; ring.
2: rewrite (V2 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
intros v tmp; elim tmp; intros Hv1 Hv2; clear tmp.
exists v; split.
unfold FtoRradix in |- *; rewrite <- Hv2; rewrite Hu1; auto with real.
elim Hv1; intros tmp H3; elim tmp; intros H4 H5; clear tmp; split;
auto with zarith.
case (Zle_or_lt 0 (Fnum v)); intros H'.
rewrite Zabs_eq; auto with zarith.
replace (Zpos (vNum b2)) with
(Zsucc
(vNumSup
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))));
auto with zarith.
apply trans_eq with (Zsucc (pred (nat_of_P (vNum b2))));
[ simpl in |- *; auto | idtac ].
rewrite inj_pred; auto with zarith.
rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith; rewrite <- Zsucc_pred; auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
replace (Zpos (vNum b2)) with
(Zsucc
(vNumInf
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))));
auto with zarith.
apply trans_eq with (Zsucc (pred (nat_of_P (vNum b2))));
[ simpl in |- *; auto | idtac ].
rewrite inj_pred; auto with zarith.
rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith.
rewrite <- Zsucc_pred; auto.
apply Zle_trans with (2:=H3); simpl.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith;
case (dExp b2); auto with zarith.
Qed.
Theorem SterbenzApprox_weak_1 :
forall (rho : R) (x y : float),
(0 < rho)%R ->
IZR (Zpos (vNum b1)) = (rho * Zpos (vNum b2))%R ->
(- dExp b2 <= - dExp b1)%Z ->
Fbounded b1 x ->
Fbounded b1 y ->
(0 <= y)%R ->
(y <= x)%R ->
(x <= (1 + / rho) * y)%R ->
Fbounded b2
(Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y)).
intros rho x y H1 H2 H'' H3 H4 H5 H6 H7.
cut
(0 <=
Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y))%R;
[ intros Rle1 | idtac ].
2: rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- *.
2: unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
2: apply Rplus_le_reg_l with (r := FtoR radix y); auto.
2: fold FtoRradix in |- *; ring_simplify; auto with real.
cut
(Fexp
(Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y)) =
Fexp (Fnormalize radix b1 prec1 y)); [ intros He | idtac ].
2: unfold Fminus in |- *; simpl in |- *; apply Zmin_le2.
2: apply Fcanonic_Rle_Zle with radix b1 prec1; auto with real zarith float.
2: repeat rewrite FnormalizeCorrect; auto.
2: fold FtoRradix in |- *; repeat rewrite Rabs_right; auto with real.
2: apply Rle_ge; apply Rle_trans with (FtoRradix y); auto with real.
split.
rewrite Zabs_eq; [ idtac | apply LeR0Fnum with radix; auto with real zarith ].
apply Zlt_Rlt;
apply
Rle_lt_trans
with ((x - y) * powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)))%R.
right;
apply
trans_eq
with
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y) *
powerRZ radix
(-
Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y))))%R.
unfold FtoRradix, FtoR in |- *; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify
(Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y)) +
-
Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y)))%Z; simpl in |- *;
ring.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite <- FnormalizeCorrect with radix b1 prec1 x; auto.
rewrite <- FnormalizeCorrect with radix b1 prec1 y; auto.
rewrite He; ring.
apply
Rle_lt_trans
with
(/ rho * FtoRradix y *
powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with (FtoRradix y); auto.
ring_simplify (FtoRradix y + (FtoRradix x - FtoRradix y))%R.
apply Rle_trans with (1 := H7); right; ring.
apply Rle_lt_trans with (/ rho * Fnum (Fnormalize radix b1 prec1 y))%R.
unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix b1 prec1 y;
auto.
right; unfold FtoR in |- *.
apply
trans_eq
with
(/ rho *
(powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)) *
powerRZ radix (Fexp (Fnormalize radix b1 prec1 y))) *
Fnum (Fnormalize radix b1 prec1 y))%R.
ring.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify
(- Fexp (Fnormalize radix b1 prec1 y) +
Fexp (Fnormalize radix b1 prec1 y))%Z; simpl in |- *;
ring.
apply Rlt_le_trans with (/ rho * Zpos (vNum b1))%R.
apply Rmult_lt_compat_l; auto with real.
rewrite <- (Zabs_eq (Fnum (Fnormalize radix b1 prec1 y)));
auto with real zarith float.
apply LeR0Fnum with radix; auto with zarith real.
rewrite FnormalizeCorrect; auto with real float zarith.
right; rewrite H2; rewrite <- Rmult_assoc; rewrite Rinv_l;
[ ring | auto with zarith real ].
apply Zle_trans with (1 := H''); auto with zarith; rewrite He;
auto with float zarith.
Qed.
Theorem SterbenzApprox2 :
forall (rho : R) (x y : float),
(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)).
intros rho x y Hrho Hv1 Hv2 F1x F1y H1 H2.
cut (0 < 1 + / rho)%R; [ intros H' | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
cut (y <= (1 + / rho) * x)%R; [ intros H'1 | idtac ].
2: apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
2: rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; ring_simplify (1 * x)%R;
auto with real.
cut (0 <= y)%R; [ intros H'2 | idtac ].
2: apply Rmult_le_reg_l with (1 + / rho - / (1 + / rho))%R.
2: apply Rplus_lt_reg_r with (/ (1 + / rho))%R.
2: ring_simplify.
2: apply Rmult_lt_reg_l with (1 + / rho)%R; auto with real.
2: rewrite Rinv_r; auto with real.
2: apply Rlt_le_trans with (1+(/rho+(/rho+/rho*/rho)))%R;[idtac|right; ring].
2: apply Rle_lt_trans with (1 + (0 + (0 + 0)))%R;
[ right; ring | apply Rplus_lt_compat_l; auto with real ].
2: apply Rplus_lt_compat; auto with real.
2: apply Rplus_lt_compat; auto with real.
2: apply Rmult_lt_0_compat; auto with real.
2: ring_simplify ((1 + / rho - / (1 + / rho)) * 0)%R.
2: apply Rplus_le_reg_l with (/ (1 + / rho) * FtoRradix y)%R.
2: ring_simplify; auto with real.
2: apply Rle_trans with (FtoRradix x); auto with real.
2: apply Rle_trans with (1 := H2); right; ring.
cut (0 <= x)%R; [ intros H'3 | idtac ].
2: apply Rle_trans with (2 := H1); apply Rmult_le_pos; auto with real.
case (Rle_or_lt y x); intros H3.
apply SterbenzApprox_weak_1 with rho; auto with real float.
apply oppBoundedInv; rewrite Fopp_Fminus.
apply SterbenzApprox_weak_1 with rho; auto with real float.
Qed.
End SterbenzApprox.
Section RinvProps.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable prec : nat.
Hypothesis precMoreThanOne : 1 < prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Theorem Rle_floats_isMax_Pos :
forall (f g : float) (r : R),
Fcanonic radix b f ->
Fcanonic radix b g ->
(0 < f)%R ->
isMax b radix r g ->
(f - Fulp b radix prec (FPred b radix prec f) < r)%R -> (f <= g)%R.
intros f g r Hf Hg Hf' H1 H.
rewrite <- FSucPred with b radix prec f; auto with arith.
unfold FtoRradix in |- *; apply FSuccProp; fold FtoRradix in |- *;
auto with arith float.
apply Rlt_le_trans with r; auto with real float.
2: elim H1; intros H2 H3; elim H3; auto with real.
apply Rle_lt_trans with (2 := H).
apply Rplus_le_reg_l with (Fulp b radix prec (FPred b radix prec f)).
right; ring_simplify (Fulp b radix prec (FPred b radix prec f) +
(f - Fulp b radix prec (FPred b radix prec f)))%R.
rewrite Rplus_comm; unfold FtoRradix in |- *; apply FpredUlpPos;
auto with float real zarith.
Qed.
Theorem Rle_floats_isMax_Neg :
forall (f g : float) (r : R),
Fcanonic radix b f ->
Fcanonic radix b g ->
(f < 0)%R ->
isMax b radix r g -> (f - Fulp b radix prec f < r)%R -> (f <= g)%R.
intros f g r Hf Hg Hf' H1 H.
rewrite <- FSucPred with b radix prec f; auto with arith.
unfold FtoRradix in |- *; apply FSuccProp; fold FtoRradix in |- *;
auto with arith float.
apply Rlt_le_trans with r; auto with real float.
2: elim H1; intros H2 H3; elim H3; auto with real.
apply Rle_lt_trans with (2 := H).
apply
Rplus_le_reg_l
with (Fulp b radix prec f - FtoRradix (FPred b radix prec f))%R.
right; ring_simplify.
apply trans_eq with (Fulp b radix prec (Fopp f)).
repeat rewrite CanonicFulp; auto with float zarith.
rewrite <- FSuccUlpPos; auto with float real;
[ idtac | rewrite Fopp_correct; auto with real ].
rewrite Fminus_correct; auto with zarith; rewrite FPredFopFSucc;
auto with arith.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring.
Qed.
Theorem FulpFPred_not_pow :
forall f : float,
(forall e : Z, FtoRradix f <> powerRZ radix e) ->
(0 < f)%R ->
Fcanonic radix b f ->
Fulp b radix prec (FPred b radix prec f) = Fulp b radix prec f.
intros f H Hfpos Hf.
cut (Fcanonic radix b (FPred b radix prec f));
[ intros H1 | apply FPredCanonic; auto with arith ].
repeat rewrite CanonicFulp; auto.
unfold FtoR in |- *; simpl in |- *; ring_simplify.
generalize (Z_eq_bool_correct (Fnum f) (- pPred (vNum b)));
case (Z_eq_bool (Fnum f) (- pPred (vNum b))); intros H2.
Contradict Hfpos; apply Rle_not_lt; unfold FtoRradix in |- *;
apply LeZEROFnum; auto.
rewrite H2; unfold pPred in |- *; replace 0%Z with (- (0))%Z;
auto with zarith float.
generalize (Z_eq_bool_correct (Fnum f) (nNormMin radix prec));
case (Z_eq_bool (Fnum f) (nNormMin radix prec)); intros H3.
unfold nNormMin in H3; Contradict H.
apply
ex_not_not_all
with
(U := Z)
(P := fun t : Z => FtoRradix f <> powerRZ radix t).
exists (Fexp f + Zpred prec)%Z.
cut (FtoRradix f = powerRZ radix (Fexp f + Zpred prec)); auto with real.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite powerRZ_add;
auto with zarith real.
rewrite H3; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith;
ring.
rewrite FPredSimpl4; auto.
Qed.
Theorem RinvClosestRinvMaxRle_Pos :
radix = 2%Z ->
forall a u v : float,
(forall e : Z, FtoRradix a <> powerRZ radix e) ->
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> (0 < a)%R -> (0 < u)%R -> (a <= v)%R.
intros Hradix a u v Hpow Fa Fu Nu Ca Cv Hu Hv H H'.
apply Rle_floats_isMax_Pos with (/ u)%R; auto; unfold Rminus in |- *.
rewrite FulpFPred_not_pow; auto.
cut (0 < powerRZ radix prec - 1)%R; [ intros V0 | idtac ].
2: apply Rplus_lt_reg_r with 1%R.
2: ring_simplify.
2: replace 1%R with (powerRZ radix 0); auto with real zarith arith.
apply Rle_lt_trans with (FtoRradix a + - (a * / (powerRZ radix prec - 1)))%R;
[ apply Rplus_le_compat_l; apply Ropp_le_contravar | idtac ].
apply Rmult_le_reg_l with (powerRZ radix prec - 1)%R; auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l; auto with real.
ring_simplify (FtoRradix a * 1)%R.
apply Rle_trans with (Rabs a); [ apply RRle_abs | idtac ].
unfold FtoRradix in |- *; apply FulpGe; auto with real zarith.
apply Rle_lt_trans with (FtoRradix a * (1 + - / (powerRZ radix prec - 1)))%R;
[ right; ring; ring | idtac ].
cut (0 < 1 + - / (powerRZ radix prec - 1))%R; [ intros V1 | idtac ].
2: apply Rplus_lt_reg_r with (/ (powerRZ radix prec - 1))%R.
2: ring_simplify.
2: pattern 1%R at 2 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar;
auto with real.
2: apply Rlt_le_trans with (1 := V0); right; ring.
2: apply Rplus_lt_reg_r with 1%R; ring_simplify (1 + (powerRZ radix prec - 1))%R.
2: apply Rle_lt_trans with (IZR radix); auto with zarith real.
2: replace 2%R with (IZR 2); auto with real zarith.
2: pattern (IZR radix) at 1 in |- *;
replace (IZR radix) with (powerRZ radix 1); auto with real zarith.
cut (0 < 1 + - / (2%nat * powerRZ radix (Zpred prec)))%R;
[ intros V2 | idtac ].
2: apply Rplus_lt_reg_r with (/ (2%nat * powerRZ radix (Zpred prec)))%R.
2: ring_simplify.
2: rewrite <- Rinv_1; apply Rinv_lt_contravar; auto with real.
2: repeat apply Rmult_lt_0_compat; auto with arith zarith real.
2: apply Rlt_trans with (powerRZ radix (Zpred prec)).
2: replace 1%R with (powerRZ radix (Zpred 1)); auto with real zarith arith.
2: apply Rle_lt_trans with (1 * powerRZ radix (Zpred prec))%R;
[ right; ring | auto with real arith ].
apply
Rle_lt_trans
with
(/ FtoRradix u * / (1 + - / (2%nat * powerRZ radix (Zpred prec))) *
(1 + - / (powerRZ radix prec - 1)))%R.
apply Rmult_le_compat_r; auto with real.
rewrite <- Rinv_involutive with (FtoRradix a); auto with real.
rewrite <- Rinv_mult_distr; auto with real.
apply Rle_Rinv; [ apply Rmult_lt_0_compat; auto with real | idtac ].
rewrite Rinv_mult_distr; auto with real arith zarith.
apply Rle_trans with (FtoRradix u + - (/ 2%nat * Fulp b radix prec u))%R.
apply Rle_trans with (u + - (/ 2%nat *( /powerRZ radix (Zpred prec)*u)))%R;
[right; ring|idtac].
apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real arith.
apply Rle_trans with (Rabs u * powerRZ radix (Zsucc (- prec)))%R.
unfold FtoRradix in |- *; apply FulpLe2; auto with float.
rewrite Rinv_powerRZ; auto with zarith real.
rewrite Rabs_right with (FtoRradix u);
[ idtac | apply Rle_ge; auto with real ].
replace (Zsucc (- prec)) with (- Zpred prec)%Z;
[ right | unfold Zsucc, Zpred in |- * ]; ring.
apply Rplus_le_reg_l with (/ 2%nat * Fulp b radix prec u + - / FtoRradix a)%R.
ring_simplify.
apply Rle_trans with (Rabs (- / FtoRradix a + FtoRradix u));
[ apply RRle_abs | idtac ].
rewrite <- Rabs_Ropp.
replace (- (- / FtoRradix a + FtoRradix u))%R with (/ FtoRradix a - 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.
right; simpl; field.
rewrite Rmult_assoc;
apply Rlt_le_trans with (/u * 1)%R;[ apply Rmult_lt_compat_l; auto with real| right; ring].
apply Rmult_lt_reg_l with (1 + - / (2%nat * powerRZ radix (Zpred prec)))%R;
auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
ring_simplify.
apply Rplus_lt_compat_r; apply Ropp_lt_contravar; apply Rinv_lt_contravar.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R; unfold Rminus in |- *;
auto with real.
ring_simplify (powerRZ radix prec + -0)%R.
pattern (Z_of_nat prec) at 1 in |- *;
replace (Z_of_nat prec) with (1 + Zpred prec)%Z;
[ rewrite powerRZ_add; auto with real zarith | unfold Zpred in |- *; ring ].
apply Rmult_le_compat_r; auto with real zarith; simpl in |- *.
ring_simplify (radix * 1)%R; rewrite Hradix; auto with real zarith.
Qed.
Theorem RinvClosestRinvMaxRle_Neg :
radix = 2%Z ->
forall a u v : float,
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> (a < 0)%R -> (u < 0)%R -> (a <= v)%R.
intros Hradix a u v Fa Fu Nu Ca Cv Hu Hv H H'.
apply Rle_floats_isMax_Neg with (/ u)%R; auto; unfold Rminus in |- *.
cut (0 < powerRZ radix prec - 1)%R; [ intros V0 | idtac ].
2: apply Rplus_lt_reg_r with 1%R.
2: ring_simplify.
2: replace 1%R with (powerRZ radix 0); auto with real zarith arith.
apply Rle_lt_trans with (FtoRradix a + a * / (powerRZ radix prec - 1))%R;
[ apply Rplus_le_compat_l | idtac ].
apply Ropp_le_cancel; rewrite Ropp_involutive;
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_reg_l with (powerRZ radix prec - 1)%R; auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l; auto with real.
ring_simplify (- FtoRradix a * 1)%R; rewrite <- Rabs_left; auto with real.
unfold FtoRradix in |- *; apply FulpGe; auto with real zarith.
apply Rle_lt_trans with (FtoRradix a * (1 + / (powerRZ radix prec - 1)))%R;
[ right; ring; ring | idtac ].
cut (0 < 1 + / (powerRZ radix prec - 1))%R; [ intros V1 | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
cut (0 < 1 + / (2%nat * powerRZ radix (Zpred prec)))%R; [ intros V2 | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
2: apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
auto with real arith zarith.
apply
Rle_lt_trans
with
(/ FtoRradix u * / (1 + / (2%nat * powerRZ radix (Zpred prec))) *
(1 + / (powerRZ radix prec - 1)))%R.
apply Rmult_le_compat_r; auto with real.
rewrite <- Rinv_involutive with (FtoRradix a); auto with real.
rewrite <- Rinv_mult_distr; auto with real.
apply Ropp_le_cancel; rewrite Ropp_inv_permute; auto with real.
rewrite Ropp_inv_permute with (/ FtoRradix a)%R; auto with real.
apply Rle_Rinv; [ auto with real | apply Ropp_le_contravar ].
rewrite Rinv_mult_distr; auto with real arith zarith.
apply Rle_trans with (FtoRradix u + - (/ 2%nat * Fulp b radix prec u))%R.
apply Rle_trans with (u+(/2%nat*(/ powerRZ radix (Zpred prec) * u)))%R;
[right; ring|idtac].
apply Rplus_le_compat_l; apply Ropp_le_cancel; rewrite Ropp_involutive.
apply
Rle_trans with (/ 2%nat * (/ powerRZ radix (Zpred prec) * - FtoRradix u))%R;
[ apply Rmult_le_compat_l; auto with real arith | right; ring ].
apply Rle_trans with (Rabs u * powerRZ radix (Zsucc (- prec)))%R.
unfold FtoRradix in |- *; apply FulpLe2; auto with float.
rewrite Rinv_powerRZ; auto with zarith real.
rewrite Rabs_left with (FtoRradix u); [ idtac | auto with real ].
replace (Zsucc (- prec)) with (- Zpred prec)%Z;
[ right | unfold Zsucc, Zpred in |- * ]; ring.
apply Rplus_le_reg_l with (/ 2%nat * Fulp b radix prec u + - / FtoRradix a)%R.
ring_simplify.
apply Rle_trans with (Rabs (- / FtoRradix a + FtoRradix u));
[ apply RRle_abs | idtac ].
rewrite <- Rabs_Ropp.
replace (- (- / FtoRradix a + FtoRradix u))%R with (/ FtoRradix a - 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.
right; simpl; field.
apply Ropp_lt_cancel; rewrite Ropp_inv_permute; auto with real.
rewrite <- Ropp_mult_distr_l_reverse; rewrite <- Ropp_mult_distr_l_reverse;
rewrite Ropp_inv_permute; auto with real.
pattern (/ - FtoRradix u)%R at 1 in |- *;
replace (/ - FtoRradix u)%R with (/ - FtoRradix u * 1)%R;
[ idtac | ring ].
rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real.
apply Rmult_lt_reg_l with (1 + / (2%nat * powerRZ radix (Zpred prec)))%R;
auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
ring_simplify.
apply Rplus_lt_compat_r; apply Rinv_lt_contravar; auto with real.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R; unfold Rminus in |- *;
auto with real.
ring_simplify (powerRZ radix prec + -0)%R.
pattern (Z_of_nat prec) at 1 in |- *;
replace (Z_of_nat prec) with (1 + Zpred prec)%Z;
[ rewrite powerRZ_add; auto with real zarith | unfold Zpred in |- *; ring ].
apply Rmult_le_compat_r; auto with real zarith; simpl in |- *.
ring_simplify (radix * 1)%R; rewrite Hradix; auto with real zarith.
Qed.
Theorem RinvClosestRinvMaxRle_pow :
forall (a u v : float) (e : Z),
a = powerRZ radix e :>R ->
(e <= dExp b)%Z ->
Fbounded b a ->
Closest b radix (/ a) u -> isMax b radix (/ u) v -> a = v :>R.
intros a u v e Ha He Fa Hu Hv.
cut (ProjectorP b radix (isMax b radix));
[ unfold ProjectorP in |- *; intros V | apply ProjectMax ].
unfold FtoR in |- *; apply V; auto.
replace (FtoR radix a) with (/ FtoRradix u)%R; auto.
replace (FtoRradix u) with (powerRZ radix (- e)); fold FtoRradix in |- *.
rewrite Ha; rewrite Rinv_powerRZ; auto with zarith real; ring_simplify (- - e)%Z; auto.
apply trans_eq with (FtoRradix (Float 1 (- e)));
[ unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
unfold FtoRradix in |- *;
apply RoundedModeProjectorIdemEq with b prec (Closest b radix);
auto.
apply ClosestRoundedModeP with prec; auto.
split; simpl in |- *; auto with zarith; rewrite pGivesBound;
replace 1%Z with (Zpower_nat radix 0); auto with zarith.
replace (FtoR radix (Float 1 (- e))) with (/ FtoRradix a)%R; auto.
rewrite Ha; rewrite Rinv_powerRZ; auto with zarith real; unfold FtoR in |- *;
simpl in |- *; ring.
Qed.
Theorem RinvClosestRinvMaxRle_pow2 :
forall (a u v : float) (e : Z),
a = powerRZ radix e :>R ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fbounded b a ->
Closest b radix (/ a) u -> isMax b radix (/ u) v -> a = v :>R.
intros a u v e Ha Nu Fa Hu Hv.
apply RinvClosestRinvMaxRle_pow with u e; auto.
case (Zle_or_lt e (dExp b)); intros H; auto with zarith.
absurd (u <= powerRZ radix (- dExp b))%R.
apply Rlt_not_le;
apply Rlt_le_trans with (FtoRradix (firstNormalPos radix b prec)).
unfold firstNormalPos, nNormMin, FtoRradix, FtoR in |- *; simpl in |- *;
rewrite Zpower_nat_Z_powerRZ.
apply Rle_lt_trans with (powerRZ radix 0 * powerRZ radix (- dExp b))%R;
[ right; simpl in |- *; ring | idtac ].
apply Rmult_lt_compat_r; auto with real zarith; rewrite inj_pred;
auto with zarith arith.
apply Rlt_powerRZ; unfold Zpred in |- *; auto with arith zarith real.
unfold FtoRradix in |- *;
rewrite <- FnormalizeCorrect with (p := u) (b := b) (precision := prec);
auto.
apply FnormalLtFirstNormalPos; auto with arith.
rewrite FnormalizeCorrect; auto.
apply RleRoundedR0 with b prec (Closest b radix) (/ a)%R; auto;
[ apply ClosestRoundedModeP with prec; auto
| rewrite Ha; auto with real zarith ].
cut (MonotoneP radix (Closest b radix));
[ unfold MonotoneP in |- *; intros V | apply ClosestMonotone ].
apply Rle_trans with (FtoRradix (Float 1 (- dExp b)));
unfold FtoRradix in |- *;
[ idtac | right; unfold FtoR in |- *; simpl in |- *; ring ].
unfold FtoRradix in |- *;
apply V with (/ a)%R (FtoRradix (Float 1 (- dExp b)));
auto.
rewrite Ha; rewrite Rinv_powerRZ; unfold FtoRradix, FtoR in |- *;
simpl in |- *; auto with real zarith.
ring_simplify (1 * powerRZ radix (- dExp b))%R; auto with real zarith.
unfold FtoRradix in |- *; apply RoundedModeProjectorIdem with b;
auto with float zarith.
apply ClosestRoundedModeP with prec; auto.
split; simpl in |- *; auto with zarith float.
rewrite pGivesBound; replace 1%Z with (Zpower_nat radix 0);
auto with arith zarith real.
Qed.
Theorem RinvClosestRinvMaxRle :
radix = 2%Z ->
forall a u v : float,
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> a <> 0%R :>R -> (a <= v)%R.
intros Hradix a u v Fa Fu Nu Ca Cv Hu Hv Ha.
cut (forall a b : R, (a <= b)%R -> a <> b -> (a < b)%R); [ intros V | idtac ].
2: intros x y H'1 H'2; case H'1; auto with real; intros H'3.
2: absurd (x = y :>R); auto with real.
cut (u <> 0%R :>R); [ intros H' | idtac ].
2: unfold FtoRradix in |- *;
rewrite <- FnormalizeCorrect with (b := b) (precision := prec);
auto.
2: cut
(~ is_Fzero (Fnormalize radix b prec u) ->
FtoR radix (Fnormalize radix b prec u) <> 0%R :>R);
[ intros V'; apply V' | idtac ].
2: apply FnormalNotZero with radix b; auto with float real.
2: unfold is_Fzero in |- *; intros H2; unfold FtoR in |- *; simpl in |- *.
2: apply prod_neq_R0; auto with real zarith.
case (Rle_or_lt a 0); intros H.
case H; intros H1; [ idtac | absurd (FtoRradix a = 0%R :>R); auto with real ].
apply RinvClosestRinvMaxRle_Neg with u; auto.
apply V; auto; unfold FtoRradix in |- *.
apply RleRoundedLessR0 with b prec (Closest b radix) (/ a)%R;
auto with float zarith real.
apply ClosestRoundedModeP with prec; auto.
case (classic (forall e : Z, FtoRradix a <> powerRZ radix e :>R));
intros H1.
apply RinvClosestRinvMaxRle_Pos with u; auto with real.
apply V; auto; unfold FtoRradix in |- *.
apply RleRoundedR0 with b prec (Closest b radix) (/ a)%R;
auto with float zarith real.
apply ClosestRoundedModeP with prec; auto.
cut (exists e : Z, FtoRradix a = powerRZ radix e :>R);
[ intros H2 | idtac ].
elim H2; intros e H3.
right; apply RinvClosestRinvMaxRle_pow2 with u e; auto.
apply
not_all_not_ex
with
(U := Z)
(P := fun t : Z => FtoRradix a = powerRZ radix t :>R);
auto.
Qed.
End RinvProps.
Require Export Classical.
Section SterbenzApprox.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables (b1 : Fbound) (b2 : Fbound).
Variables (prec1 : nat) (prec2 : nat).
Hypothesis prec1MoreThanOne : 1 < prec1.
Hypothesis p1GivesBound : Zpos (vNum b1) = Zpower_nat radix prec1.
Hypothesis prec2MoreThanOne : 1 < prec2.
Hypothesis p2GivesBound : Zpos (vNum b2) = Zpower_nat radix prec2.
Theorem Rmin_1 : forall x y : R, (x <= y)%R -> Rmin x y = x.
intros x y H; unfold Rmin in |- *.
case (Rle_dec x y); auto with real.
Qed.
Theorem Rmin_2 : forall x y : R, (y <= x)%R -> Rmin x y = y.
intros x y H; unfold Rmin in |- *.
case (Rle_dec x y); auto with real.
Qed.
Theorem Rmin_eq : forall x : R, Rmin x x = x.
intros x; unfold Rmin in |- *.
case (Rle_dec x x); auto with real.
Qed.
Theorem Rdiv_Rle :
forall a b c d : R,
(0 < a)%R ->
(0 < b)%R ->
(0 < c)%R -> (0 < d)%R -> (a <= c)%R -> (d <= b)%R -> (a / b <= c / d)%R.
intros a b c d Ha Hb Hc Hd H1 H2; unfold Rdiv in |- *.
apply Rle_trans with (c * / b)%R; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rle_Rinv; auto with real.
Qed.
Theorem SterbenzApprox :
forall (rho : R) (x y : float),
(0 < rho)%R ->
IZR (Zpos (vNum b1)) = (rho * Zsucc (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 ->
exists u : float, u = (x - y)%R :>R /\ Fbounded b2 u.
intros rho x y Hrho Hrho' Hv0 Fx Fy H1 H2.
cut
(forall b : Fbound,
Z_of_nat
(vNumInf
(BoundI (pred (nat_of_P (vNum b))) (nat_of_P (vNum b))
(Zabs_nat (dExp b)))) = Zpred (Zpos (vNum b)));
[ intros V1 | idtac ].
2: intros b; apply trans_eq with (Z_of_nat (pred (nat_of_P (vNum b))));
[ simpl in |- *; auto | idtac ].
2: apply trans_eq with (Zpred (nat_of_P (vNum b)));
[ apply inj_pred; auto with zarith | idtac ].
2: rewrite inject_nat_convert with (Zpos (vNum b)) (vNum b);
auto with zarith arith.
cut
(forall b : Fbound,
Z_of_nat
(vNumSup
(BoundI (pred (nat_of_P (vNum b))) (nat_of_P (vNum b))
(Zabs_nat (dExp b)))) = Zpos (vNum b)); [ intros V2 | idtac ].
2: intros b; apply trans_eq with (Z_of_nat (nat_of_P (vNum b)));
[ simpl in |- *; auto | idtac ].
2: apply inject_nat_convert; auto with zarith arith.
elim
SterbenzApproxI_pos
with
radix
(BoundI (pred (nat_of_P (vNum b1))) (nat_of_P (vNum b1))
(Zabs_nat (dExp b1)))
(BoundI (pred (nat_of_P (vNum b2))) (nat_of_P (vNum b2))
(Zabs_nat (dExp b2)))
rho
x
y; auto with real zarith.
2: rewrite (V1 b1); rewrite (V1 b2); rewrite (V2 b1); rewrite (V2 b2).
2: repeat rewrite <- Zsucc_pred.
2: rewrite
Rmin_1
with
(x := (Zpos (vNum b1) / Zsucc (Zpos (vNum b2)))%R);
[ idtac | apply Rdiv_Rle; auto with real zarith ].
2: rewrite Rmin_2; [ rewrite Hrho' | idtac ].
2: unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_r;
auto with real zarith arith.
2: case
(Rle_or_lt (Zpos (vNum b1) / Zpos (vNum b2))
(Zsucc (Zpos (vNum b1)) / Zsucc (Zpos (vNum b2))));
intros H.
2: rewrite Rmin_1; auto with real; apply Rdiv_Rle; auto with real zarith.
2: rewrite Rmin_2; auto with real; apply Rdiv_Rle; auto with real zarith.
2: simpl; repeat rewrite <- Zabs_absolu.
2: repeat rewrite Zabs_eq; auto with zarith.
2: case (dExp b1); auto with zarith.
2: case (dExp b2); auto with zarith.
2: intros z Hz.
2: apply FoppBoundedI2 with (Zabs_nat (Zpower_nat radix (pred prec2)));
auto with zarith.
2: rewrite (V1 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: replace (radix * Zpower_nat radix (pred prec2))%Z with
(Zpower_nat radix prec2); auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
2: rewrite (V2 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
2: intros z Hz.
2: apply FoppBoundedI2 with (Zabs_nat (Zpower_nat radix (pred prec1)));
auto with zarith.
2: rewrite (V1 b1); rewrite p1GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: replace (radix * Zpower_nat radix (pred prec1))%Z with
(Zpower_nat radix prec1); auto with zarith arith.
2: pattern prec1 at 1 in |- *; replace prec1 with (1 + pred prec1);
auto with zarith arith.
2: rewrite (V2 b1); rewrite p1GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec1 at 1 in |- *; replace prec1 with (1 + pred prec1);
auto with zarith arith.
2: split; simpl in |- *; auto with zarith float.
2: split.
2: apply Zle_Zopp_Inv; rewrite Zopp_involutive;
apply Zle_trans with (Zabs (Fnum x)).
2: apply Zle_trans with (Zabs (- Fnum x)); auto with zarith.
2: rewrite Zabs_Zopp; auto with zarith.
2: rewrite inj_pred; auto with float zarith arith.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: apply Zle_trans with (Zabs (Fnum x)); auto with zarith float.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith float.
2: case (dExp b1); auto with zarith.
2: split; simpl in |- *; auto with zarith arith float.
2: split.
2: apply Zle_Zopp_Inv; rewrite Zopp_involutive;
apply Zle_trans with (Zabs (Fnum y)).
2: apply Zle_trans with (Zabs (- Fnum y)); auto with zarith float.
2: rewrite Zabs_Zopp; auto with zarith.
2: rewrite inj_pred; auto with float zarith arith.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: apply Zle_trans with (Zabs (Fnum y)); auto with zarith float.
2: rewrite inject_nat_convert with (Zpos (vNum b1)) (vNum b1);
auto with zarith float.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith float.
2: case (dExp b1); auto with zarith.
intros u tmp; elim tmp; intros Hu1 Hu2; clear tmp.
elim
ReductRangeI
with
radix
(BoundI (pred (nat_of_P (vNum b2))) (nat_of_P (vNum b2))
(Zabs_nat (dExp b2)))
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))
(Zabs_nat (Zpower_nat radix (pred prec2)))
u; auto with real zarith.
2: rewrite (V2 b2);
apply trans_eq with (pred (nat_of_P (vNum b2)) + 1)%Z;
[ idtac | simpl in |- *; auto ].
2: rewrite inj_pred; auto with zarith.
2: rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith arith; unfold Zpred in |- *; ring.
2: rewrite (V2 b2); rewrite p2GivesBound; rewrite <- Zabs_absolu;
rewrite Zabs_eq; auto with zarith arith.
2: pattern prec2 at 1 in |- *; replace prec2 with (1 + pred prec2);
auto with zarith arith.
intros v tmp; elim tmp; intros Hv1 Hv2; clear tmp.
exists v; split.
unfold FtoRradix in |- *; rewrite <- Hv2; rewrite Hu1; auto with real.
elim Hv1; intros tmp H3; elim tmp; intros H4 H5; clear tmp; split;
auto with zarith.
case (Zle_or_lt 0 (Fnum v)); intros H'.
rewrite Zabs_eq; auto with zarith.
replace (Zpos (vNum b2)) with
(Zsucc
(vNumSup
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))));
auto with zarith.
apply trans_eq with (Zsucc (pred (nat_of_P (vNum b2))));
[ simpl in |- *; auto | idtac ].
rewrite inj_pred; auto with zarith.
rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith; rewrite <- Zsucc_pred; auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
replace (Zpos (vNum b2)) with
(Zsucc
(vNumInf
(BoundI (pred (nat_of_P (vNum b2)))
(pred (nat_of_P (vNum b2))) (Zabs_nat (dExp b2)))));
auto with zarith.
apply trans_eq with (Zsucc (pred (nat_of_P (vNum b2))));
[ simpl in |- *; auto | idtac ].
rewrite inj_pred; auto with zarith.
rewrite inject_nat_convert with (Zpos (vNum b2)) (vNum b2);
auto with zarith.
rewrite <- Zsucc_pred; auto.
apply Zle_trans with (2:=H3); simpl.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith;
case (dExp b2); auto with zarith.
Qed.
Theorem SterbenzApprox_weak_1 :
forall (rho : R) (x y : float),
(0 < rho)%R ->
IZR (Zpos (vNum b1)) = (rho * Zpos (vNum b2))%R ->
(- dExp b2 <= - dExp b1)%Z ->
Fbounded b1 x ->
Fbounded b1 y ->
(0 <= y)%R ->
(y <= x)%R ->
(x <= (1 + / rho) * y)%R ->
Fbounded b2
(Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y)).
intros rho x y H1 H2 H'' H3 H4 H5 H6 H7.
cut
(0 <=
Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y))%R;
[ intros Rle1 | idtac ].
2: rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- *.
2: unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
2: apply Rplus_le_reg_l with (r := FtoR radix y); auto.
2: fold FtoRradix in |- *; ring_simplify; auto with real.
cut
(Fexp
(Fminus radix (Fnormalize radix b1 prec1 x) (Fnormalize radix b1 prec1 y)) =
Fexp (Fnormalize radix b1 prec1 y)); [ intros He | idtac ].
2: unfold Fminus in |- *; simpl in |- *; apply Zmin_le2.
2: apply Fcanonic_Rle_Zle with radix b1 prec1; auto with real zarith float.
2: repeat rewrite FnormalizeCorrect; auto.
2: fold FtoRradix in |- *; repeat rewrite Rabs_right; auto with real.
2: apply Rle_ge; apply Rle_trans with (FtoRradix y); auto with real.
split.
rewrite Zabs_eq; [ idtac | apply LeR0Fnum with radix; auto with real zarith ].
apply Zlt_Rlt;
apply
Rle_lt_trans
with ((x - y) * powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)))%R.
right;
apply
trans_eq
with
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y) *
powerRZ radix
(-
Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y))))%R.
unfold FtoRradix, FtoR in |- *; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify
(Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y)) +
-
Fexp
(Fminus radix (Fnormalize radix b1 prec1 x)
(Fnormalize radix b1 prec1 y)))%Z; simpl in |- *;
ring.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite <- FnormalizeCorrect with radix b1 prec1 x; auto.
rewrite <- FnormalizeCorrect with radix b1 prec1 y; auto.
rewrite He; ring.
apply
Rle_lt_trans
with
(/ rho * FtoRradix y *
powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with (FtoRradix y); auto.
ring_simplify (FtoRradix y + (FtoRradix x - FtoRradix y))%R.
apply Rle_trans with (1 := H7); right; ring.
apply Rle_lt_trans with (/ rho * Fnum (Fnormalize radix b1 prec1 y))%R.
unfold FtoRradix in |- *; rewrite <- FnormalizeCorrect with radix b1 prec1 y;
auto.
right; unfold FtoR in |- *.
apply
trans_eq
with
(/ rho *
(powerRZ radix (- Fexp (Fnormalize radix b1 prec1 y)) *
powerRZ radix (Fexp (Fnormalize radix b1 prec1 y))) *
Fnum (Fnormalize radix b1 prec1 y))%R.
ring.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify
(- Fexp (Fnormalize radix b1 prec1 y) +
Fexp (Fnormalize radix b1 prec1 y))%Z; simpl in |- *;
ring.
apply Rlt_le_trans with (/ rho * Zpos (vNum b1))%R.
apply Rmult_lt_compat_l; auto with real.
rewrite <- (Zabs_eq (Fnum (Fnormalize radix b1 prec1 y)));
auto with real zarith float.
apply LeR0Fnum with radix; auto with zarith real.
rewrite FnormalizeCorrect; auto with real float zarith.
right; rewrite H2; rewrite <- Rmult_assoc; rewrite Rinv_l;
[ ring | auto with zarith real ].
apply Zle_trans with (1 := H''); auto with zarith; rewrite He;
auto with float zarith.
Qed.
Theorem SterbenzApprox2 :
forall (rho : R) (x y : float),
(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)).
intros rho x y Hrho Hv1 Hv2 F1x F1y H1 H2.
cut (0 < 1 + / rho)%R; [ intros H' | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
cut (y <= (1 + / rho) * x)%R; [ intros H'1 | idtac ].
2: apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
2: rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; ring_simplify (1 * x)%R;
auto with real.
cut (0 <= y)%R; [ intros H'2 | idtac ].
2: apply Rmult_le_reg_l with (1 + / rho - / (1 + / rho))%R.
2: apply Rplus_lt_reg_r with (/ (1 + / rho))%R.
2: ring_simplify.
2: apply Rmult_lt_reg_l with (1 + / rho)%R; auto with real.
2: rewrite Rinv_r; auto with real.
2: apply Rlt_le_trans with (1+(/rho+(/rho+/rho*/rho)))%R;[idtac|right; ring].
2: apply Rle_lt_trans with (1 + (0 + (0 + 0)))%R;
[ right; ring | apply Rplus_lt_compat_l; auto with real ].
2: apply Rplus_lt_compat; auto with real.
2: apply Rplus_lt_compat; auto with real.
2: apply Rmult_lt_0_compat; auto with real.
2: ring_simplify ((1 + / rho - / (1 + / rho)) * 0)%R.
2: apply Rplus_le_reg_l with (/ (1 + / rho) * FtoRradix y)%R.
2: ring_simplify; auto with real.
2: apply Rle_trans with (FtoRradix x); auto with real.
2: apply Rle_trans with (1 := H2); right; ring.
cut (0 <= x)%R; [ intros H'3 | idtac ].
2: apply Rle_trans with (2 := H1); apply Rmult_le_pos; auto with real.
case (Rle_or_lt y x); intros H3.
apply SterbenzApprox_weak_1 with rho; auto with real float.
apply oppBoundedInv; rewrite Fopp_Fminus.
apply SterbenzApprox_weak_1 with rho; auto with real float.
Qed.
End SterbenzApprox.
Section RinvProps.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable prec : nat.
Hypothesis precMoreThanOne : 1 < prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Theorem Rle_floats_isMax_Pos :
forall (f g : float) (r : R),
Fcanonic radix b f ->
Fcanonic radix b g ->
(0 < f)%R ->
isMax b radix r g ->
(f - Fulp b radix prec (FPred b radix prec f) < r)%R -> (f <= g)%R.
intros f g r Hf Hg Hf' H1 H.
rewrite <- FSucPred with b radix prec f; auto with arith.
unfold FtoRradix in |- *; apply FSuccProp; fold FtoRradix in |- *;
auto with arith float.
apply Rlt_le_trans with r; auto with real float.
2: elim H1; intros H2 H3; elim H3; auto with real.
apply Rle_lt_trans with (2 := H).
apply Rplus_le_reg_l with (Fulp b radix prec (FPred b radix prec f)).
right; ring_simplify (Fulp b radix prec (FPred b radix prec f) +
(f - Fulp b radix prec (FPred b radix prec f)))%R.
rewrite Rplus_comm; unfold FtoRradix in |- *; apply FpredUlpPos;
auto with float real zarith.
Qed.
Theorem Rle_floats_isMax_Neg :
forall (f g : float) (r : R),
Fcanonic radix b f ->
Fcanonic radix b g ->
(f < 0)%R ->
isMax b radix r g -> (f - Fulp b radix prec f < r)%R -> (f <= g)%R.
intros f g r Hf Hg Hf' H1 H.
rewrite <- FSucPred with b radix prec f; auto with arith.
unfold FtoRradix in |- *; apply FSuccProp; fold FtoRradix in |- *;
auto with arith float.
apply Rlt_le_trans with r; auto with real float.
2: elim H1; intros H2 H3; elim H3; auto with real.
apply Rle_lt_trans with (2 := H).
apply
Rplus_le_reg_l
with (Fulp b radix prec f - FtoRradix (FPred b radix prec f))%R.
right; ring_simplify.
apply trans_eq with (Fulp b radix prec (Fopp f)).
repeat rewrite CanonicFulp; auto with float zarith.
rewrite <- FSuccUlpPos; auto with float real;
[ idtac | rewrite Fopp_correct; auto with real ].
rewrite Fminus_correct; auto with zarith; rewrite FPredFopFSucc;
auto with arith.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring.
Qed.
Theorem FulpFPred_not_pow :
forall f : float,
(forall e : Z, FtoRradix f <> powerRZ radix e) ->
(0 < f)%R ->
Fcanonic radix b f ->
Fulp b radix prec (FPred b radix prec f) = Fulp b radix prec f.
intros f H Hfpos Hf.
cut (Fcanonic radix b (FPred b radix prec f));
[ intros H1 | apply FPredCanonic; auto with arith ].
repeat rewrite CanonicFulp; auto.
unfold FtoR in |- *; simpl in |- *; ring_simplify.
generalize (Z_eq_bool_correct (Fnum f) (- pPred (vNum b)));
case (Z_eq_bool (Fnum f) (- pPred (vNum b))); intros H2.
Contradict Hfpos; apply Rle_not_lt; unfold FtoRradix in |- *;
apply LeZEROFnum; auto.
rewrite H2; unfold pPred in |- *; replace 0%Z with (- (0))%Z;
auto with zarith float.
generalize (Z_eq_bool_correct (Fnum f) (nNormMin radix prec));
case (Z_eq_bool (Fnum f) (nNormMin radix prec)); intros H3.
unfold nNormMin in H3; Contradict H.
apply
ex_not_not_all
with
(U := Z)
(P := fun t : Z => FtoRradix f <> powerRZ radix t).
exists (Fexp f + Zpred prec)%Z.
cut (FtoRradix f = powerRZ radix (Fexp f + Zpred prec)); auto with real.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite powerRZ_add;
auto with zarith real.
rewrite H3; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith;
ring.
rewrite FPredSimpl4; auto.
Qed.
Theorem RinvClosestRinvMaxRle_Pos :
radix = 2%Z ->
forall a u v : float,
(forall e : Z, FtoRradix a <> powerRZ radix e) ->
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> (0 < a)%R -> (0 < u)%R -> (a <= v)%R.
intros Hradix a u v Hpow Fa Fu Nu Ca Cv Hu Hv H H'.
apply Rle_floats_isMax_Pos with (/ u)%R; auto; unfold Rminus in |- *.
rewrite FulpFPred_not_pow; auto.
cut (0 < powerRZ radix prec - 1)%R; [ intros V0 | idtac ].
2: apply Rplus_lt_reg_r with 1%R.
2: ring_simplify.
2: replace 1%R with (powerRZ radix 0); auto with real zarith arith.
apply Rle_lt_trans with (FtoRradix a + - (a * / (powerRZ radix prec - 1)))%R;
[ apply Rplus_le_compat_l; apply Ropp_le_contravar | idtac ].
apply Rmult_le_reg_l with (powerRZ radix prec - 1)%R; auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l; auto with real.
ring_simplify (FtoRradix a * 1)%R.
apply Rle_trans with (Rabs a); [ apply RRle_abs | idtac ].
unfold FtoRradix in |- *; apply FulpGe; auto with real zarith.
apply Rle_lt_trans with (FtoRradix a * (1 + - / (powerRZ radix prec - 1)))%R;
[ right; ring; ring | idtac ].
cut (0 < 1 + - / (powerRZ radix prec - 1))%R; [ intros V1 | idtac ].
2: apply Rplus_lt_reg_r with (/ (powerRZ radix prec - 1))%R.
2: ring_simplify.
2: pattern 1%R at 2 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar;
auto with real.
2: apply Rlt_le_trans with (1 := V0); right; ring.
2: apply Rplus_lt_reg_r with 1%R; ring_simplify (1 + (powerRZ radix prec - 1))%R.
2: apply Rle_lt_trans with (IZR radix); auto with zarith real.
2: replace 2%R with (IZR 2); auto with real zarith.
2: pattern (IZR radix) at 1 in |- *;
replace (IZR radix) with (powerRZ radix 1); auto with real zarith.
cut (0 < 1 + - / (2%nat * powerRZ radix (Zpred prec)))%R;
[ intros V2 | idtac ].
2: apply Rplus_lt_reg_r with (/ (2%nat * powerRZ radix (Zpred prec)))%R.
2: ring_simplify.
2: rewrite <- Rinv_1; apply Rinv_lt_contravar; auto with real.
2: repeat apply Rmult_lt_0_compat; auto with arith zarith real.
2: apply Rlt_trans with (powerRZ radix (Zpred prec)).
2: replace 1%R with (powerRZ radix (Zpred 1)); auto with real zarith arith.
2: apply Rle_lt_trans with (1 * powerRZ radix (Zpred prec))%R;
[ right; ring | auto with real arith ].
apply
Rle_lt_trans
with
(/ FtoRradix u * / (1 + - / (2%nat * powerRZ radix (Zpred prec))) *
(1 + - / (powerRZ radix prec - 1)))%R.
apply Rmult_le_compat_r; auto with real.
rewrite <- Rinv_involutive with (FtoRradix a); auto with real.
rewrite <- Rinv_mult_distr; auto with real.
apply Rle_Rinv; [ apply Rmult_lt_0_compat; auto with real | idtac ].
rewrite Rinv_mult_distr; auto with real arith zarith.
apply Rle_trans with (FtoRradix u + - (/ 2%nat * Fulp b radix prec u))%R.
apply Rle_trans with (u + - (/ 2%nat *( /powerRZ radix (Zpred prec)*u)))%R;
[right; ring|idtac].
apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real arith.
apply Rle_trans with (Rabs u * powerRZ radix (Zsucc (- prec)))%R.
unfold FtoRradix in |- *; apply FulpLe2; auto with float.
rewrite Rinv_powerRZ; auto with zarith real.
rewrite Rabs_right with (FtoRradix u);
[ idtac | apply Rle_ge; auto with real ].
replace (Zsucc (- prec)) with (- Zpred prec)%Z;
[ right | unfold Zsucc, Zpred in |- * ]; ring.
apply Rplus_le_reg_l with (/ 2%nat * Fulp b radix prec u + - / FtoRradix a)%R.
ring_simplify.
apply Rle_trans with (Rabs (- / FtoRradix a + FtoRradix u));
[ apply RRle_abs | idtac ].
rewrite <- Rabs_Ropp.
replace (- (- / FtoRradix a + FtoRradix u))%R with (/ FtoRradix a - 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.
right; simpl; field.
rewrite Rmult_assoc;
apply Rlt_le_trans with (/u * 1)%R;[ apply Rmult_lt_compat_l; auto with real| right; ring].
apply Rmult_lt_reg_l with (1 + - / (2%nat * powerRZ radix (Zpred prec)))%R;
auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
ring_simplify.
apply Rplus_lt_compat_r; apply Ropp_lt_contravar; apply Rinv_lt_contravar.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R; unfold Rminus in |- *;
auto with real.
ring_simplify (powerRZ radix prec + -0)%R.
pattern (Z_of_nat prec) at 1 in |- *;
replace (Z_of_nat prec) with (1 + Zpred prec)%Z;
[ rewrite powerRZ_add; auto with real zarith | unfold Zpred in |- *; ring ].
apply Rmult_le_compat_r; auto with real zarith; simpl in |- *.
ring_simplify (radix * 1)%R; rewrite Hradix; auto with real zarith.
Qed.
Theorem RinvClosestRinvMaxRle_Neg :
radix = 2%Z ->
forall a u v : float,
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> (a < 0)%R -> (u < 0)%R -> (a <= v)%R.
intros Hradix a u v Fa Fu Nu Ca Cv Hu Hv H H'.
apply Rle_floats_isMax_Neg with (/ u)%R; auto; unfold Rminus in |- *.
cut (0 < powerRZ radix prec - 1)%R; [ intros V0 | idtac ].
2: apply Rplus_lt_reg_r with 1%R.
2: ring_simplify.
2: replace 1%R with (powerRZ radix 0); auto with real zarith arith.
apply Rle_lt_trans with (FtoRradix a + a * / (powerRZ radix prec - 1))%R;
[ apply Rplus_le_compat_l | idtac ].
apply Ropp_le_cancel; rewrite Ropp_involutive;
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_reg_l with (powerRZ radix prec - 1)%R; auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l; auto with real.
ring_simplify (- FtoRradix a * 1)%R; rewrite <- Rabs_left; auto with real.
unfold FtoRradix in |- *; apply FulpGe; auto with real zarith.
apply Rle_lt_trans with (FtoRradix a * (1 + / (powerRZ radix prec - 1)))%R;
[ right; ring; ring | idtac ].
cut (0 < 1 + / (powerRZ radix prec - 1))%R; [ intros V1 | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
cut (0 < 1 + / (2%nat * powerRZ radix (Zpred prec)))%R; [ intros V2 | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
[ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
2: apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
auto with real arith zarith.
apply
Rle_lt_trans
with
(/ FtoRradix u * / (1 + / (2%nat * powerRZ radix (Zpred prec))) *
(1 + / (powerRZ radix prec - 1)))%R.
apply Rmult_le_compat_r; auto with real.
rewrite <- Rinv_involutive with (FtoRradix a); auto with real.
rewrite <- Rinv_mult_distr; auto with real.
apply Ropp_le_cancel; rewrite Ropp_inv_permute; auto with real.
rewrite Ropp_inv_permute with (/ FtoRradix a)%R; auto with real.
apply Rle_Rinv; [ auto with real | apply Ropp_le_contravar ].
rewrite Rinv_mult_distr; auto with real arith zarith.
apply Rle_trans with (FtoRradix u + - (/ 2%nat * Fulp b radix prec u))%R.
apply Rle_trans with (u+(/2%nat*(/ powerRZ radix (Zpred prec) * u)))%R;
[right; ring|idtac].
apply Rplus_le_compat_l; apply Ropp_le_cancel; rewrite Ropp_involutive.
apply
Rle_trans with (/ 2%nat * (/ powerRZ radix (Zpred prec) * - FtoRradix u))%R;
[ apply Rmult_le_compat_l; auto with real arith | right; ring ].
apply Rle_trans with (Rabs u * powerRZ radix (Zsucc (- prec)))%R.
unfold FtoRradix in |- *; apply FulpLe2; auto with float.
rewrite Rinv_powerRZ; auto with zarith real.
rewrite Rabs_left with (FtoRradix u); [ idtac | auto with real ].
replace (Zsucc (- prec)) with (- Zpred prec)%Z;
[ right | unfold Zsucc, Zpred in |- * ]; ring.
apply Rplus_le_reg_l with (/ 2%nat * Fulp b radix prec u + - / FtoRradix a)%R.
ring_simplify.
apply Rle_trans with (Rabs (- / FtoRradix a + FtoRradix u));
[ apply RRle_abs | idtac ].
rewrite <- Rabs_Ropp.
replace (- (- / FtoRradix a + FtoRradix u))%R with (/ FtoRradix a - 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.
right; simpl; field.
apply Ropp_lt_cancel; rewrite Ropp_inv_permute; auto with real.
rewrite <- Ropp_mult_distr_l_reverse; rewrite <- Ropp_mult_distr_l_reverse;
rewrite Ropp_inv_permute; auto with real.
pattern (/ - FtoRradix u)%R at 1 in |- *;
replace (/ - FtoRradix u)%R with (/ - FtoRradix u * 1)%R;
[ idtac | ring ].
rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real.
apply Rmult_lt_reg_l with (1 + / (2%nat * powerRZ radix (Zpred prec)))%R;
auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
ring_simplify.
apply Rplus_lt_compat_r; apply Rinv_lt_contravar; auto with real.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rlt_le_trans with (powerRZ radix prec - 0)%R; unfold Rminus in |- *;
auto with real.
ring_simplify (powerRZ radix prec + -0)%R.
pattern (Z_of_nat prec) at 1 in |- *;
replace (Z_of_nat prec) with (1 + Zpred prec)%Z;
[ rewrite powerRZ_add; auto with real zarith | unfold Zpred in |- *; ring ].
apply Rmult_le_compat_r; auto with real zarith; simpl in |- *.
ring_simplify (radix * 1)%R; rewrite Hradix; auto with real zarith.
Qed.
Theorem RinvClosestRinvMaxRle_pow :
forall (a u v : float) (e : Z),
a = powerRZ radix e :>R ->
(e <= dExp b)%Z ->
Fbounded b a ->
Closest b radix (/ a) u -> isMax b radix (/ u) v -> a = v :>R.
intros a u v e Ha He Fa Hu Hv.
cut (ProjectorP b radix (isMax b radix));
[ unfold ProjectorP in |- *; intros V | apply ProjectMax ].
unfold FtoR in |- *; apply V; auto.
replace (FtoR radix a) with (/ FtoRradix u)%R; auto.
replace (FtoRradix u) with (powerRZ radix (- e)); fold FtoRradix in |- *.
rewrite Ha; rewrite Rinv_powerRZ; auto with zarith real; ring_simplify (- - e)%Z; auto.
apply trans_eq with (FtoRradix (Float 1 (- e)));
[ unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
unfold FtoRradix in |- *;
apply RoundedModeProjectorIdemEq with b prec (Closest b radix);
auto.
apply ClosestRoundedModeP with prec; auto.
split; simpl in |- *; auto with zarith; rewrite pGivesBound;
replace 1%Z with (Zpower_nat radix 0); auto with zarith.
replace (FtoR radix (Float 1 (- e))) with (/ FtoRradix a)%R; auto.
rewrite Ha; rewrite Rinv_powerRZ; auto with zarith real; unfold FtoR in |- *;
simpl in |- *; ring.
Qed.
Theorem RinvClosestRinvMaxRle_pow2 :
forall (a u v : float) (e : Z),
a = powerRZ radix e :>R ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fbounded b a ->
Closest b radix (/ a) u -> isMax b radix (/ u) v -> a = v :>R.
intros a u v e Ha Nu Fa Hu Hv.
apply RinvClosestRinvMaxRle_pow with u e; auto.
case (Zle_or_lt e (dExp b)); intros H; auto with zarith.
absurd (u <= powerRZ radix (- dExp b))%R.
apply Rlt_not_le;
apply Rlt_le_trans with (FtoRradix (firstNormalPos radix b prec)).
unfold firstNormalPos, nNormMin, FtoRradix, FtoR in |- *; simpl in |- *;
rewrite Zpower_nat_Z_powerRZ.
apply Rle_lt_trans with (powerRZ radix 0 * powerRZ radix (- dExp b))%R;
[ right; simpl in |- *; ring | idtac ].
apply Rmult_lt_compat_r; auto with real zarith; rewrite inj_pred;
auto with zarith arith.
apply Rlt_powerRZ; unfold Zpred in |- *; auto with arith zarith real.
unfold FtoRradix in |- *;
rewrite <- FnormalizeCorrect with (p := u) (b := b) (precision := prec);
auto.
apply FnormalLtFirstNormalPos; auto with arith.
rewrite FnormalizeCorrect; auto.
apply RleRoundedR0 with b prec (Closest b radix) (/ a)%R; auto;
[ apply ClosestRoundedModeP with prec; auto
| rewrite Ha; auto with real zarith ].
cut (MonotoneP radix (Closest b radix));
[ unfold MonotoneP in |- *; intros V | apply ClosestMonotone ].
apply Rle_trans with (FtoRradix (Float 1 (- dExp b)));
unfold FtoRradix in |- *;
[ idtac | right; unfold FtoR in |- *; simpl in |- *; ring ].
unfold FtoRradix in |- *;
apply V with (/ a)%R (FtoRradix (Float 1 (- dExp b)));
auto.
rewrite Ha; rewrite Rinv_powerRZ; unfold FtoRradix, FtoR in |- *;
simpl in |- *; auto with real zarith.
ring_simplify (1 * powerRZ radix (- dExp b))%R; auto with real zarith.
unfold FtoRradix in |- *; apply RoundedModeProjectorIdem with b;
auto with float zarith.
apply ClosestRoundedModeP with prec; auto.
split; simpl in |- *; auto with zarith float.
rewrite pGivesBound; replace 1%Z with (Zpower_nat radix 0);
auto with arith zarith real.
Qed.
Theorem RinvClosestRinvMaxRle :
radix = 2%Z ->
forall a u v : float,
Fbounded b a ->
Fbounded b u ->
Fnormal radix b (Fnormalize radix b prec u) ->
Fcanonic radix b a ->
Fcanonic radix b v ->
Closest b radix (/ a) u ->
isMax b radix (/ u) v -> a <> 0%R :>R -> (a <= v)%R.
intros Hradix a u v Fa Fu Nu Ca Cv Hu Hv Ha.
cut (forall a b : R, (a <= b)%R -> a <> b -> (a < b)%R); [ intros V | idtac ].
2: intros x y H'1 H'2; case H'1; auto with real; intros H'3.
2: absurd (x = y :>R); auto with real.
cut (u <> 0%R :>R); [ intros H' | idtac ].
2: unfold FtoRradix in |- *;
rewrite <- FnormalizeCorrect with (b := b) (precision := prec);
auto.
2: cut
(~ is_Fzero (Fnormalize radix b prec u) ->
FtoR radix (Fnormalize radix b prec u) <> 0%R :>R);
[ intros V'; apply V' | idtac ].
2: apply FnormalNotZero with radix b; auto with float real.
2: unfold is_Fzero in |- *; intros H2; unfold FtoR in |- *; simpl in |- *.
2: apply prod_neq_R0; auto with real zarith.
case (Rle_or_lt a 0); intros H.
case H; intros H1; [ idtac | absurd (FtoRradix a = 0%R :>R); auto with real ].
apply RinvClosestRinvMaxRle_Neg with u; auto.
apply V; auto; unfold FtoRradix in |- *.
apply RleRoundedLessR0 with b prec (Closest b radix) (/ a)%R;
auto with float zarith real.
apply ClosestRoundedModeP with prec; auto.
case (classic (forall e : Z, FtoRradix a <> powerRZ radix e :>R));
intros H1.
apply RinvClosestRinvMaxRle_Pos with u; auto with real.
apply V; auto; unfold FtoRradix in |- *.
apply RleRoundedR0 with b prec (Closest b radix) (/ a)%R;
auto with float zarith real.
apply ClosestRoundedModeP with prec; auto.
cut (exists e : Z, FtoRradix a = powerRZ radix e :>R);
[ intros H2 | idtac ].
elim H2; intros e H3.
right; apply RinvClosestRinvMaxRle_pow2 with u e; auto.
apply
not_all_not_ex
with
(U := Z)
(P := fun t : Z => FtoRradix a = powerRZ radix t :>R);
auto.
Qed.
End RinvProps.