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).

Require Export FArgReduct.

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 : ∀ 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.

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.

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.

A few lemmas

Theorem minus_Zminus_precq : (prec - q)%Z = prec - q.
clear - pMoinsqGreaterThanOne.
apply sym_eq; apply inj_minus1; auto with zarith arith.
Qed.

Theorem vNum_eq_Zpower :
∀ 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.
clear k N x bzH b1 Fboundedx zHNormal zHDef zLDef NDef zL k preczH_Less_Than_Prec preczH_Pos
  preczH_Greater_Than_One q_not_too_big.
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 :
∀ (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 prec2 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 (∃ 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; ∃ u; split; auto.
∃
(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.
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 ].
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.
∃ 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

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 : ∀ 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 arith.
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 (∃ f:float , Fbounded bmoinsq f ∧
   (FtoRradix f = powerRZ radix (- dExp b +prec -q))%R).
∃ (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

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.

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 : ∀ 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.

No underflow

Hypothesis gamma_ge: (powerRZ radix (-dExp b +prec -q +(Zmax 1 (N -1)))≤ gamma)%R.

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.
∃ (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.

As before, zH shall no be 2^(-N)

Hypothesis zH_not_too_small : (powerRZ radix (2 - Zsucc N) ≤ Rabs zH1)%R.

And x must not be too big

Hypothesis
  xalpha_small :
    (Rabs (x × alpha) ≤
     powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.

A few lemmas

Theorem vNum_eq_Zpower_bzH_fn :
∀ 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 :
∀ 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.
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.
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.
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 :
∀ (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 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 :
∀ (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 ].
∃ (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.
∃ (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.
∃ k; ∃ 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.
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 : ∀ 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.

x not too big

Hypothesis
  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: ∀ (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: ∀ (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 (∃ f:float , Fbounded bmoinsq f ∧
   (FtoRradix f = powerRZ radix (- dExp b +prec -q))%R).
∃ (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.
∃ 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
(∃ k : Z ,
    (∃ zH : float ,
       FtoR 2 zH1 = FtoR 2 zH ∧
       (Zsucc (k + N) ≤ Zpred (Zpred prec))%Z ∧
       (0 ≤ Zsucc (k + N))%Z ∧
       1 < Zabs_nat (Zsucc (k + N)) ∧
       N = (- Fexp zH)%Z ∧
       Fnormal 2
         ((fun k0 : Z ⇒
           Bound
             (P_of_succ_nat
                (pred (Zabs_nat (Zpower_nat 2 (Zabs_nat (Zsucc (k0 + N)))))))
             (dExp b)) k) zH ∧
       (Rabs (FtoR 2 x × FtoR 2 alpha - FtoR 2 zH) ≤
        powerRZ 2%Z (Zpred (- N)))%R ∧
       (powerRZ 2%Z k ≤ Rabs (FtoR 2 zH1) < powerRZ 2%Z (Zsucc k))%R)).
2: apply arg_reduct_exists_k_zH with u; auto with real zarith.
fold radix FtoRradix in |- ×.
intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H3 T4;
elim T4; intros H4 T5; elim T5; intros H5 T6; elim T6;
intros H6 T7; elim T7; intros H7 T8; elim T8; intros H8 T9;
elim T9; intros H9 T10; elim T10; intros H10 H11;
clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10.
rewrite H3.
apply Fmac_arg_reduct_correct1 with q k alpha (x × alpha - zH)%R;
auto with zarith real arith.
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
(∃ 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.
∃ (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.
∃
(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.
Qed.
End Total.