Library Float.Others.PradixE

Require Export FroundPlus.
Section prog.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.

Coercion Local FtoRradix := FtoR radix.
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.
Variable P : RfloatProp.
Hypothesis ProundedMode : RoundedModeP b radix P.

Let Cp := RoundedModeP_inv2 b radix P ProundedMode.
Variable fplus : floatfloatfloat.
Variable fminus : floatfloatfloat.
Variable fmult : floatfloatfloat.
Hypothesis
  fplusCorrect :
     p q : float, Fbounded b pFbounded b qP (p + q) (fplus p q).
Hypothesis
  fminusCorrect :
     p q : float,
    Fbounded b pFbounded b qP (p - q) (fminus p q).
Hypothesis
  fmultCorrect :
     p q : float, Fbounded b pFbounded b qP (p × q) (fmult p q).
Variables f0 f1 f2 : float.
Variable f0Bounded : Fbounded b f0.
Variable f0Correct : f0 = 0%Z :>R.
Variable f1Bounded : Fbounded b f1.
Variable f1Correct : f1 = 1%Z :>R.
Variable f2Bounded : Fbounded b f2.
Variable f2Correct : f2 = 2%Z :>R.

Theorem Loop0 :
  p : float,
 Fbounded b p
  n : Z,
 (1 n)%Z
 (n pPred (vNum b))%Zp = n :>Rfplus p f1 = (p + f1)%R :>R.
intros p H' n H'0 H'1 H'2.
case (FboundNext _ radixMoreThanOne b precision) with (p := Float n 0%nat);
 auto with arith; fold FtoRradix in |- ×.
repeat split; simpl in |- *; auto with zarith arith.
rewrite Zabs_eq; auto with zarith.
rewrite (fun xZsucc_pred (Zpos x)); auto with zarith.
case (dExp b); auto with zarith.
intros x (H'3, H'4).
cut ((p + f1)%R = FtoRradix x); [ intros Eq1; rewrite Eq1 | idtac ].
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto; fold FtoRradix in |- ×.
apply Cp with (1 := fplusCorrect _ _ H' f1Bounded); auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + f1)%R);
 auto.
rewrite H'4; rewrite H'2; rewrite f1Correct;
 unfold FtoRradix, FtoR, Zsucc in |- *; simpl in |- *;
 rewrite plus_IZR; simpl in |- *; repeat rewrite <- INR_IZR_INZ;
 ring.
Qed.

Theorem Loop1 :
  p : float,
 Fbounded b p
  n : Z,
 (Zpos (vNum b) n)%Z
 (n radix × pPred (vNum b))%Z
 p = n :>Rfplus p f1 = p :>R fplus p f1 = (p + radix)%R :>R.
intros p H' n H'0 H'1 H'2.
replace (IZR radix) with (powerRZ radix 1%nat);
 [ idtac | simpl in |- *; ring ].
apply (InBinade b radix precision) with (q := f1) (P := P); auto with zarith;
 fold FtoRradix in |- ×.
case (dExp b); auto with zarith.
rewrite H'2; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_r;
 rewrite <- Rmult_IZR; pattern radix at 2 in |- *;
 rewrite <- (Zpower_nat_1 radix); try rewrite <- Zpower_nat_is_exp.
replace (pred precision + 1) with precision;
 [ rewrite <- pGivesBound; auto with real | idtac ].
rewrite plus_comm; generalize precisionGreaterThanOne; case precision;
 simpl in |- *; auto; (intros tmp; Contradict tmp; auto with arith).
rewrite H'2; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_r;
 rewrite <- Rmult_IZR; rewrite Zmult_comm; auto with real.
rewrite f1Correct; auto with real arith.
rewrite f1Correct; replace (powerRZ radix 1%nat) with (IZR radix);
 auto with real arith.
Qed.

Theorem Loop2 :
  p : float,
 Fbounded b p
  n : Z,
 (1 n)%Z
 (n pPred (vNum b))%Zp = n :>Rfminus (fplus p f1) p = f1 :>R.
intros p H' n H'0 H'1 H'2.
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
cut (Fbounded b (fplus p f1)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto.
rewrite Loop0 with (n := n); auto.
fold FtoRradix in |- *; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p f1 - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + f1)%R);
 auto.
Qed.

Theorem Loop3 :
  p : float,
 Fbounded b p
  n : Z,
 (Zpos (vNum b) n)%Z
 (n radix × pPred (vNum b))%Z
 p = n :>Rfminus (fplus p f1) p f1 :>R.
intros p H' n H'0 H'1 H'2.
case (Loop1 p) with (n := n); auto; intros Eq1; red in |- *; intros Eq2.
absurd (f1 = f0 :>R).
rewrite f1Correct; rewrite f0Correct; auto with real.
rewrite <- Eq2.
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
cut (Fbounded b (fplus p f1)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto.
rewrite Eq1; fold FtoRradix in |- *; rewrite f0Correct;simpl; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p f1 - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + f1)%R);
 auto.
