Library Float.Others.FroundDivSqrt

Require Export AllFloat.
Require Export Classical.

Section FroundDiv.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Theorem NearestInteger :
  (r : R) (n : Z),
 ( z : Z, (Rabs (n - r) Rabs (z - r))%R) →
 (Rabs (n - r) / 2)%R.
intros r n H.
case (Rle_or_lt (Rabs (n - r)) (/ 2)); auto; intros H1; Contradict H.
apply
 ex_not_not_all
  with
    (U := Z)
    (P := fun t : Z ⇒ (Rabs (n - r) Rabs (t - r))%R).
generalize H1; case (Rcase_abs (n - r)); intros H2.
repeat rewrite Rabs_left; auto; intros H3.
2: repeat rewrite Rabs_right; auto; intros H3.
(Zsucc n); apply Rlt_not_le.
case (Rcase_abs (Zsucc n - r)); intros H4;
 [ rewrite Rabs_left | rewrite Rabs_right ]; auto.
apply Ropp_lt_contravar; unfold Rminus in |- *; apply Rplus_lt_compat_r;
 auto with zarith real.
apply Rlt_trans with (2 := H3); apply Rplus_lt_reg_r with (-1)%R.
replace (-1 + (Zsucc n - r))%R with (n - r)%R;
 [ idtac | unfold Zsucc in |- *; rewrite plus_IZR; simpl in |- *; ring ].
replace (-1 + / 2)%R with (- / 2)%R; [ idtac | field; auto with real ].
apply Ropp_lt_cancel; rewrite Ropp_involutive; auto.
(Zpred n); apply Rlt_not_le.
case (Rcase_abs (Zpred n - r)); intros H4;
 [ rewrite Rabs_left | rewrite Rabs_right ]; auto.
apply Rlt_trans with (2 := H3); apply Ropp_lt_cancel; rewrite Ropp_involutive;
 auto.
apply Rplus_lt_reg_r with 1%R.
replace (1 + (Zpred n - r))%R with (n - r)%R;
 [ idtac | unfold Zpred in |- *; rewrite plus_IZR; simpl in |- *; ring ].
replace (1 + - / 2)%R with (/ 2)%R; [ auto | field; auto with real ].
unfold Rminus in |- *; apply Rplus_lt_compat_r; auto with zarith real.
Qed.

Theorem errorBoundedModulo_aux :
  (x y : float) (n : Z),
 Fbounded b x
 Fcanonic radix b x
 Fbounded b y
 Fcanonic radix b y
 FtoRradix y 0%R
 (0 < y)%R
 (0 x)%R
 ( z : Z, (Rabs (n - x / y) Rabs (z - x / y))%R) →
 Fbounded b (Fminus radix x (Fmult (Float n 0) y)).
intros x y n Fx Cx Fy Cy Hy Py Px Hn.
cut (/ 2 1)%R; [ intros V | idtac ].
2: pattern 1%R at 3 in |- *; rewrite <- Rinv_1; apply Rle_Rinv;
    auto with real.
case (Zle_or_lt (Fexp y) (Fexp x)); intros H1.
split; [ idtac | simpl in |- *; rewrite Zmin_le2; auto with float ].
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs.
replace (IZR (Fnum (Fminus radix x (Fmult (Float n 0) y)))) with
 (Fminus radix x (Fmult (Float n 0) y) ×
  powerRZ radix (- Fexp (Fminus radix x (Fmult (Float n 0) y))))%R.
2: unfold FtoRradix in |- *; unfold FtoR in |- *; rewrite Rmult_assoc.
2: rewrite <- powerRZ_add; auto with real zarith.
2: ring_simplify
       (Fexp (Fminus radix x (Fmult (Float n 0) y)) +
        - Fexp (Fminus radix x (Fmult (Float n 0) y)))%Z;
    auto with real.