absurd (f1 = radix :>R).
rewrite f1Correct; apply Rlt_not_eq; auto with real zarith.
rewrite <- Eq2.
replace (IZR radix) with (FtoRradix (Float 1%nat 1%nat)).
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
repeat split; simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
 auto with zarith.
case (dExp b); auto with zarith.
cut (Fbounded b (fplus p f1)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto.
rewrite Eq1; unfold FtoR in |- *; simpl in |- *; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p f1 - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + f1)%R);
 auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
Qed.

Theorem Loop4 :
  p : float,
 Fbounded b p
  n : Z,
 (1 n)%Z → (n pPred (vNum b))%Zp = n :>R → (p < fmult f2 p)%R.
intros p H' n H'0 H'1 H'2.
case (Zle_or_lt (2 × n) (pPred (vNum b))); intros le1.
replace (FtoRradix (fmult f2 p)) with (FtoRradix (Float (2 × n) 0%nat)).
replace (FtoRradix p) with (FtoRradix (Float (1 × n) 0%nat)).
unfold FtoRradix, FtoR in |- *; apply Rlt_monotony_exp; auto with real zarith.
change ((1 × n)%Z < (2 × n)%Z)%R in |- *; apply Rlt_IZR;
 apply Zmult_gt_0_lt_compat_r; auto with zarith.
ring_simplify (1×n)%Z;rewrite H'2; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
apply (RoundedModeProjectorIdemEq b radix precision) with (P := P); auto.
repeat split; auto with zarith.
rewrite Zabs_eq; auto.
rewrite (Zsucc_pred (Zpos (vNum b))); auto with zarith.
change (0 2 × n)%Z in |- *; auto with zarith.
simpl in |- *; case (dExp b); auto with zarith.
apply Cp with (1 := fmultCorrect _ _ f2Bounded H'); auto.
rewrite H'2; rewrite f2Correct; rewrite <- Rmult_IZR;
 unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (f2 × p)%R);
 auto.
cut
 (FtoRradix (Float (nNormMin radix precision) 1%nat) =
  Zpower_nat radix precision);
 [ intros Eq1 | unfold FtoRradix, FtoR, nNormMin in |- *; simpl in |- × ].
apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) 1%nat)).
rewrite H'2; rewrite Eq1; simpl in |- ×.
rewrite <- pGivesBound; rewrite (Zsucc_pred (Zpos (vNum b)));
 auto with real zarith.
apply (RleBoundRoundl b radix precision) with (P := P) (r := (f2 × p)%R);
 auto.
repeat split; simpl in |- *; auto with zarith arith.
rewrite Zabs_eq; auto with float zarith.
apply ZltNormMinVnum; auto with float zarith.
apply Zlt_le_weak; apply nNormPos; auto with float zarith.
case (dExp b); auto with zarith.
fold FtoRradix in |- *; rewrite Eq1.
rewrite f2Correct; rewrite H'2; rewrite <- Rmult_IZR.
apply Rle_IZR.
rewrite <- pGivesBound; rewrite (Zsucc_pred (Zpos (vNum b)));
 auto with zarith.
pattern precision at 2 in |- *; rewrite (S_pred precision 0).
2: apply lt_trans with 1; auto.
replace (S (pred precision)) with (pred precision+1)%nat; auto with zarith.
rewrite Zpower_nat_is_exp; auto with real zarith.
rewrite Zpower_nat_1; rewrite Rmult_IZR; auto with real; ring.
Qed.

Theorem BLoop1 :
  p q : float,
 Fbounded b p
 Fbounded b q
  m n : Z,
 (Zpower_nat radix precision m)%Z
 (m radix × pPred (vNum b))%Z
 p = m :>R
 (1 n)%Z
 (n < radix)%Z
 q = n :>Rfplus p q = p :>R fplus p q = (p + radix)%R :>R.
intros p q H' H'0 m n H'1 H'2 H'3 H'4 H'5 H'6.
replace (IZR radix) with (powerRZ radix 1%nat);
 [ idtac | simpl in |- *; ring ].
apply (InBinade b radix precision) with (P := P) (q := q);
 fold FtoRradix in |- *; auto with zarith.
case (dExp b); auto with zarith.
rewrite H'3; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
rewrite Rmult_1_r; pattern radix at 2 in |- *;
 rewrite <- (Zpower_nat_1 radix); rewrite <- Rmult_IZR;
 rewrite <- Zpower_nat_is_exp.
replace (pred precision + 1) with (S (pred precision));
 [ rewrite <- (S_pred precision 0) | rewrite plus_comm ];
 auto with real arith.
rewrite H'3; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_r;
 rewrite Rmult_comm; rewrite <- Rmult_IZR; auto with real arith.
rewrite H'6; auto with real zarith.
rewrite H'6; replace (powerRZ radix 1%nat) with (IZR radix);
 auto with real zarith.
Qed.

Theorem BLoop2 :
  p q : float,
 Fbounded b p
 Fbounded b q
  m n : Z,
 (Zpower_nat radix precision m)%Z
 (m radix × pPred (vNum b))%Z
 p = m :>R
 (1 n)%Z → (n < radix)%Zq = n :>Rfminus (fplus p q) p q :>R.
intros p q H' H'0 m n H'1 H'2 H'3 H'4 H'5 H'6.
case (BLoop1 p q) with (n := n) (m := m); auto; intros Eq1; red in |- *;
 intros Eq2.
absurd (q = f0 :>R).
rewrite H'6; rewrite f0Correct; auto with real zarith.
rewrite <- Eq2.
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
cut (Fbounded b (fplus p q)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto.
rewrite Eq1; fold FtoRradix in |- *; rewrite f0Correct; simpl; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p q - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + q)%R);
 auto.
absurd (q = radix :>R).
rewrite H'6; auto with real zarith.
rewrite <- Eq2.
replace (IZR radix) with (FtoRradix (Float 1%nat 1%nat)).
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
repeat split; simpl in |- *; auto with zarith.
apply vNumbMoreThanOne with (radix := radix) (precision := precision);
 auto with float zarith.
case (dExp b); auto with zarith.
cut (Fbounded b (fplus p q)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto.
rewrite Eq1; unfold FtoR in |- *; simpl in |- *; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p q - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + q)%R);
 auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
Qed.

Theorem BLoop3 :
  p q : float,
 Fbounded b p
 Fbounded b q
  m : Z,
 (Zpower_nat radix precision m)%Z
 (m radix × pPred (vNum b))%Z
 p = m :>Rq = radix :>Rfminus (fplus p q) p = q :>R.
intros p q H' H'0 m H'1 H'2 H'3 H'4.
cut (fplus p q = (p + q)%R :>R); [ intros Eq1 | idtac ].
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
cut (Fbounded b (fplus p q)); [ intros Fbp | auto ].
apply Cp with (1 := fminusCorrect _ _ Fbp H'); auto; fold FtoRradix in |- ×.
rewrite Eq1; ring.
apply
 RoundedModeBounded with (radix := radix) (P := P) (r := (fplus p q - p)%R);
 auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + q)%R);
 auto.
case
 (FboundNext _ radixMoreThanOne b precision)
  with (p := Fnormalize radix b precision p); auto with arith;
 fold FtoRradix in |- ×.
apply FcanonicBound with (radix := radix); auto.
apply FnormalizeCanonic with (radix := radix) (precision := precision);
 auto with arith.
intros p' H'5; elim H'5; intros H'6 H'7; clear H'5.
cut (Fexp (Fnormalize radix b precision p) = 1%Z); [ intros Eq1 | idtac ].
cut ((p + q)%R = FtoRradix p' :>R); [ intros Eq2 | idtac ].
rewrite Eq2.
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
apply Cp with (1 := fplusCorrect _ _ H' H'0); auto; fold FtoRradix in |- ×.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + q)%R);
 auto.
rewrite H'7.
rewrite H'4.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace
 (Zsucc (Fnum (Fnormalize radix b precision p)) ×
  powerRZ radix (Fexp (Fnormalize radix b precision p)))%R with
 (Fnum (Fnormalize radix b precision p) ×
  powerRZ radix (Fexp (Fnormalize radix b precision p)) +
  powerRZ radix (Fexp (Fnormalize radix b precision p)))%R.
replace
 (Fnum (Fnormalize radix b precision p) ×
  powerRZ radix (Fexp (Fnormalize radix b precision p)))%R with
 (FtoRradix (Fnormalize radix b precision p)); auto.
rewrite (FnormalizeCorrect radix); auto.
rewrite Eq1; unfold FtoR in |- *; simpl in |- *; ring.
unfold Zsucc in |- *; simpl in |- *; rewrite plus_IZR; simpl; ring.
apply boundedNorMinGivesExp; auto with zarith.
case (dExp b); auto with zarith.
fold FtoRradix in |- *; rewrite H'3; unfold FtoRradix, FtoR, nNormMin in |- *;
 simpl in |- ×.
rewrite Rmult_1_r; pattern radix at 2 in |- *;
 rewrite <- (Zpower_nat_1 radix); rewrite <- Rmult_IZR;
 rewrite <- Zpower_nat_is_exp.
replace (pred precision + 1) with (S (pred precision));
 [ rewrite <- (S_pred precision 0) | rewrite plus_comm ];
 auto with real arith.
fold FtoRradix in |- *; rewrite H'3; unfold FtoRradix, FtoR in |- *;
 simpl in |- *; rewrite Rmult_1_r; rewrite Rmult_comm;
 rewrite <- Rmult_IZR; auto with real arith.
Qed.

Theorem BLoop4 :
  p : float,
 Fbounded b p
  n : Z,
 (1 n)%Z → (n < radix)%Zp = n :>R → (p < fplus p f1)%R.