simpl in |- *; rewrite Zmin_le2; auto; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (- Fexp y)));
 [ idtac | apply Rle_ge; auto with real zarith ].
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
replace (FtoRradix (Float n 0)) with (IZR n);
 [ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
replace (FtoRradix x - n × FtoRradix y)%R with
 (FtoRradix y × (FtoRradix x / FtoRradix y - n))%R;
 [ idtac| field; auto with real].
rewrite Rabs_mult;
 apply
  Rle_lt_trans with (Rabs (FtoRradix y) × 1 × powerRZ radix (- Fexp y))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_compat_l; auto with real.
rewrite <- Rabs_Ropp; apply Rle_trans with (/ 2)%R; auto.
replace (- (FtoRradix x / FtoRradix y - n))%R with (n - x / y)%R;
 [ idtac | ring ].
apply NearestInteger; auto.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith;
 unfold FtoR in |- *; simpl in |- ×.
apply Rle_lt_trans with (IZR (Zabs (Fnum y)));
 [ right | auto with float zarith real ].
ring_simplify;rewrite Rmult_assoc;rewrite <- powerRZ_add; auto with zarith real.
ring_simplify ( Fexp y +- Fexp y)%Z; simpl; ring.
replace (INR (nat_of_P (vNum b))) with (IZR (Zpos (vNum b)));
 auto with float zarith real.
case (Req_dec n 0); intros H'0.
cut (n = 0%Z); [ intros H2 | apply eq_IZR; auto ].
rewrite H2; unfold Fmult, Fminus, Fopp, Fplus in |- *; simpl in |- *;
 rewrite Zmin_le1; auto with zarith; simpl in |- *;
 ring_simplify (Fexp x - Fexp x)%Z; simpl in |- ×.
replace (Zpower_nat radix 0) with 1%Z;
 [ ring_simplify (Fnum x × 1 + 0)%Z | simpl in |- × ]; auto with float.
case (Req_dec n 1); intros H'1.
cut (n = 1%Z); [ intros H2 | apply eq_IZR; auto ].
replace (Fmult (Float n 0) y) with y;
 [ idtac
 | unfold Fmult in |- *; rewrite H2; auto with float zarith; simpl in |- × ].
2: apply floatEq; simpl in |- *; auto with zarith float; case (Fnum y);
    auto with zarith.
apply Sterbenz; auto; fold FtoRradix in |- ×.
apply Rmult_le_reg_l with (/ y)%R; auto with real.
apply Rle_trans with (/ 2%nat × (FtoRradix y × / FtoRradix y))%R;
 [ right; ring | rewrite Rinv_r; auto ].
ring_simplify (/ 2%nat × 1)%R;
 apply Rplus_le_reg_l with (/ 2%nat + - (/ FtoRradix y × FtoRradix x))%R.
ring_simplify
    (/ 2%nat + - (/ FtoRradix y × FtoRradix x) + / FtoRradix y × FtoRradix x)%R.
replace (/ FtoRradix y × FtoRradix x)%R with (FtoRradix x / FtoRradix y)%R;
 [ idtac | unfold Rdiv in |- *; ring ].
apply Rle_trans with (/ 2%nat + / 2%nat - FtoRradix x / FtoRradix y)%R;
 [ right; ring | idtac ].
replace (/ 2%nat + / 2%nat)%R with 1%R; [ idtac | simpl; field; auto with real ].
apply Rle_trans with (Rabs (1 - FtoRradix x / FtoRradix y));
 [ apply RRle_abs | rewrite <- H'1 ].
apply NearestInteger; auto.
apply Rmult_le_reg_l with (/ y)%R; auto with real.
apply Rle_trans with (2%nat × (FtoRradix y × / FtoRradix y))%R;
 [ rewrite Rinv_r; auto | right; ring ].
ring_simplify (2%nat × 1)%R; apply Rplus_le_reg_l with (-1)%R.
apply Rle_trans with (- (1 - FtoRradix x / FtoRradix y))%R;
 [ right; unfold Rdiv in |- *; ring | idtac ].
apply Rle_trans with (Rabs (- (1 - FtoRradix x / FtoRradix y)));
 [ apply RRle_abs | rewrite <- H'1; rewrite Rabs_Ropp ].
apply Rle_trans with (/ 2)%R; [ apply NearestInteger; auto | rewrite H'1 ].
apply Rle_trans with 1%R; [ auto | simpl in |- *; right; ring ].
cut (n 1%Z);
 [ intros H''1 | Contradict H'1; rewrite H'1; auto with real zarith ].
cut (n 0%Z);
 [ intros H''0 | Contradict H'0; rewrite H'0; auto with real zarith ].
cut (n 1)%Z; [ intros H'3 | idtac ].
cut (0 n)%Z;
 [ intros H'2; absurd (IZR n 0%Z); auto with zarith | idtac ].
apply Zlt_succ_le; apply lt_IZR; simpl in |- ×.
apply Rle_lt_trans with (FtoRradix x / FtoRradix y)%R; auto with real.
unfold Rdiv in |- *; apply Rmult_le_pos; auto with real.
unfold Zsucc in |- *; simpl in |- *; apply Rplus_lt_reg_r with (- n)%R.
apply Rle_lt_trans with (- (n - FtoRradix x / FtoRradix y))%R;
 [ right; ring | idtac ].
apply Rle_lt_trans with (Rabs (- (n - FtoRradix x / FtoRradix y)));
 [ apply RRle_abs | rewrite Rabs_Ropp ].
apply Rle_lt_trans with (/ 2)%R; [ apply NearestInteger; auto | idtac ].
rewrite plus_IZR; ring_simplify (- n + (n + 1%Z))%R.
simpl; pattern 1%R at 3 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar;
 auto with real.
ring_simplify (1 × 2)%R; auto with real.
apply Zlt_succ_le; apply lt_IZR; simpl in |- ×.
apply Rlt_le_trans with (n + (1 + - (FtoRradix x / FtoRradix y)))%R.
apply Rplus_lt_reg_r with (-1 + - n)%R.
ring_simplify.
apply Ropp_lt_contravar; apply Rmult_lt_reg_l with (FtoRradix y);
 auto with real.
unfold Rdiv in |- *; rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l;
 auto.
ring_simplify.
unfold FtoRradix in |- *; apply FcanonicPosFexpRlt with b precision;
 auto with real arith.
apply Rle_trans with (1 + (n - FtoRradix x / FtoRradix y))%R;
 [ right; ring | apply Rplus_le_compat_l ].
apply Rle_trans with (Rabs (n - FtoRradix x / FtoRradix y));
 [ apply RRle_abs | idtac ].
apply Rle_trans with (/ 2)%R; [ apply NearestInteger; auto | auto ].
Qed.

Theorem errorBoundedModulo_aux_y :
  (x y : float) (n : Z),
 Fbounded b x
 Fcanonic radix b x
 Fbounded b y
 Fcanonic radix b y
 FtoRradix y 0%R
 (0 x)%R
 ( z : Z, (Rabs (n - x / y) Rabs (z - x / y))%R) →
 Fbounded b (Fminus radix x (Fmult (Float n 0) y)).
intros x y n Fx Cx Fy Cy Hy Px Hn.
case (Rle_or_lt 0 y); intros H1.
case H1; intros H2.
apply errorBoundedModulo_aux; auto.
absurd (FtoRradix y = 0%R); auto with real.
replace (Fmult (Float n 0) y) with (Fmult (Float (- n) 0) (Fopp y)).
2: unfold Fopp, Fmult in |- *; simpl in |- *; apply floatEq; simpl in |- *;
    ring.
apply errorBoundedModulo_aux; unfold FtoRradix in |- *;
 repeat rewrite Fopp_correct; fold FtoRradix in |- *;
 auto with float real.
intros z; rewrite Ropp_Ropp_IZR.
rewrite <- Rabs_Ropp;
 rewrite <- (Rabs_Ropp (z - FtoRradix x / - FtoRradix y)).
replace (- (- n - FtoRradix x / - FtoRradix y))%R with
 (n - FtoRradix x / FtoRradix y)%R;
 [ idtac | unfold Rdiv in |- *; rewrite <- Ropp_inv_permute; auto; ring ].
replace (- (z - FtoRradix x / - FtoRradix y))%R with
 (- z - FtoRradix x / FtoRradix y)%R;
 [ idtac | unfold Rdiv in |- *; rewrite <- Ropp_inv_permute; auto; ring ].
rewrite <- Ropp_Ropp_IZR; apply Hn; auto.
Qed.

Theorem errorBoundedModuloCan :
  (x y : float) (n : Z),
 Fbounded b x
 Fcanonic radix b x
 Fbounded b y
 Fcanonic radix b y
 FtoRradix y 0%R
 ( z : Z, (Rabs (n - x / y) Rabs (z - x / y))%R) →
 Fbounded b (Fminus radix x (Fmult (Float n 0) y)).
intros x y n Fx Cx Fy Cy Hy Hn.
case (Rle_or_lt 0 x); intros H1.
apply errorBoundedModulo_aux_y; auto.
replace (Fminus radix x (Fmult (Float n 0) y)) with
 (Fopp (Fminus radix (Fopp x) (Fmult (Float (- n) 0) y))).
2: unfold Fminus, Fopp, Fmult, Fplus in |- *; simpl in |- *; apply floatEq;
    simpl in |- *; ring.
apply oppBounded.
apply errorBoundedModulo_aux_y; unfold FtoRradix in |- *;
 repeat rewrite Fopp_correct; fold FtoRradix in |- *;
 auto with float real.
intros z; rewrite Ropp_Ropp_IZR.
rewrite <- Rabs_Ropp;
 rewrite <- (Rabs_Ropp (z - - FtoRradix x / FtoRradix y)).
replace (- (- n - - FtoRradix x / FtoRradix y))%R with
 (n - FtoRradix x / FtoRradix y)%R; [ idtac | unfold Rdiv in |- *; ring ].
replace (- (z - - FtoRradix x / FtoRradix y))%R with
 (- z - FtoRradix x / FtoRradix y)%R; [ idtac | unfold Rdiv in |- *; ring ].
rewrite <- Ropp_Ropp_IZR; apply Hn; auto.
Qed.

Theorem errorBoundedRem :
  (x y : float) (n : Z),
  (Fbounded b x) → (Fbounded b y) →
   y 0 :>R
  ( z : Z, (Rabs (n - x / y) Rabs (z - x / y))%R) →
    (Fbounded b
      (Fminus radix (Fnormalize radix b precision x)
      (Fmult (Float n 0) (Fnormalize radix b precision y)))).
intros x y n Fx Fy Hy Hn.
apply errorBoundedModuloCan; auto with float.
apply FnormalizeBounded; auto with arith.
apply FnormalizeCanonic; auto with arith.
apply FnormalizeBounded; auto with arith.
apply FnormalizeCanonic; auto with arith.
unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto.
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto.
Qed.

Theorem errorBoundedDiv :
  (x y q : float) P,
  (RoundedModeP b radix P) →
  (Fbounded b x) → (Fbounded b y) → (Fbounded b q) →
  y 0 :>R → (P (x / y)%R q) →
  (- dExp b Fexp q + Fexp y)%Z
  (Rabs q) (powerRZ radix (- dExp b))
   ((powerRZ radix (- dExp b)) / 2%nat Rabs (x / y))%R
      (Fbounded b (Fminus radix x (Fmult q y))).
intros x y q P HP Fx Fy Fq H1 H2 H3 H'.
cut (FtoRradix q = Fnormalize radix b precision q);
 [ intros Hq
 | apply sym_eq; unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision q));
 [ intros Cq | apply FnormalizeCanonic; auto with arith ].
cut (FtoRradix y = Fnormalize radix b precision y);
 [ intros Hy
 | apply sym_eq; unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision y));
 [ intros Cy | apply FnormalizeCanonic; auto with arith ].
case (Zle_or_lt (Fexp q + Fexp y) (Fexp x)); intros H4.
split; [ idtac | simpl in |- *; rewrite Zmin_le2; auto ].
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs.
replace (IZR (Fnum (Fminus radix x (Fmult q y)))) with
 (Fminus radix x (Fmult q y) ×
  powerRZ radix (- Fexp (Fminus radix x (Fmult q y))))%R.
2: unfold FtoRradix in |- *; unfold FtoR in |- *; rewrite Rmult_assoc.
2: rewrite <- powerRZ_add; auto with real zarith.
2: ring_simplify
       (Fexp (Fminus radix x (Fmult q y)) +
        - Fexp (Fminus radix x (Fmult q y)))%Z; auto with real.
simpl in |- *; rewrite Zmin_le2; auto; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (- (Fexp q + Fexp y))));
 [ idtac | apply Rle_ge; auto with real zarith ].
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
replace (FtoRradix x - FtoRradix q × FtoRradix y)%R with
 (FtoRradix y × (FtoRradix x / FtoRradix y - FtoRradix q))%R;
 [ rewrite Rabs_mult | idtac ].
2: field; auto with real.
apply
 Rle_lt_trans
  with
    (Rabs (FtoRradix y) × Fulp b radix precision q ×
     powerRZ radix (- (Fexp q + Fexp y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_compat_l; auto with real.
apply Rlt_le; unfold FtoRradix in |- *; apply RoundedModeUlp with P; auto.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith;
 unfold FtoR, Fulp in |- *; simpl in |- ×.
repeat rewrite Rmult_assoc; repeat rewrite <- powerRZ_add;
 auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum y) × powerRZ radix 0)%R;
 [ apply Rmult_le_compat_l; auto with zarith real | idtac ].
ring_simplify
    (Fexp y + (Fexp (Fnormalize radix b precision q) + - (Fexp q + Fexp y)))%Z;
 apply Rle_powerRZ; auto with zarith real.
apply Zplus_le_reg_l with (Fexp q).
ring_simplify.
apply FcanonicLeastExp with radix b precision; auto with arith.
simpl in |- *; ring_simplify (Zabs (Fnum y) × 1)%R.
apply Rlt_le_trans with (IZR (Zpos (vNum b)));
 auto with float zarith real.
case (Req_dec q 0); intros H5.
replace (Fminus radix x (Fmult q y)) with x; auto.
unfold Fminus, Fmult, Fopp, Fplus in |- *; simpl in |- *; rewrite Zmin_le1;
 auto with zarith.
replace (Fnum q) with 0%Z; ring_simplify (Fexp x - Fexp x)%Z.
ring_simplify (- (0 × Fnum y) × Zpower_nat radix (Zabs_nat (Fexp q + Fexp y - Fexp x)))%Z.
ring_simplify (Fnum x × Zpower_nat radix (Zabs_nat 0) + 0)%Z.
apply floatEq; auto with zarith.
replace (Zpower_nat radix (Zabs_nat 0)) with 1%Z;
 [ ring_simplify (1 × Fnum x)%Z ; simpl| idtac ]; auto with zarith.
cut (is_Fzero q);
 [ unfold is_Fzero in |- × | apply is_Fzero_rep2 with radix ];
 auto.
case (Zle_or_lt (Zabs (Fnum (Fnormalize radix b precision q))) 1); intros H6.
split; [ idtac | simpl in |- *; rewrite Zmin_le1; auto with zarith float ].
apply Zle_lt_trans with (Zabs (Fnum x)); auto with float.
apply Zle_Rle; repeat rewrite <- Faux.Rabsolu_Zabs.
apply Rmult_le_reg_l with (powerRZ radix (Fexp x)); auto with zarith real.
rewrite <- (Rabs_right (powerRZ radix (Fexp x)));
 [ idtac | apply Rle_ge; auto with zarith real ].
repeat rewrite <- Rabs_mult.
replace (powerRZ radix (Fexp x) × Fnum x)%R with (FtoRradix x);
 [ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
replace (powerRZ radix (Fexp x) × Fnum (Fminus radix x (Fmult q y)))%R with
 (FtoRradix (Fminus radix x (Fmult q y))).
2: unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Zmin_le1;
    auto with zarith; ring.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
replace (FtoRradix x - FtoRradix q × FtoRradix y)%R with
 (FtoRradix y × (FtoRradix x / FtoRradix y - FtoRradix q))%R;
 [ rewrite Rabs_mult | idtac ].
2: field; auto with real.
cut (0 < Rabs y)%R; [ intros V | idtac ].
2: cut (0 Rabs y)%R; [ intros V'; case V'; intros W | idtac ];
    auto with real.
2: Contradict W; apply not_eq_sym; apply Rabs_no_R0; auto.
apply Rmult_le_reg_l with (/ Rabs (FtoRradix y))%R; auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
ring_simplify (1 × Rabs (FtoRradix x / FtoRradix y - FtoRradix q))%R.
rewrite <- Rabs_Rinv; auto; rewrite <- Rabs_mult.
replace (/ FtoRradix y × FtoRradix x)%R with (FtoRradix x / FtoRradix y)%R;
 [ idtac | unfold Rdiv in |- *; ring ].
cut
 ( s t : R,
  (Rabs t / 2%nat Rabs s)%R
  (Rabs s 2%nat × Rabs t)%R
  (0 s × t)%R → (Rabs (s - t) Rabs s)%R); [ intros W | idtac ].
cut (Fabs (Fnormalize radix b precision q) = Float 1 (- dExp b));
 [ intros D | idtac ].
cut (Rabs (FtoRradix q) = powerRZ radix (- dExp b)); [ intros H7 | idtac ].
2: rewrite Hq; unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto.
2: rewrite D; unfold FtoR in |- *; simpl in |- *; ring.
apply W.
rewrite H7; case H'; intros H8; auto.
absurd (Rabs (FtoRradix q) = powerRZ radix (- dExp b)); auto with real.
apply Rle_trans with (Rabs (FtoRradix q) + Fulp b radix precision q)%R.
apply Rplus_le_reg_l with (- Rabs (FtoRradix q))%R.
ring_simplify.
apply Rle_trans with (Rabs (FtoRradix x / FtoRradix y - FtoRradix q)).
apply
 Rle_trans with (Rabs (FtoRradix x / FtoRradix y) - Rabs (FtoRradix q))%R;
 [ right; ring | apply Rabs_triang_inv ].
apply Rlt_le; unfold FtoRradix in |- *; apply RoundedModeUlp with P; auto.
rewrite
 FulpComp
          with
          (b := b)
         (radix := radix)
         (precision := precision)
         (q := Fnormalize radix b precision q); auto with float real zarith.
rewrite H7; unfold FtoRradix in |- *; rewrite FulpFabs; auto;
 fold FtoRradix in |- *; rewrite D; simpl in |- *;
 right.
replace (Fulp b radix precision (Float 1 (- dExp b))) with
 (powerRZ radix (- dExp b)); [ ring | unfold Fulp in |- × ].
replace (Fnormalize radix b precision (Float 1 (- dExp b))) with
 (Float 1 (- dExp b)); [ simpl in |- × | idtac ]; auto with float zarith real.
cut (Fbounded b (Float 1 (- dExp b))); [ intros tmp | idtac ].
apply FcanonicUnique with radix b precision; auto with float zarith real.
right; repeat (split; simpl in |- *; auto with zarith float).
ring_simplify (radix × 1)%Z; rewrite Zabs_eq; auto with zarith.
replace radix with (Zpower_nat radix 1);
 [ rewrite pGivesBound | unfold Zpower_nat in |- *; simpl in |- × ];
 auto with zarith float.
apply sym_eq; apply FnormalizeCorrect; auto.
repeat (split; simpl in |- *; auto with zarith float).
rewrite pGivesBound; replace 1%Z with (Zpower_nat radix 0);
 auto with zarith float.
case (Rle_or_lt 0 (FtoRradix x / FtoRradix y)); intros H8.
apply Rmult_le_pos; auto.
unfold FtoRradix in |- *;
 apply RleRoundedR0 with b precision P (FtoRradix x / FtoRradix y)%R;
 auto.
apply Ropp_le_cancel; rewrite Ropp_0; rewrite <- Ropp_mult_distr_l_reverse.
replace 0%R with (- (FtoRradix x / FtoRradix y) × 0)%R;
 [ apply Rmult_le_compat_l; auto with real | ring ].
unfold FtoRradix in |- *;
 apply RleRoundedLessR0 with b precision P (FtoRradix x / FtoRradix y)%R;
 auto with real.
apply floatEq; simpl in |- *; auto with zarith.
cut ( z : Z, (0 z)%Zz 0%Z → (z 1)%Zz = 1%Z);
 [ intros X | auto with zarith ].
apply X; auto with zarith.
cut (Rabs (FtoRradix q) 0%R);
 [ rewrite Hq; intros H7; Contradict H7 | apply Rabs_no_R0; auto with real ].
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto.
unfold Zabs, FtoR in |- *; simpl in |- *; rewrite H7; simpl; ring.
case Cq; intros H; elim H; intros H7 H8; auto with float zarith.
absurd (Zpos (vNum b) radix)%Z;
 [ apply Zlt_not_le | apply Zle_trans with (1 := H8) ].
replace radix with (Zpower_nat radix 1);
 [ rewrite pGivesBound | unfold Zpower_nat in |- *; simpl in |- × ];
 auto with zarith float.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (radix × 1)%Z; auto with zarith.
intros s t H; cut (Rabs t 2 × Rabs s)%R; simpl in |- ×.
case (Rcase_abs t); case (Rcase_abs s); intros H'1 H'2; unfold Rminus in |- ×.
rewrite (Rabs_left t); auto; rewrite (Rabs_left s); auto; intros H'3 H'4 H'5.
case (Rcase_abs (s + - t)); intros H'6.
rewrite Rabs_left; auto with real.
ring_simplify (- (s + - t))%R; apply Rle_trans with ( - s+0)%R; auto with real.
rewrite Rabs_right; auto with real.
apply Rplus_le_reg_l with (- s)%R; ring_simplify.
apply Rle_trans with (1 := H'3); right; ring.
rewrite (Rabs_left t); auto; rewrite (Rabs_right s); auto; intros H'3 H'4 H'5.
cut (0 s)%R; [ intros H'6; case H'6; intros H'7 | idtac ]; auto with real.
Contradict H'5; apply Rlt_not_le; apply Ropp_lt_cancel; rewrite Ropp_0;
 rewrite Rmult_comm; rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_lt_0_compat; auto with real.
rewrite <- H'7; replace (- t)%R with 0%R; auto with real.
ring_simplify (0 + 0)%R; rewrite Rabs_R0; auto with real.
apply Rle_antisym; auto with real.
apply Rle_trans with (1 := H'3); rewrite <- H'7; right; ring.
rewrite (Rabs_right t); auto; rewrite (Rabs_left s); auto; intros H'3 H'4 H'5.
cut (0 t)%R; [ intros H'6; case H'6; intros H'7 | idtac ]; auto with real.
Contradict H'5; apply Rlt_not_le; apply Ropp_lt_cancel; rewrite Ropp_0;
 rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_lt_0_compat; auto with real.
rewrite <- H'7; replace s with 0%R; auto with real.
ring_simplify (0 + -0)%R; rewrite Rabs_R0; auto with real.
apply Rle_antisym; auto with real.
apply Ropp_le_cancel; rewrite Ropp_0.
replace 0%R with (2 × t)%R; [ auto | rewrite <- H'7; ring ].
rewrite (Rabs_right t); auto; rewrite (Rabs_right s); auto;
 intros H'3 H'4 H'5.
case (Rcase_abs (s + - t)); intros H'6.
rewrite Faux.Rabsolu_left1; auto with real.
apply Rplus_le_reg_l with s; ring_simplify (s + - (s + - t))%R; auto with real.
apply Rle_trans with (1 := H'3); right; ring.
rewrite Rabs_right; auto; apply Rle_trans with (s + 0)%R; auto with real.
apply Rmult_le_reg_l with (/ 2)%R; auto with real.
apply Rle_trans with (Rabs t / 2%nat)%R;
 [ right; simpl in |- *; unfold Rdiv in |- *; ring
 | apply Rle_trans with (1 := H) ].
right; rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
split; [ idtac | simpl in |- *; rewrite Zmin_le1; auto with zarith float ].
apply Zle_lt_trans with (Zabs (Fnum x)); auto with float.
apply Zle_Rle; repeat rewrite <- Faux.Rabsolu_Zabs.
apply Rmult_le_reg_l with (powerRZ radix (Fexp x)); auto with zarith real.
rewrite <- (Rabs_right (powerRZ radix (Fexp x)));
 [ idtac | apply Rle_ge; auto with zarith real ].
repeat rewrite <- Rabs_mult.
replace (powerRZ radix (Fexp x) × Fnum x)%R with (FtoRradix x);
 [ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
replace (powerRZ radix (Fexp x) × Fnum (Fminus radix x (Fmult q y)))%R with
 (FtoRradix (Fminus radix x (Fmult q y))).
2: unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Zmin_le1;
    auto with zarith; ring.
apply
 Rle_trans
  with
    ((Zabs (Fnum (Fnormalize radix b precision q)) - 1) ×
     Rabs (FtoRradix (Fminus radix x (Fmult q y))))%R.
apply Rle_trans with (1 × Rabs (FtoRradix (Fminus radix x (Fmult q y))))%R;
 [ right; ring | apply Rmult_le_compat_r; auto with real ].
apply Rplus_le_reg_l with 1%R;
 ring_simplify (1 + (Zabs (Fnum (Fnormalize radix b precision q)) - 1))%R.
replace 2%R with (IZR (Zsucc 1)); auto with real zarith.
apply Rplus_le_reg_l with (Rabs (FtoRradix (Fminus radix x (Fmult q y)))).
ring_simplify.
cut (0 < Zabs (Fnum (Fnormalize radix b precision q)))%R;
 [ intros V | auto with real zarith ].
apply
 Rmult_le_reg_l with (/ IZR (Zabs (Fnum (Fnormalize radix b precision q))))%R;
 auto with real.
apply Rle_trans with (Rabs (FtoRradix (Fminus radix x (Fmult q y)))).
right; rewrite <- Rmult_assoc; rewrite Rmult_comm; rewrite <- Rmult_assoc.
rewrite Rinv_r; auto with real.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
pattern (FtoRradix x - FtoRradix q × FtoRradix y)%R at 1 in |- ×.
replace (FtoRradix x - FtoRradix q × FtoRradix y)%R with
 (FtoRradix y × (FtoRradix x / FtoRradix y - FtoRradix q))%R;
 [ rewrite Rabs_mult | idtac ].
2: field; auto with real.
apply Rle_trans with (Rabs (FtoRradix y) × Fulp b radix precision q)%R.
apply Rmult_le_compat_l; auto with real.
apply Rlt_le; unfold FtoRradix in |- *; apply RoundedModeUlp with P; auto.
pattern (FtoRradix y) at 1 in |- *;
 replace (FtoRradix y) with
  ((FtoRradix x - (FtoRradix x - FtoRradix q × FtoRradix y)) × / FtoRradix q)%R;
 [ idtac | field; auto ].
rewrite Rabs_mult.
rewrite Rmult_assoc.
replace (Rabs (/ FtoRradix q) × Fulp b radix precision q)%R with
 (/ Zabs (Fnum (Fnormalize radix b precision q)))%R;
 [ rewrite Rmult_comm | idtac ].
apply Rmult_le_compat_l; auto with real.
replace (FtoRradix x - (FtoRradix x - FtoRradix q × FtoRradix y))%R with
 (- (FtoRradix x - FtoRradix q × FtoRradix y) + FtoRradix x)%R;
 [ idtac | ring ].
rewrite <- (Rabs_Ropp (FtoRradix x - FtoRradix q × FtoRradix y));
 apply Rabs_triang.
rewrite Rabs_Rinv; auto; rewrite Hq; unfold FtoRradix in |- *;
 rewrite <- Fabs_correct; auto.
unfold Fabs, FtoR in |- *; simpl in |- *; rewrite Rinv_mult_distr;
 auto with real zarith.
rewrite Rmult_assoc; unfold Fulp in |- *; rewrite Rinv_l;
 auto with real zarith.
Qed.

Theorem errorBoundedDivSimplHyp :
  (x y q : float) P,
 RoundedModeP b radix P
 Fbounded b x
 Fbounded b y
 Fbounded b q
 FtoRradix y 0%R
 P (x / y)%R q
 (- dExp b Fexp (Fnormalize radix b precision x) - precision)%Z
 (- dExp b Fexp q + Fexp y)%Z.
intros x y q P HP Fx Fy Fq Hy Hq H.
cut (IZR (Zpos (vNum b)) = powerRZ radix precision);
 [ intros V | rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision x));
 [ intros H1; case H1; intros H2 | apply FnormalizeCanonic; auto with arith ].
apply Zle_trans with (1 := H); apply Zlt_succ_le.
apply Zplus_lt_reg_l with (-1 + (precision + - Fexp y))%Z;
 unfold Zsucc in |- ×.
ring_simplify (-1 + (precision + - Fexp y) + (Fexp q + Fexp y + 1))%Z.
replace
 (-1 + (precision + - Fexp y) +
  (Fexp (Fnormalize radix b precision x) - precision))%Z with
 (Zpred precision + Fexp (Fnormalize radix b precision x) +
  - (precision + Fexp y))%Z; [ idtac | unfold Zpred in |- *; ring ].
apply Zlt_powerRZ with (IZR radix); [ idtac | rewrite powerRZ_add ];
 auto with zarith real.
apply Rle_lt_trans with (Rabs x × powerRZ radix (- (precision + Fexp y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
unfold FtoRradix in |- *;
 rewrite <- FnormalizeCorrect with (precision := precision) (b := b);
 auto.
rewrite <- Fabs_correct; auto with zarith; unfold Fabs, FtoR in |- *;
 simpl in |- ×.
rewrite powerRZ_add; auto with zarith real; apply Rmult_le_compat_r;
 auto with real zarith.
elim H2; intros H3 H4; apply Rmult_le_reg_l with (IZR radix);
 auto with zarith real.
apply Rle_trans with (IZR (Zpos (vNum b)));
 [ rewrite V; right | idtac ].
pattern (IZR radix) at 1 in |- *; replace (IZR radix) with (powerRZ radix 1);
 [ idtac | simpl in |- *; ring ].
unfold Zpred in |- *; rewrite <- powerRZ_add;
 [ ring_simplify (1 + (precision + -1))%Z | idtac ]; auto with zarith real.
rewrite <- (Rabs_right radix);
 [ idtac | apply Rle_ge; auto with zarith real ].
rewrite Faux.Rabsolu_Zabs; rewrite <- Rmult_IZR; rewrite <- Zabs_Zmult;
 auto with real zarith.
apply Rle_lt_trans with (Rabs (FtoRradix x) × / Rabs (FtoRradix y))%R.
apply Rmult_le_compat_l; auto with real; rewrite powerRZ_Zopp;
 auto with real zarith.
apply Rle_Rinv; auto with real zarith.
cut (0 Rabs (FtoRradix y))%R; [ intros H3; case H3 | idtac ];
 auto with real.
intros H4; Contradict H4; apply not_eq_sym; apply Rabs_no_R0; auto.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith;
 unfold Fabs, FtoR in |- *; simpl in |- ×.
rewrite powerRZ_add; [ apply Rmult_le_compat_r | idtac ];
 auto with real zarith float.
rewrite <- V; auto with float real.
apply Rplus_lt_reg_r with (- Fulp b radix precision q)%R.
apply Rlt_le_trans with (Rabs q).
apply Rplus_lt_reg_r with (Fulp b radix precision q + - Rabs (FtoRradix q))%R.
ring_simplify.
rewrite <- Rabs_Rinv; auto; rewrite <- Rabs_mult.
rewrite Rmult_comm.
apply Rle_lt_trans with (Rabs (/ FtoRradix y × FtoRradix x) - Rabs (FtoRradix q))%R;
  [right; ring|idtac].
apply Rle_lt_trans with (Rabs (/ FtoRradix y × FtoRradix x - FtoRradix q));
 [ apply Rabs_triang_inv | idtac ].
unfold FtoRradix in |- *; apply RoundedModeUlp with P; auto with real.
fold FtoRradix in |- *;
 replace (/ FtoRradix y × FtoRradix x)%R with (FtoRradix x / FtoRradix y)%R;
 [ auto | unfold Rdiv in |- *; ring ].
apply
 Rle_trans
  with (- powerRZ radix (Fexp q) + powerRZ radix (Fexp q + precision))%R.
rewrite powerRZ_add; auto with zarith real.
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith;
 unfold Fabs, FtoR in |- *; simpl in |- ×.
apply
 Rle_trans with ((-1 + powerRZ radix precision) × powerRZ radix (Fexp q))%R;
 [ apply Rmult_le_compat_r; auto with real zarith | right; ring ].
apply Rle_trans with (IZR (Zpred (Zpos (vNum b))));
 auto with real zarith float.
unfold Zpred in |- *; rewrite plus_IZR; rewrite Rplus_comm;
 apply Rplus_le_compat; right; auto with real zarith float.
rewrite Zplus_comm; apply Rplus_le_compat_r; apply Ropp_le_contravar; unfold Fulp in |- *;
 apply Rle_powerRZ; auto with zarith real.
apply FcanonicLeastExp with radix b precision; auto with zarith float real.
apply sym_eq; apply FnormalizeCorrect; auto.
elim H2; intros H3 H4; elim H4; intros H5 H6.
absurd (- dExp b Fexp (Fnormalize radix b precision x) - precision)%Z;
  auto with zarith.
Qed.

Theorem errorBoundedDivClosest :
  x y q : float,
 Fbounded b x
 Fbounded b y
 Fbounded b q
 FtoRradix y 0%R
 Closest b radix (x / y) q
 (- dExp b Fexp q + Fexp y)%ZFbounded b (Fminus radix x (Fmult q y)).
intros x y q Fx Fy Fq H2 H3 H.
apply errorBoundedDiv with (Closest b radix); auto.
apply ClosestRoundedModeP with precision; auto.
case (Req_dec (Rabs (FtoRradix q)) (powerRZ radix (- dExp b))); intros H4;
 auto.
right.
case
 (Rle_or_lt (powerRZ radix (- dExp b) / 2%nat)
    (Rabs (FtoRradix x / FtoRradix y))); auto.
intros H5; elim H3; intros H6 H7.
absurd
 (powerRZ radix (- dExp b) / 2%nat < powerRZ radix (- dExp b) / 2%nat)%R;
 auto with real.
apply Rle_lt_trans with (2 := H5).
apply
 Rle_trans
  with (powerRZ radix (- dExp b) + - (powerRZ radix (- dExp b) / 2%nat))%R.
unfold Rdiv in |- *;
 apply Rle_trans with (powerRZ radix (- dExp b) × (1 + - / 2%nat))%R;
 [ apply Rmult_le_compat_l; auto with real zarith | right; ring; ring ].
right; simpl in |- *; field; auto with real.
apply Rle_trans with (Rabs q - Rabs (x / y))%R.
unfold Rminus in |- *; rewrite H4; apply Rplus_le_compat_l;
 apply Ropp_le_contravar; auto with real.
apply Rle_trans with (Rabs (FtoRradix q - FtoRradix x / FtoRradix y));
 [ apply Rabs_triang_inv | idtac ].
apply
 Rle_trans
  with (Rabs (FtoR radix (Fzero (- dExp b)) - FtoRradix x / FtoRradix y)).
apply H7; apply FboundedFzero.
rewrite FzeroisZero; ring_simplify (0 - FtoRradix x / FtoRradix y)%R.
rewrite Rabs_Ropp; auto with real.
Qed.

Theorem errorBoundedDivToZero :
  x y q : float,
 Fbounded b x
 Fbounded b y
 Fbounded b q
 FtoRradix y 0%R
 ToZeroP b radix (x / y) q
 (- dExp b Fexp q + Fexp y)%ZFbounded b (Fminus radix x (Fmult q y)).
intros x y q Fx Fy Fq H2 H3 H.
apply errorBoundedDiv with (ToZeroP b radix); auto.
apply ToZeroRoundedModeP with precision; auto.
case (Req_dec (Rabs (FtoRradix q)) (powerRZ radix (- dExp b))); intros H4;
 auto.
right.
case H3; intros H'; elim H'; [ unfold isMin in |- × | unfold isMax in |- × ];
 intros H5 H6; clear H'; elim H6; intros H7 H8; elim H8;
 clear H6 H8; fold FtoRradix in |- *; intros H6 H8.
apply Rle_trans with (powerRZ radix (- dExp b));
 [ unfold Rdiv in |- × | idtac ].
apply Rle_trans with (powerRZ radix (- dExp b) × 1)%R;
 [ apply Rmult_le_compat_l; auto with real zarith | right; ring ].
rewrite <- Rinv_1; simpl in |- *; apply Rle_Rinv; auto with real.
rewrite <- H4; repeat rewrite Rabs_right; auto with real float.
apply Rle_ge; unfold FtoRradix in |- *;
 apply
  RleRoundedR0
   with b precision (ToZeroP b radix) (FtoRradix x / FtoRradix y)%R;
 auto with float real zarith.
apply ToZeroRoundedModeP with precision; auto.
apply Rle_trans with (powerRZ radix (- dExp b));
 [ unfold Rdiv in |- × | idtac ].
apply Rle_trans with (powerRZ radix (- dExp b) × 1)%R;
 [ apply Rmult_le_compat_l; auto with real zarith | right; ring ].
rewrite <- Rinv_1; simpl in |- *; apply Rle_Rinv; auto with real.
rewrite <- H4; repeat rewrite Faux.Rabsolu_left1; auto with real float.
unfold FtoRradix in |- *;
 apply
  RleRoundedLessR0
   with b precision (ToZeroP b radix) (FtoRradix x / FtoRradix y)%R;
 auto with float real zarith.
apply ToZeroRoundedModeP with precision; auto.
Qed.

Theorem errorBoundedSqrt :
  x q : float,
 (Fbounded b x) → (Fbounded b q) →
 (0 x)%R → (Closest b radix (sqrt x) q) →
 (- dExp b Fexp q + Fexp q)%Z
   (Fbounded b (Fminus radix x (Fmult q q))).
intros x q Fx Fq H1 H2 H3.
cut (FtoRradix q = Fnormalize radix b precision q);
 [ intros Hq
 | apply sym_eq; unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ].
cut (Fcanonic radix b (Fnormalize radix b precision q));
 [ intros Cq | apply FnormalizeCanonic; auto with arith ].
cut (0 q)%R; [ intros H'1 | idtac ].
2: unfold FtoRradix in |- *;
    apply RleRoundedR0 with b precision (Closest b radix) (sqrt x);
    auto with float zarith real.
2: apply ClosestRoundedModeP with precision; auto.
2: rewrite <- sqrt_0; apply sqrt_le_1; auto with real.
cut (Rabs (sqrt x - q) Fulp b radix precision q × / 2%nat)%R;
 [ intros H'2 | idtac ].
2: apply Rmult_le_reg_l with (INR 2); auto with real arith.
2: apply Rle_trans with (Fulp b radix precision q);
    [ unfold FtoRradix in |- *; apply ClosestUlp; auto | right ].
2: apply trans_eq with (Fulp b radix precision q × (2%nat × / 2%nat))%R;
    [ rewrite Rinv_r; auto with real | idtac ]; ring.
case (Zle_or_lt (Fexp q + Fexp q) (Fexp x)); intros H4.
split; [ idtac | simpl in |- *; rewrite Zmin_le2; auto ].
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs.
replace (IZR (Fnum (Fminus radix x (Fmult q q)))) with
 (Fminus radix x (Fmult q q) ×
  powerRZ radix (- Fexp (Fminus radix x (Fmult q q))))%R.
2: unfold FtoRradix in |- *; unfold FtoR in |- *; rewrite Rmult_assoc.
2: rewrite <- powerRZ_add; auto with real zarith.
2: ring_simplify
       (Fexp (Fminus radix x (Fmult q q)) +
        - Fexp (Fminus radix x (Fmult q q)))%Z; auto with real.
simpl in |- *; rewrite Zmin_le2; auto; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (- (Fexp q + Fexp q))));
 [ idtac | apply Rle_ge; auto with real zarith ].
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
replace (FtoRradix x - FtoRradix q × FtoRradix q)%R with
 ((sqrt x - q) × (sqrt x + q))%R;
 [ rewrite Rabs_mult | idtac ].
2: apply trans_eq with ((sqrt x)*(sqrt x)-q×q)%R; try ring.
2: rewrite sqrt_def; auto with real.
apply
 Rle_lt_trans
  with
    (Fulp b radix precision q × / 2%nat ×
     Rabs (sqrt (FtoRradix x) + FtoRradix q) ×
     powerRZ radix (- (Fexp q + Fexp q)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply
 Rle_lt_trans
  with
    (Fulp b radix precision q × / 2%nat ×
     (2 × Rabs q + Fulp b radix precision q × / 2%nat) ×
     powerRZ radix (- (Fexp q + Fexp q)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_compat_l;
 [ unfold Fulp in |- *; auto with real zarith float | idtac ].
apply Rmult_le_pos; auto with real zarith float.
replace (sqrt (FtoRradix x) + FtoRradix q)%R with
 (sqrt (FtoRradix x) - FtoRradix q + 2 × FtoRradix q)%R;
 [ idtac | ring ].
apply
 Rle_trans
  with (Rabs (sqrt (FtoRradix x) - FtoRradix q) + Rabs (2 × FtoRradix q))%R;
 [ apply Rabs_triang | idtac ].
rewrite Rplus_comm; apply Rplus_le_compat; auto.
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
apply Rle_ge; auto with real.
unfold Fulp in |- *; rewrite Hq.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp (Fnormalize radix b precision q))));
 [ idtac | apply Rle_ge; auto with real zarith ].
apply
 Rle_lt_trans
  with
    (powerRZ radix (- (Fexp q + Fexp q)) ×
     (powerRZ radix (Fexp (Fnormalize radix b precision q)) ×
      powerRZ radix (Fexp (Fnormalize radix b precision q))) ×
     (/ 2 × 2 × Rabs (Fnum (Fnormalize radix b precision q)) + / 2 × / 2))%R;
 [ right; ring | idtac ].
repeat rewrite <- powerRZ_add; auto with zarith real.
rewrite Rinv_l; auto with real.
apply
 Rle_lt_trans
  with
    (powerRZ radix 0 ×
     (1 × Rabs (Fnum (Fnormalize radix b precision q)) + / 2 × / 2))%R.
apply Rmult_le_compat_r; auto with real zarith.
replace 0%R with (0 + 0)%R;
 [ apply Rplus_le_compat; auto with real zarith | ring ].
apply Rmult_le_pos; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Zplus_le_reg_l with (Fexp q + Fexp q)%Z.
ring_simplify.
apply Zmult_le_compat_l; auto with zarith.
apply FcanonicLeastExp with radix b precision; auto with arith.
simpl in |- *;
 ring_simplify (1 × (1 × Rabs (Fnum (Fnormalize radix b precision q)) + / 2 × / 2))%R;
 rewrite Faux.Rabsolu_Zabs.
apply Rle_lt_trans with (Zpred (Zpos (vNum b))+(/ 2)^2 )%R;
 auto with real float zarith.
apply Rplus_le_compat_r; auto with real float zarith.
replace (IZR (Zpred (Zpos (vNum b)))) with
 (nat_of_P (vNum b) + -1)%R.
apply Rle_lt_trans with (-1 + / 2 × / 2 + nat_of_P (vNum b))%R;
 [ right; ring | idtac ].
apply Rlt_le_trans with (0 + nat_of_P (vNum b))%R;
 [ apply Rplus_lt_compat_r | right; ring ].
apply Rplus_lt_reg_r with 1%R; ring_simplify.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with (/2)%R;[right;field; auto with real|idtac].
ring_simplify (2×1)%R; apply Rmult_lt_reg_l with 2%R; auto with real; rewrite Rinv_r; auto with real.
apply Rlt_le_trans with 2%R; auto with real.
unfold Zpred in |- *; rewrite plus_IZR; simpl in |- *; auto with real.
case (Req_dec x 0); intros H5.
cut (is_Fzero x); [ idtac | apply is_Fzero_rep2 with radix; auto ].
cut (is_Fzero q);
 [ unfold is_Fzero in |- × | apply is_Fzero_rep2 with radix; auto ].
intros H6 H7; unfold Fmult, Fminus, Fopp, Fplus in |- *; simpl in |- *;
 rewrite H6; rewrite H7; simpl in |- ×.
rewrite Zmin_le1; auto with zarith.
repeat (split; simpl in |- *; auto with zarith float).
cut (ProjectorP b radix (Closest b radix));
 [ unfold ProjectorP in |- *; intros H6
 | apply RoundedProjector; auto with float zarith ].
2: apply ClosestRoundedModeP with precision; auto.
rewrite <- (FzeroisReallyZero radix (- dExp b)).
apply sym_eq; apply H6; auto.
unfold Fzero in |- *; repeat (split; simpl in |- *; auto with zarith float).
replace (FtoR radix (Fzero (- dExp b))) with (sqrt (FtoRradix x)); auto.
rewrite H5; rewrite FzeroisReallyZero; apply sqrt_0.
case Cq; intros Cq2.
split.
2: unfold Fmult, Fminus, Fopp, Fplus in |- *; simpl in |- *; rewrite Zmin_le1;
    auto with zarith float.
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs.
replace (IZR (Fnum (Fminus radix x (Fmult q q)))) with
 (Fminus radix x (Fmult q q) ×
  powerRZ radix (- Fexp (Fminus radix x (Fmult q q))))%R.
2: unfold FtoRradix in |- *; unfold FtoR in |- *; rewrite Rmult_assoc.
2: rewrite <- powerRZ_add; auto with real zarith.
2: ring_simplify
       (Fexp (Fminus radix x (Fmult q q)) +
        - Fexp (Fminus radix x (Fmult q q)))%Z; auto with real.
apply Rle_lt_trans with (IZR (Zabs (Fnum x)));
 [ idtac | auto with float zarith real ].
simpl in |- *; rewrite Zmin_le1; auto with zarith; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (- Fexp x)));
 [ idtac | apply Rle_ge; auto with real zarith ].
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
apply Rmult_le_reg_l with (powerRZ radix (Fexp x)); auto with real zarith.
apply
 Rle_trans
  with
    (Rabs (FtoRradix x - FtoRradix q × FtoRradix q) ×
     (powerRZ radix (Fexp x) × powerRZ radix (- Fexp x)))%R;
 [ right; ring | rewrite <- powerRZ_add; auto with real zarith ].
ring_simplify (Fexp x + - Fexp x)%Z; simpl in |- ×.
ring_simplify (Rabs (FtoRradix x - FtoRradix q × FtoRradix q) × 1)%R.
replace (powerRZ radix (Fexp x) × Zabs (Fnum x))%R with (Rabs x);
 [ idtac
 | unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto;
    unfold FtoR in |- *; simpl in |- *; ring ].
cut
 ( v w : R,
  (0 v)%R → (0 w)%R → (w 2 × v)%R → (Rabs (v - w) Rabs v)%R);
 [ intros H6; apply H6; auto with real | idtac ].
apply Rmult_le_pos; auto.
cut (0 < 1 - / 2%nat × powerRZ radix (Zsucc (- precision)))%R;
 [ intros H'3 | idtac ].
2: apply
    Rplus_lt_reg_r with (/ 2%nat × powerRZ radix (Zsucc (- precision)))%R.
2: ring_simplify.
2: apply Rlt_trans with (/ 2%nat×powerRZ radix 0 )%R; auto with real zarith.
2: simpl in |- *; ring_simplify ( / 2×1)%R; pattern 1%R at 3 in |- *;
    rewrite <- Rinv_1; auto with real.
apply
 Rle_trans
  with
    (Rsqr (sqrt x × / (1 - / 2%nat × powerRZ radix (Zsucc (- precision))))).
fold (Rsqr (FtoRradix q)) in |- *; apply Rsqr_le_abs_1.
rewrite Rabs_mult.
rewrite (Rabs_right (/ (1 - / 2%nat × powerRZ radix (Zsucc (- precision)))));
 [ idtac | apply Rle_ge; auto with real ].
apply
 Rmult_le_reg_l with (1 - / 2%nat × powerRZ radix (Zsucc (- precision)))%R;
 auto.
ring_simplify
    ((1 - / 2%nat × powerRZ radix (Zsucc (- precision))) × Rabs (FtoRradix q))%R.
apply
 Rle_trans
  with
    (Rabs (sqrt (FtoRradix x)) ×
     ((1 - / 2%nat × powerRZ radix (Zsucc (- precision))) ×
      / (1 - / 2%nat × powerRZ radix (Zsucc (- precision)))))%R;
 [ idtac | right; ring; ring ].
rewrite Rinv_r; auto with real.
ring_simplify (Rabs (sqrt (FtoRradix x)) × 1)%R.
apply Rle_trans with (- (/ 2%nat × Fulp b radix precision q)+Rabs q)%R.
apply Rplus_le_compat_r; repeat rewrite Ropp_mult_distr_l_reverse.
apply Ropp_le_contravar.
rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real.
unfold FtoRradix in |- *; rewrite Rmult_comm; apply FulpLe2; auto.
apply
 Rplus_le_reg_l
  with (- Rabs (sqrt (FtoRradix x)) + / 2%nat × Fulp b radix precision q)%R.
ring_simplify.
apply Rle_trans with (Rabs (q - sqrt (FtoRradix x))).
apply Rle_trans with (Rabs q - Rabs (sqrt (FtoRradix x)))%R;
 [ right; ring | apply Rabs_triang_inv ].
rewrite <- Rabs_Ropp.
replace (- (FtoRradix q - sqrt (FtoRradix x)))%R with
 (sqrt (FtoRradix x) - FtoRradix q)%R;
   [ apply Rle_trans with (1:=H'2);auto with real| ring ].
rewrite Rsqr_mult; rewrite Rsqr_sqrt; auto.
rewrite Rmult_comm; apply Rmult_le_compat_r; auto.
cut (0 < 1 - / 2%nat × powerRZ radix (Zsucc (- 2%nat)))%R;
 [ intros H'4 | idtac ].
2: apply Rplus_lt_reg_r with (/ 2%nat × powerRZ radix (Zsucc (- 2%nat)))%R.
2: ring_simplify.
2: apply Rlt_trans with (/ 2%nat × powerRZ radix 0 )%R; auto with real zarith.
2: simpl in |- *; ring_simplify ( / 2×1)%R; pattern 1%R at 3 in |- *;
    rewrite <- Rinv_1; auto with real.
apply
 Rle_trans with (Rsqr (/ (1 - / 2%nat × powerRZ radix (Zsucc (- 2%nat))))).
apply Rsqr_le_abs_1.
rewrite Rabs_right; [ idtac | apply Rle_ge; auto with real ].
rewrite Rabs_right; [ idtac | apply Rle_ge; auto with real zarith ].
apply Rle_Rinv; auto with real zarith.
unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (Rsqr (4%nat × / 3%nat)).
apply Rsqr_le_abs_1.
rewrite Rabs_right; [ idtac | apply Rle_ge; auto with real ].
rewrite Rabs_right; [ idtac | apply Rle_ge; auto with real zarith arith ].
2: apply Rmult_le_pos; auto with real arith.
apply Rle_trans with (/ (3%nat × / 4%nat))%R;
 [ idtac | right; field; auto with arith real ].
apply Rle_Rinv; auto with real arith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rle_trans with (1 - / 2%nat × / 2%nat)%R.
rewrite <- Rinv_mult_distr; auto with arith real;
 replace 1%R with (4%nat × / 4%nat)%R; auto with real.
simpl in |- *; replace 4%R with (2 + 1 + 1)%R; [ right; ring | ring ].
unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real zarith.
unfold powerRZ in |- *; simpl in |- *; ring_simplify (radix × 1)%R.
apply Rle_Rinv; auto with real zarith.
replace 2%R with (IZR (Zsucc 1)); auto with real zarith.
replace (2 + 1 + 1)%R with (INR 4); auto with real.
unfold Rsqr in |- *; apply Rmult_le_reg_l with (3%nat × 3%nat)%R;
 auto with real arith.
apply Rmult_lt_0_compat; auto with real arith zarith.
apply
 Rle_trans with (3%nat × / 3%nat × (4%nat × 4%nat × (3%nat × / 3%nat)))%R;
 [ right; ring | idtac ].
repeat rewrite Rinv_r; auto with real arith zarith.
simpl in |- *; ring_simplify.
apply Rle_trans with (16+0)%R; auto with real.
apply Rle_trans with (16+2)%R; auto with real.
right; ring.
intros v w Hv Hw Hvw; unfold Rminus in |- ×.
rewrite (Rabs_right v); [ idtac | apply Rle_ge; auto ].
case (Rcase_abs (v + - w)); intros H'.
rewrite Rabs_left; auto with real.
apply Rplus_le_reg_l with v; ring_simplify (v + - (v + - w))%R; auto with real.
apply Rle_trans with (1 := Hvw); right; ring.
rewrite Rabs_right; auto.
apply Rle_trans with (v + -0)%R; [ auto with real | right; ring ].
case (Req_dec q 0); intros H6.
cut (is_Fzero q);
 [ unfold is_Fzero in |- × | apply is_Fzero_rep2 with radix; auto ].
intros H7; unfold Fmult, Fminus, Fopp, Fplus in |- *; simpl in |- *;
 rewrite H7; simpl in |- ×.
rewrite Zmin_le1; auto with zarith.
ring_simplify (Fexp x - Fexp x)%Z; unfold Zpower_nat in |- *; simpl in |- *;
 auto with zarith float.
ring_simplify (Fnum x × 1 + 0)%Z; auto with float.
split; [ idtac | simpl in |- *; rewrite Zmin_le1; auto with zarith float ].
apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs.
replace (IZR (Fnum (Fminus radix x (Fmult q q)))) with
 (Fminus radix x (Fmult q q) ×
  powerRZ radix (- Fexp (Fminus radix x (Fmult q q))))%R.
2: unfold FtoRradix in |- *; unfold FtoR in |- *; rewrite Rmult_assoc.
2: rewrite <- powerRZ_add; auto with real zarith.
2: ring_simplify
       (Fexp (Fminus radix x (Fmult q q)) +
        - Fexp (Fminus radix x (Fmult q q)))%Z; auto with real.
simpl in |- *; rewrite Zmin_le1; auto with zarith float; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (- Fexp x)));
 [ idtac | apply Rle_ge; auto with real zarith ].
unfold FtoRradix in |- *; rewrite Fminus_correct; auto; rewrite Fmult_correct;
 auto; fold FtoRradix in |- ×.
replace (FtoRradix x - FtoRradix q × FtoRradix q)%R with
 ((sqrt x - q) × (sqrt x + q))%R;
 [ rewrite Rabs_mult | idtac ].
2: apply trans_eq with (sqrt x×sqrt x - q × q)%R; try ring.
2: rewrite sqrt_def; auto with real.
apply
 Rle_lt_trans
  with
    (Fulp b radix precision q × / 2%nat ×
     Rabs (sqrt (FtoRradix x) + FtoRradix q) × powerRZ radix (- Fexp x))%R.
apply Rmult_le_compat_r; auto with real zarith.
elim Cq2; intros H7 H8; elim H8; clear H7 H8; intros H7 H8.
apply
 Rle_lt_trans
  with
    (Fulp b radix precision q × / 2%nat ×
     (2 × Rabs (sqrt (FtoRradix x)) + Fulp b radix precision q × / 2%nat) ×
     powerRZ radix (- Fexp x))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_pos; unfold Fulp in |- *; auto with arith real.
replace (sqrt (FtoRradix x) + FtoRradix q)%R with
 (FtoRradix q - sqrt (FtoRradix x) + 2 × sqrt (FtoRradix x))%R;
 [ idtac | ring ].
apply
 Rle_trans
  with
    (Rabs (FtoRradix q - sqrt (FtoRradix x)) + Rabs (2 × sqrt (FtoRradix x)))%R;
 [ apply Rabs_triang | idtac ].
rewrite Rplus_comm; apply Rplus_le_compat; auto.
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
apply Rle_ge; auto with real.
rewrite <- Rabs_Ropp.
replace (- (FtoRradix q - sqrt (FtoRradix x)))%R with
 (sqrt (FtoRradix x) - FtoRradix q)%R; [ auto | ring ].
unfold Fulp in |- *; rewrite H7.
ring_simplify.
cut (0 Fnum x)%Z; [ intros H'3 | apply LeR0Fnum with radix; auto ].
apply Rle_lt_trans with (/ 2%nat × / 2%nat + Fnum x)%R;
 [ apply Rplus_le_compat | idtac ].
apply
 Rle_trans
  with
    (powerRZ radix (- dExp b) × powerRZ radix (- dExp b) ×
     powerRZ radix (- Fexp x) × (/ 2%nat × / 2%nat))%R;
 [ right; ring | rewrite <- powerRZ_add; auto with zarith real ].
rewrite <- powerRZ_add; auto with zarith real.
apply Rle_trans with (powerRZ radix 0 × (/ 2%nat × / 2%nat))%R;
 [ idtac | simpl in |- *; right; ring ].
apply Rmult_le_compat_r; auto with real.
apply Rmult_le_pos; auto with real.
apply Rle_powerRZ; auto with real zarith float.
apply Zplus_le_reg_l with (Fexp x).
ring_simplify; auto with float.
apply Zle_trans with (- dExp b)%Z; auto with zarith float.
cut (0 dExp b)%Z; auto with zarith; case (dExp b); auto with zarith.
apply
 Rle_trans
  with
    (2 × / 2%nat ×
     (powerRZ radix (- dExp b) × powerRZ radix (- Fexp x) ×
      Rabs (sqrt (FtoRradix x))))%R; [ right; ring | simpl in |- × ].
rewrite Rinv_r; auto with real.
ring_simplify.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply sqrt_positivity; auto ].
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite sqrt_mult; auto with real float zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite <- (sqrt_def (powerRZ radix (- dExp b + - Fexp x)));
 auto with zarith real.
rewrite <- sqrt_mult; auto with real zarith.
rewrite Rmult_comm with (r1:=(sqrt (Fnum x))).
rewrite <- Rmult_assoc; rewrite <- sqrt_mult; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_trans with (1×sqrt (Fnum x))%R;
 [ apply Rmult_le_compat_r | idtac ].
apply sqrt_positivity; auto with real zarith.
rewrite <- sqrt_1; apply sqrt_le_1; auto with real zarith.
replace 1%R with (powerRZ radix 0); [ apply Rle_powerRZ | simpl in |- × ];
 auto with real zarith.
ring_simplify (Fexp x + (- Fexp x + - dExp b + (- Fexp x + - dExp b)))%Z.
apply Zplus_le_reg_l with (Fexp x).
ring_simplify.
apply Zle_trans with (- dExp b)%Z; auto with zarith float.
cut (0dExp b)%Z; auto with zarith; case (dExp b); auto with zarith.
ring_simplify (1×sqrt (Fnum x) )%R.
cut ( z : R, (0 z)%R → (1 z)%R → (sqrt z z)%R);
 [ intros V | idtac ].
apply V; auto with real float zarith.
cut (0%Z Fnum x); auto with zarith float real.
Contradict H5; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite <- H5;
 simpl; ring.
intros z V1 V'; case V'; intros V''.
apply Rlt_le; apply sqrt_less; auto with real.
rewrite <- V''; rewrite sqrt_1; auto with real.
apply Rmult_le_pos; auto with real zarith.
apply Rle_lt_trans with (/ 2%nat × / 2%nat + (Zpos (vNum b) + -1))%R.
apply Rplus_le_compat_l.
rewrite <- (Zabs_eq (Fnum x)); auto.
apply Rle_trans with (IZR (Zpred (Zpos (vNum b))));
 auto with zarith real float.
unfold Zpred in |- *; right; auto with zarith real.
rewrite plus_IZR; auto with real zarith.
simpl in |- *; apply Rplus_lt_reg_r with (1 + - nat_of_P (vNum b))%R.
ring_simplify.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with 1%R;[right; field; auto with real|ring_simplify; auto with real].
apply Rlt_le_trans with 2%R; auto with real.
Qed.

End FroundDiv.