intros p H' n H'0 H'1 H'2.
rewrite Loop0 with (n := n); auto.
rewrite H'2; rewrite f1Correct; auto with real zarith.
apply Zle_trans with (Zpred radix); auto with zarith.
unfold pPred in |- *; apply Zle_Zpred_Zpred.
rewrite <- (Zpower_nat_1 radix); rewrite pGivesBound; auto with real zarith.
Qed.

Lemma Loop6c :
  p b0 : float,
 Fbounded b p
  n : Z,
 (1 n)%Z
 (n pPred (vNum b))%Z
 p = n :>RFbounded b b0 b0 = radix :>R → (p < fmult p b0)%R.
intros p b0 H' n H'0 H'1 H'2 H'3.
Casec H'3; intros Fbb0 H'3.
case (Zle_or_lt (n × radix) (pPred (vNum b))); intros le1.
replace (FtoRradix (fmult p b0)) with (FtoRradix (Float (n × radix) 0%nat)).
rewrite H'2; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
rewrite Rmult_1_r; apply Rlt_IZR.
pattern n at 1 in |- *; replace n with (n × 1)%Z; auto with zarith.
apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply (RoundedModeProjectorIdemEq b radix precision) with (P := P); auto.
repeat split; simpl in |- *; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite (Zsucc_pred (Zpos (vNum b))); auto with zarith.
case (dExp b); auto with zarith.
apply Cp with (1 := fmultCorrect _ _ H' Fbb0); auto.
rewrite H'3; rewrite H'2; unfold FtoRradix, FtoR in |- *; simpl in |- *;
 rewrite Rmult_IZR; ring.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (p × b0)%R);
 auto.
cut
 (FtoRradix (Float (nNormMin radix precision) 1%nat) =
  Zpower_nat radix precision);
 [ intros Eq1 | unfold FtoRradix, FtoR, nNormMin in |- *; simpl in |- × ].
apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) 1%nat)).
rewrite H'2; rewrite Eq1; simpl in |- ×.
rewrite <- pGivesBound; rewrite (Zsucc_pred (Zpos (vNum b)));
 fold pPred in |- *; auto with real zarith.
apply (RleBoundRoundl b radix precision) with (P := P) (r := (p × b0)%R);
 auto.
repeat split; simpl in |- *; auto with zarith arith.
rewrite Zabs_eq; auto with float zarith.
apply ZltNormMinVnum; auto with float zarith.
apply Zlt_le_weak; apply nNormPos; auto with float zarith.
case (dExp b); auto with zarith.
fold FtoRradix in |- *; rewrite Eq1; rewrite <- pGivesBound; rewrite H'2;
 rewrite H'3.
rewrite (Zsucc_pred (Zpos (vNum b))); rewrite <- Rmult_IZR;
 auto with real zarith.
rewrite Rmult_1_r; pattern radix at 2 in |- *;
 rewrite <- (Zpower_nat_1 radix).
rewrite <- Rmult_IZR; repeat rewrite <- Zpower_nat_Z_powerRZ;
 rewrite <- Zpower_nat_is_exp.
replace (pred precision + 1) with precision;
 [ auto | rewrite plus_comm; simpl in |- × ].
generalize precisionGreaterThanOne; case precision; simpl in |- *;
 auto with arith.
intros tmp; Contradict tmp; auto with arith.
Qed.

Let feq := Feq_bool radix.


Theorem Goal1 :
  (x0 : float)
   (Pre2 : ( m : Z,
              (1 m)%Z (m radix × pPred (vNum b))%Z x0 = m :>R)
           Fbounded b x0) (Test1 : feq (fminus (fplus x0 f1) x0) f1 = true),
 Zabs_nat (radix × pPred (vNum b) - Int_part (fmult f2 x0)) <
 Zabs_nat (radix × pPred (vNum b) - Int_part x0)
 ex
   (fun m : Z
    (1 m)%Z (m radix × pPred (vNum b))%Z fmult f2 x0 = m :>R)
 Fbounded b (fmult f2 x0).
intros x0 Pre2 Test1.
Casec Pre2; intros Pre2; Casec Pre2; intros vx0 Pre2; Casec Pre2;
 intros Hv1 Pre2; Casec Pre2; intros Hv2 Hv3 Fb1.
cut
 (ex
    (fun m : Z
     (1 m)%Z
     (m radix × pPred (vNum b))%Z FtoRradix (fmult f2 x0) = m :>R)).
intros Pre2; Casec Pre2; intros va1 Pre2; Casec Pre2; intros Hv1' Pre2;
 Casec Pre2; intros Hv2' Hv3'.
split.
rewrite Hv3'; rewrite Hv3; repeat rewrite Int_part_IZR;
 apply Zabs.Zabs_nat_lt; split; auto with zarith.
unfold Zminus in |- *; apply Zplus_lt_compat_l; auto with zarith;
 apply Zlt_Zopp.
apply Zlt_Rlt.
rewrite <- Hv3'; rewrite <- Hv3.
apply (Loop4 x0 Fb1 vx0); auto.
case (Zle_or_lt (Zpower_nat radix precision) vx0); auto.
intros lte1; absurd (fminus (fplus x0 f1) x0 = f1 :>R).
apply Loop3 with (n := vx0); auto.
rewrite pGivesBound; auto.
generalize Feq_bool_correct_t; unfold Feq in |- ×.
intros H'; apply (H' radix); auto.
rewrite <- pGivesBound; unfold pPred in |- *; auto with zarith.
split; auto.
va1; split; auto.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (f2 × x0)%R);
 auto.
case
 (ZroundZ b radix precision)
  with (P := P) (z := (2 × vx0)%Z) (p := fmult f2 x0);
 auto.
apply Cp with (1 := fmultCorrect _ _ f2Bounded Fb1); auto.
rewrite Hv3; rewrite f2Correct; try rewrite Rmult_IZR; auto with real zarith.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (f2 × x0)%R);
 auto.
intros x H'; x; repeat split; auto.
apply Zle_Rle.
rewrite <- f1Correct; auto.
rewrite <- H'; auto.
apply (RleBoundRoundl b radix precision) with (P := P) (r := (f2 × x0)%R);
 auto.
rewrite Hv3; rewrite f2Correct.
fold FtoRradix in |- *; rewrite f1Correct.
rewrite <- Rmult_IZR; apply Rle_IZR.
apply Zle_trans with (1 := Hv1); auto with zarith.
cut (Float (pPred (vNum b)) 1%nat = (radix × pPred (vNum b))%Z :>R);
 [ intros Eq1 | idtac ].
apply Zle_Rle; rewrite <- Eq1; rewrite <- H'.
apply (RleBoundRoundr b radix precision) with (P := P) (r := (f2 × x0)%R);
 auto.
repeat split; simpl in |- *; auto with zarith.
rewrite Zabs_eq; unfold pPred in |- *; auto with float zarith.
case (dExp b); auto with zarith.
fold FtoRradix in |- *; rewrite Eq1.
rewrite Rmult_IZR; apply Rmult_le_compat; auto.
rewrite f2Correct; replace 0%R with (IZR 0); auto with real zarith.
rewrite Hv3; replace 0%R with (IZR 0); auto with real zarith.
rewrite f2Correct; auto with real zarith.
replace 2%Z with (Zsucc 1); auto with real zarith.
rewrite Hv3.
case (Zle_or_lt vx0 (pPred (vNum b))); auto with real arith.
intros H'0; absurd (fminus (fplus x0 f1) x0 = f1 :>R).
apply Loop3 with (n := vx0); auto.
rewrite (Zsucc_pred (Zpos (vNum b))); auto with zarith.
generalize (Feq_bool_correct_t radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_IZR; ring.
Qed.

Theorem Goal2 :
  (x0 : float)
   (Pre2 : ex
             (fun m : Z
              (1 m)%Z (m radix × pPred (vNum b))%Z x0 = m :>R)
           Fbounded b x0) (Test1 : feq (fminus (fplus x0 f1) x0) f1 = false),
 ex
   (fun m : Z
    (Zpower_nat radix precision m)%Z
    (m radix × pPred (vNum b))%Z x0 = m :>R)
 Fbounded b x0.
intros x0 Pre2 Test1.
Casec Pre2; intros Pre2; Casec Pre2; intros vx0 Pre2; Casec Pre2;
 intros Hv1 Pre2; Casec Pre2; intros Hv2 Hv3 Fb1.
split; auto; auto.
vx0; split; auto.
case (Zle_or_lt (Zpower_nat radix precision) vx0); auto with real arith.
intros H'0; absurd (fminus (fplus x0 f1) x0 = f1 :>R).
generalize (Feq_bool_correct_f radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
apply Loop2 with (n := vx0); auto.
unfold pPred in |- *; rewrite pGivesBound; auto with arith zarith.
Qed.

Theorem Goal3 :
 ex
   (fun m : Z
    (1 m)%Z (m radix × pPred (vNum b))%Z f1 = m :>R)
 Fbounded b f1.
split; auto.
1%Z; repeat split; auto with zarith.
apply Zle_trans with (radix × 1)%Z; auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
unfold pPred in |- *; apply Zle_Zpred;
 apply (vNumbMoreThanOne radix) with (precision := precision);
 auto with zarith.
Qed.

Theorem Goal4 :
  (x0 y0 : float)
   (Post3 : ex
              (fun m : Z
               (Zpower_nat radix precision m)%Z
               (m radix × pPred (vNum b))%Z x0 = m :>R)
            Fbounded b x0)
   (Pre4 : ex
             (fun m : Z ⇒ (1 m)%Z (m radix)%Z y0 = m :>R)
           Fbounded b y0) (Test2 : feq (fminus (fplus x0 y0) x0) y0 = false),
 Zabs_nat (radix - Int_part (fplus y0 f1)) < Zabs_nat (radix - Int_part y0)
 ex (fun m : Z ⇒ (1 m)%Z (m radix)%Z fplus y0 f1 = m :>R)
 Fbounded b (fplus y0 f1).
intros x0 y0 Post3 Pre4 Test2.
elim Post3; intros H'0 H'1; elim H'0; intros vx0 E; elim E; intros Hv1 H'3;
 elim H'3; intros Hv2 Hv3; clear H'3 E H'0 Post3.
elim Pre4; intros H' Hv1'; elim H'; intros vy0 E; elim E; intros Hv2' H'3;
 elim H'3; intros Hv3' Hv4'; clear H'3 E H' Pre4.
cut
 (ex
    (fun m : Z ⇒ (1 m)%Z (m radix)%Z fplus y0 f1 = m :>R));
 [ intros Ex1 | idtac ].
split; [ idtac | split ]; auto.
elim Ex1; intros vb1 E; elim E; intros Hv1'' H'0; elim H'0;
 intros Hv2'' Hv3''; clear H'0 E Ex1.
rewrite Hv4'; rewrite Hv3''; repeat rewrite Int_part_IZR.
apply Zabs.Zabs_nat_lt; split; auto with zarith.
cut (vy0 < vb1)%Z; auto with zarith.
apply Zlt_Rlt; rewrite <- Hv4'; rewrite <- Hv3''.
apply (BLoop4 y0 Hv1' vy0); auto.
case (Zle_or_lt radix vy0); auto; intros le1.
absurd (fminus (fplus x0 y0) x0 = y0 :>R); auto.
generalize (Feq_bool_correct_f radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
apply BLoop3 with (m := vx0); auto with real arith.
rewrite Hv4'; apply Rle_antisym; auto with real arith.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (y0 + f1)%R);
 auto.
case (Zle_lt_or_eq _ _ Hv3'); intros le1.
case
 (ZroundZ b radix precision)
  with (P := P) (z := Zsucc vy0) (p := fplus y0 f1);
 auto.
apply Cp with (1 := fplusCorrect _ _ Hv1' f1Bounded); auto.
rewrite Hv4'.
rewrite f1Correct; simpl in |- *; unfold Zsucc in |- *; rewrite plus_IZR;
 simpl in |- *; ring.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (y0 + f1)%R);
 auto.
intros x H'; x; repeat split; auto.
apply Zle_Rle.
rewrite <- H'; rewrite <- f1Correct; auto.
apply (RleBoundRoundl b radix precision) with (P := P) (r := (y0 + f1)%R);
 auto.
fold FtoRradix in |- *; rewrite Hv4'; rewrite f1Correct; auto.
rewrite <- plus_IZR; auto with real zarith.
apply Zle_Rle.
rewrite <- H'.
replace (IZR radix) with (FtoRradix (Float 1%nat 1%nat)).
apply (RleBoundRoundr b radix precision) with (P := P) (r := (y0 + f1)%R);
 auto.
repeat split; simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
 auto with zarith.
case (dExp b); auto with zarith.
rewrite Hv4'; rewrite f1Correct; unfold FtoR in |- *; simpl in |- *;
 rewrite Rmult_1_l; rewrite Rmult_1_r.
replace 1%R with (IZR 1); auto with real zarith; rewrite <- plus_IZR;
 apply Rle_IZR; auto with zarith.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_l;
 rewrite Rmult_1_r; auto.
absurd (fminus (fplus x0 y0) x0 = y0 :>R).
generalize (Feq_bool_correct_f radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
apply BLoop3 with (m := vx0); auto with real arith.
rewrite Hv4'; rewrite le1; auto with real.
Qed.

Theorem Goal5_6b :
 ex (fun m : Z ⇒ (1 m)%Z (m radix)%Z f1 = m :>R)
 Fbounded b f1.
split; [ 1%Z; split; [ idtac | split ] | idtac ]; auto with zarith.
Qed.

Theorem Goal5b :
  (x0 y0 : float)
   (Post3 : ex
              (fun m : Z
               (Zpower_nat radix precision m)%Z
               (m radix × pPred (vNum b))%Z x0 = m :>R)
            Fbounded b x0)
   (Pre4 : ex
             (fun m : Z ⇒ (1 m)%Z (m radix)%Z y0 = m :>R)
           Fbounded b y0) (Test2 : feq (fminus (fplus x0 y0) x0) y0 = true),
 Fbounded b y0 y0 = radix :>R.
intros x0 y0 Post3 Pre4 Test2.
elim Post3; intros H' Hv1; elim H'; intros va0 E; elim E; intros Hv3 H'4;
 elim H'4; intros Hv4 Hv5; clear H'4 E H' Post3.
elim Pre4; intros H' Hv1'; elim H'; intros vb0 E; elim E; intros Hv2' H'2;
 elim H'2; intros Hv3' Hv4'; clear H'2 E H' Pre4.
rewrite Hv4'.
case (Zle_lt_or_eq _ _ Hv3'); intros le1.
absurd (fminus (fplus x0 y0) x0 = y0 :>R).
apply BLoop2 with (n := vb0) (m := va0); auto.
generalize (Feq_bool_correct_t radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
rewrite le1; auto.
Qed.

Theorem Goal6 :
  (x0 y0 : float)
   (Post2 : ex
              (fun m : Z
               (Zpower_nat radix precision m)%Z
               (m radix × pPred (vNum b))%Z x0 = m :>R)
            Fbounded b x0)
   (Post1 : (ex
               (fun m : Z
                (1 m)%Z (m radix)%Z y0 = m :>R)
             Fbounded b y0) feq (fminus (fplus x0 y0) x0) y0 = true),
 y0 = radix :>R.
intros x0 y0 Post2 Post1.
elim Post1; intros H' Hv1; elim H'; intros H'1 Hv2; elim H'1; intros vy0 E;
 elim E; intros Hv3 H'4; elim H'4; intros Hv4 Hv5;
 clear H'4 E H'1 H' Post1.
elim Post2; intros H' Hv1'; elim H'; intros vx0 E; elim E; intros Hv2' H'2;
 elim H'2; intros Hv3' Hv4'; clear H'2 E H' Post2.
rewrite Hv5.
case (Zle_lt_or_eq _ _ Hv4); intros le1.
absurd (fminus (fplus x0 y0) x0 = y0 :>R).
apply BLoop2 with (m := vx0) (n := vy0); auto.
generalize (Feq_bool_correct_t radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
rewrite le1; auto.
Qed.


Theorem Goal7b :
  (y0 x2 : float) (n0 : nat) (Post2 : Fbounded b y0 y0 = radix :>R)
   (Pre6 : ex
             (fun m : Z
              ((1 m)%Z (m radix × pPred (vNum b))%Z x2 = m :>R)
              m = Zpower_nat radix n0) Fbounded b x2)
   (Test3 : feq (fminus (fplus x2 f1) x2) f1 = true),
 Zabs_nat (radix × pPred (vNum b) - Int_part (fmult x2 y0)) <
 Zabs_nat (radix × pPred (vNum b) - Int_part x2)
 ex
   (fun m : Z
    ((1 m)%Z (m radix × pPred (vNum b))%Z fmult x2 y0 = m :>R)
    m = Zpower_nat radix (S n0)) Fbounded b (fmult x2 y0).
intros y0 x2 n0 Post2 Pre6 Test3.
Casec Pre6; intros Pre6; Casec Pre6; intros va0 Pre6; Casec Pre6;
 intros Pre6 Hv1'; Casec Pre6; intros Hv1 Pre6; Casec Pre6;
 intros Hv2 Hv3 Fb1.
Casec Post2; intros Fby0 Post2.
cut
 (ex
    (fun m : Z
     ((1 m)%Z
      (m radix × pPred (vNum b))%Z FtoRradix (fmult x2 y0) = m :>R)
     m = Zpower_nat radix (S n0) :>Z)).
intros H'; split; [ idtac | split; [ try assumption | idtac ] ].
Casec H'; intros va1 Pre6; Casec Pre6; intros Pre6 H'1; Casec Pre6;
 intros Hv1'' Pre6; Casec Pre6; intros Hv2' Hv3'.
rewrite Hv3; rewrite Hv3'; repeat rewrite Int_part_IZR.
apply Zabs.Zabs_nat_lt; split; auto with zarith.
rewrite H'1; rewrite Hv1'.
unfold Zminus in |- *; auto with zarith.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (x2 × y0)%R);
 auto.
case
 (ZroundZ b radix precision)
  with (P := P) (z := (va0 × radix)%Z) (p := fmult x2 y0);
 auto.
apply Cp with (1 := fmultCorrect _ _ Fb1 Fby0); auto.
rewrite Hv3; rewrite Post2; rewrite Rmult_IZR; auto with real arith.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (x2 × y0)%R);
 auto.
intros x H'; x; repeat split; auto.
apply Zle_Rle; rewrite <- f1Correct; rewrite <- H'.
apply (RleBoundRoundl b radix precision) with (P := P) (r := (x2 × y0)%R);
 auto.
rewrite Hv3; rewrite Post2; fold FtoRradix in |- *; rewrite f1Correct.
rewrite <- Rmult_IZR.
apply Rle_IZR; apply Zle_trans with (1 × radix)%Z; auto with zarith.
apply Zle_Rle.
cut (Float (pPred (vNum b)) 1%nat = (radix × pPred (vNum b))%Z :>R);
 [ intros Eq1 | idtac ].
rewrite <- Eq1; rewrite <- H'.
apply (RleBoundRoundr b radix precision) with (P := P) (r := (x2 × y0)%R);
 auto.
repeat split; simpl in |- *; auto with zarith.
rewrite Zabs_eq; unfold pPred in |- *; auto with zarith.
case (dExp b); auto with zarith.
fold FtoRradix in |- *; rewrite Eq1.
rewrite Rmult_IZR;
 replace (radix × pPred (vNum b))%R with (pPred (vNum b) × radix)%R;
 auto with real arith.
apply Rmult_le_compat; auto with real arith.
rewrite Hv3; replace 0%R with (IZR 0); auto with real zarith.
rewrite Post2; replace 0%R with (IZR 0); auto with real zarith.
rewrite Hv3.
case (Zle_or_lt va0 (pPred (vNum b))); auto with real zarith.
intros H'0; absurd (fminus (fplus x2 f1) x2 = f1 :>R).
apply Loop3 with (n := va0); auto.
rewrite (Zsucc_pred (Zpos (vNum b))); auto with zarith.
generalize (Feq_bool_correct_t radix); unfold Feq in |- *; intros Eq2;
 apply Eq2; auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_IZR; ring.
apply IZR_inv.
rewrite <- H'.
cut (Zpower_nat radix (S n0) = Float (Fnum x2) (Zsucc (Fexp x2)) :>R);
 [ intros Eq1; rewrite Eq1 | idtac ].
apply sym_eq;
 apply (RoundedModeProjectorIdemEq b radix precision) with (P := P);
 auto.
repeat split; simpl in |- *; auto with arith zarith.
case Fb1; simpl in |- *; auto.
apply Zle_trans with (Fexp x2); auto with zarith.
case Fb1; simpl in |- *; auto.
apply Cp with (1 := fmultCorrect _ _ Fb1 Fby0); auto.
unfold FtoR in |- *; simpl in |- ×.
rewrite powerRZ_Zs; auto with real zarith.
replace (Fnum x2 × (radix × powerRZ radix (Fexp x2)))%R with
 (Fnum x2 × powerRZ radix (Fexp x2) × radix)%R; auto with real zarith.
ring.
apply RoundedModeBounded with (radix := radix) (P := P) (r := (x2 × y0)%R);
 auto.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (S n0) with (n0+1)%nat; auto with zarith.
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1.
rewrite <- Hv1'.
cut (IZR (va0×radix) = (radix × (Fnum x2 × powerRZ radix (Fexp x2)))%R :>R);
 [ intros Eq2; rewrite Eq2 | idtac ].
rewrite powerRZ_Zs; auto with real zarith; ring.
fold FtoRradix in |- ×.
rewrite Rmult_IZR.
rewrite <- Hv3; auto.
unfold FtoRradix, FtoR; ring.
Qed.

Theorem Goal8b :
 ex
   (fun m : Z
    ((1 m)%Z (m radix × pPred (vNum b))%Z f1 = m :>R)
    m = Zpower_nat radix 0) Fbounded b f1.
split; auto.
1%Z; repeat split; auto.
replace 1%Z with (1 × 1)%Z; auto with zarith.
apply Zle_trans with (radix × 1)%Z; auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
unfold pPred in |- *; apply Zle_Zpred.
apply vNumbMoreThanOne with (radix := radix) (precision := precision);
 auto with arith.
Qed.

Theorem Goal9b :
  (y0 x2 : float) (n0 : nat) (Post2 : Fbounded b y0 y0 = radix :>R)
   (Post1 : (ex
               (fun m : Z
                ((1 m)%Z (m radix × pPred (vNum b))%Z x2 = m :>R)
                m = Zpower_nat radix n0) Fbounded b x2)
            feq (fminus (fplus x2 f1) x2) f1 = false),
 y0 = radix :>R n0 = precision.
intros y0 x2 n0 Post2 Post1.
Casec Post2; intros Fby0 Post2.
split; [ try assumption | idtac ].
apply Zpower_nat_anti_eq with (n := radix); auto.
Casec Post1; intros Post1 H'0; Casec Post1; intros Post1 H'2; Casec Post1;
 intros m E; Casec E; intros H'3 H'4; rewrite <- H'4;
 Casec H'3; intros H' H'1; Casec H'1; intros H'3 H'5.
case (Zle_or_lt m (pPred (vNum b))).
intros H'1.
absurd (feq (fminus (fplus x2 f1) x2) f1 = true :>bool).
rewrite H'0; red in |- *; intros; discriminate.
unfold feq in |- *; apply Feq_bool_correct_r; auto.
unfold Feq in |- *; apply (Loop2 x2) with (n := m); auto with zarith.
intros H'1; apply Zle_antisym.
rewrite H'4; apply Zpower_nat_monotone_le; auto with zarith.
cut (n0 < S precision); auto with arith.
apply (Zpower_nat_anti_monotone_lt radix); auto.
rewrite <- H'4; auto.
apply Zle_lt_trans with (1 := H'3).
replace (S precision) with (1+precision); auto with zarith.
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1.
rewrite <- pGivesBound; unfold pPred in |- *; apply Zmult_gt_0_lt_compat_l;
 auto with zarith.
rewrite <- pGivesBound; rewrite (Zsucc_pred (Zpos (vNum b)));
 auto with zarith.
Qed.
End prog.