Library Float.Others.FminOp

Require Export AllFloat.
Require Export Paux.

Theorem oZ1_oZ : o, oZ1 o = Z_of_nat (oZ o).
intros o; case o; simpl in |- *; auto.
intros x; apply sym_equal; apply inject_nat_convert; auto.
Qed.
Opaque Pdiv.
Opaque PdivBound.

Definition FindMin (bound base a : positive)
  (dexp exp : Z) :=
  match PdivBound bound a base with
  | (q, r, n)
      match (exp + Z_of_nat n)%Z with
      | exp'
          match (dexp - exp')%Z with
          | Zpos e
              match q with
              | Some q1
                  match Pdiv q1 (positive_exp base e) with
                  | (q', r')
                      (Float (oZ1 q') dexp,
                      Fplus (Zpos base) (Float (oZ1 r') exp')
                        (Float (oZ1 r) exp))
                  end
              | None(Float 0 dexp, Float (oZ1 r) exp)
              end
          | _(Float (oZ1 q) exp', Float (oZ1 r) exp)
          end
      end
  end.
Section FminOp.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Coercion Local FtoRradix := FtoR radix.
Variable b : Fbound.
Variable precision : nat.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Let dExp := (- dExp b)%Z.

Theorem Zpower_nat_exp :
  (a : positive) (n : nat),
 exp (nat_of_P a) n = Zpower_nat (Zpos a) n :>Z.
intros a n; elim n; simpl in |- *; auto.
intros n0 H; rewrite inj_mult; rewrite H.
replace (S n0) with (1 + n0); [ rewrite Zpower_nat_is_exp | idtac ]; auto.
rewrite Zpower_nat_1; auto.
rewrite (inject_nat_convert (Zpos a)); auto.
Qed.

Definition Z2pos x :=
  match x with
  | Z0 ⇒ 1%positive
  | Zpos pp
  | Zneg pp
  end.

Theorem Z2pos_correct :
  z : Z, (0 < z)%ZZpos (Z2pos z) = z.
intros z; case z; simpl in |- *; auto; unfold Zlt in |- *; simpl in |- *;
 intros; discriminate.
Qed.

Theorem FminOp_correct1 :
  a e,
 Float (Zpos a) e =
 (fst (FindMin (vNum b) (Z2pos radix) a dExp e) +
  snd (FindMin (vNum b) (Z2pos radix) a dExp e))%R :>R.
cut (1 < nat_of_P (Z2pos radix));
 [ intros Z2
 | apply lt_Zlt_inv; simpl in |- *; idtac;
    try
     rewrite (inject_nat_convert (Zpos (Z2pos radix)) (Z2pos radix));
    auto; rewrite Z2pos_correct; auto with zarith ].
intros a e; unfold FindMin in |- ×.
generalize (PdivBound_correct1 (vNum b) a (Z2pos radix));
 case (PdivBound (vNum b) a (Z2pos radix)); simpl in |- ×.
intros p; case p; simpl in |- ×.
intros o1 o2 n H1.
CaseEq (dExp - (e + n))%Z; simpl in |- ×.
intros H; unfold FtoRradix in |- *;
 rewrite <- (FshiftCorrect radix radixMoreThanOne n (Float (oZ1 o1) (e + n)));
 simpl in |- *; auto.
unfold Fshift in |- *; simpl in |- *; auto.
replace (e + n - n)%Z with e; [ idtac | auto with zarith ].
unfold FtoR in |- *; simpl in |- *; auto with arith.
rewrite <- Rmult_plus_distr_r; rewrite H1; auto.
rewrite plus_INR; rewrite INR_IZR_INZ; rewrite inj_mult.
rewrite Zpower_nat_exp; simpl in |- ×.
rewrite Z2pos_correct; auto with zarith.
repeat rewrite oZ1_oZ; auto.
repeat rewrite <- INR_IZR_INZ; auto.
intros p0 H; generalize H1; clear H1; case o1.
intros x H1; generalize (Pdiv_correct x (positive_exp (Z2pos radix) p0));
 case (Pdiv x (positive_exp (Z2pos radix) p0)).
intros q' r'; simpl in |- ×.
intros (H2, H3).
unfold FtoRradix in |- *;
 rewrite <-
  (FshiftCorrect radix radixMoreThanOne (Zabs_nat (n + Zpos p0))
     (Float (oZ1 q') dExp)); simpl in |- *; auto.
rewrite Z2pos_correct; auto with zarith.
rewrite Fplus_correct; auto with zarith.
rewrite <- (FshiftCorrect radix radixMoreThanOne n (Float (oZ1 r') (e + n)));
 simpl in |- *; auto.
unfold Fshift in |- *; simpl in |- *; auto.
replace (dExp - Zabs_nat (n + Zpos p0))%Z with e.
replace (e + n - n)%Z with e.
unfold FtoR in |- *; simpl in |- *; auto.
repeat rewrite <- Rmult_plus_distr_r; rewrite H1; simpl in |- *; auto.
rewrite H2.
rewrite positive_exp_correct.
repeat rewrite oZ1_oZ.
rewrite mult_plus_distr_r.
rewrite mult_assoc_reverse.
rewrite <- expPlus.
repeat rewrite plus_INR.
repeat (rewrite INR_IZR_INZ; rewrite inj_mult).
rewrite plus_comm.
repeat rewrite Zpower_nat_exp; simpl in |- ×.
repeat rewrite Z2pos_correct; auto with zarith.
replace (Zabs_nat (n + Zpos p0)) with (n + nat_of_P p0); auto.
repeat rewrite <- INR_IZR_INZ; ring.
rewrite <- (inject_nat_convert (Zpos p0) p0); auto.
rewrite <- inj_plus.
apply sym_equal; apply absolu_INR.
ring.
rewrite <- (inject_nat_convert (Zpos p0) p0); auto.
rewrite <- inj_plus.
rewrite absolu_INR.
rewrite inj_plus.
rewrite (inject_nat_convert (Zpos p0) p0); auto.
rewrite <- H; ring.
auto with arith.
auto with arith.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
intros H1; rewrite H1.
rewrite oZ1_oZ; repeat rewrite <- INR_IZR_INZ; ring.
apply lt_Zlt_inv; simpl in |- *; idtac;
 try rewrite (inject_nat_convert (Zpos (Z2pos radix)) (Z2pos radix));
 auto; rewrite Z2pos_correct; auto with zarith.
intros p0 H; unfold FtoRradix in |- *;
 rewrite <- (FshiftCorrect radix radixMoreThanOne n (Float (oZ1 o1) (e + n)));
 simpl in |- *; auto.
unfold Fshift in |- *; simpl in |- *; auto.
replace (e + n - n)%Z with e; [ idtac | auto with zarith ].
unfold FtoR in |- *; simpl in |- *; auto with arith.
rewrite <- Rmult_plus_distr_r; rewrite H1; auto.
rewrite plus_INR; rewrite INR_IZR_INZ; rewrite inj_mult.
rewrite Zpower_nat_exp; simpl in |- ×.
repeat rewrite Z2pos_correct; auto with zarith.
repeat rewrite oZ1_oZ; auto.
repeat rewrite <- INR_IZR_INZ; auto.
Qed.

Theorem FminOp_correct2 :
  a e, (0 snd (FindMin (vNum b) (Z2pos radix) a dExp e))%R.
intros a e; unfold FindMin in |- *; case (PdivBound (vNum b) a (Z2pos radix)).
intros p; case p; simpl in |- ×.
intros o1 o2 n; case (dExp - (e + n))%Z; simpl in |- *; auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto.
replace 0%R with (0 × powerRZ radix e)%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real zarith.
case o2; simpl in |- *; auto with real.
intros p0; case o1; simpl in |- ×.
intros o1'; case (Pdiv o1' (positive_exp (Z2pos radix) p0)); simpl in |- *;
 auto.
intros o o0.
repeat rewrite Z2pos_correct; auto with zarith.
unfold FtoRradix in |- *; rewrite Fplus_correct; auto with arith.
replace 0%R with (0 + 0)%R; [ idtac | ring ].
apply Rplus_le_compat; unfold FtoR in |- *; simpl in |- *; auto with real.
replace 0%R with (0 × powerRZ radix (e + n))%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
case o0; simpl in |- *; auto with real.
replace 0%R with (0 × powerRZ radix e)%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
case o2; simpl in |- *; auto with real.
unfold FtoRradix, FtoR in |- *; simpl in |- *;
 replace 0%R with (0 × powerRZ radix e)%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
case o2; simpl in |- *; auto with real.
intros o; unfold FtoRradix, FtoR in |- *; simpl in |- *;
 replace 0%R with (0 × powerRZ radix e)%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
case o2; simpl in |- *; auto with real.
Qed.

Theorem FminOp_correct3 :
  a e, Fbounded b (fst (FindMin (vNum b) (Z2pos radix) a dExp e)).
cut (1 < nat_of_P (Z2pos radix));
 [ intros Z2
 | apply lt_Zlt_inv; simpl in |- *; idtac;
    try
     rewrite (inject_nat_convert (Zpos (Z2pos radix)) (Z2pos radix));
    auto; rewrite Z2pos_correct; auto with zarith ].
intros a e; unfold FindMin in |- *;
 generalize (PdivBound_correct2 (vNum b) a (Z2pos radix));
 case (PdivBound (vNum b) a (Z2pos radix)).
intros p; case p; simpl in |- ×.
intros o1 o2 n H1.
CaseEq (dExp - (e + n))%Z; simpl in |- ×.
intros H2; repeat (split; simpl in |- *; auto).
rewrite Zabs_eq;
 [ idtac
 | case o1; simpl in |- *; intros; red in |- *; simpl in |- *; auto;
    red in |- *; intros; discriminate ].
rewrite oZ1_oZ;
 rewrite <- (inject_nat_convert (Zpos (vNum b)) (vNum b));
 auto with zarith.
fold dExp in |- *; auto with zarith.
intros p0 H; generalize H1; clear H1; case o1; simpl in |- ×.
intros x H1; generalize (Pdiv_correct x (positive_exp (Z2pos radix) p0));
 case (Pdiv x (positive_exp (Z2pos radix) p0)); simpl in |- ×.
intros o o0 (H2, H3).
repeat (split; simpl in |- *; auto).
rewrite oZ1_oZ;
 rewrite <- (inject_nat_convert (Zpos (vNum b)) (vNum b));
 auto with zarith.
rewrite Zabs_eq; [ idtac | case o; simpl in |- *; auto with zarith ].
apply inj_lt.
apply le_lt_trans with (nat_of_P x); auto.
replace (oZ o) with (oZ o × 1 + 0); [ rewrite H2 | ring ].
apply plus_le_compat; auto with arith.
fold dExp in |- *; auto with zarith.
intros H1; repeat (split; simpl in |- *; auto with zarith).
intros p0 H; rewrite oZ1_oZ; repeat (split; simpl in |- *; auto).
rewrite Zabs_eq; [ idtac | case o1; simpl in |- *; auto with zarith ].
rewrite <- (inject_nat_convert (Zpos (vNum b)) (vNum b));
 auto with zarith.
fold dExp in |- *; auto with zarith.
replace dExp with (e + n + (dExp - (e + n)))%Z; auto with zarith.
pattern (e + n)%Z at 3 in |- *; replace (e + n)%Z with (e + n + 0)%Z.
apply Zplus_le_compat; try rewrite H; auto with zarith.
auto with zarith.
Qed.

Theorem FminOp_correct4 :
  a e,
 snd (FindMin (vNum b) (Z2pos radix) a dExp e) = 0%R :>R
 Fcanonic radix b (fst (FindMin (vNum b) (Z2pos radix) a dExp e)).
intros a e; generalize (FminOp_correct3 a e); unfold FindMin in |- *;
 generalize (PdivBound_correct2 (vNum b) a (Z2pos radix));
 generalize (PdivBound_correct3 (vNum b) a (Z2pos radix));
 generalize (PdivBound_correct4 (vNum b) a (Z2pos radix));
 case (PdivBound (vNum b) a (Z2pos radix)).
cut (1 < nat_of_P (Z2pos radix));
 [ intros Z2
 | apply lt_Zlt_inv; simpl in |- *; idtac;
    try
     rewrite (inject_nat_convert (Zpos (Z2pos radix)) (Z2pos radix));
    auto; rewrite Z2pos_correct; auto with zarith ].
intros p; case p; simpl in |- ×.
intros o1 o2 n H1 H2 H3.
CaseEq (dExp - (e + n))%Z; simpl in |- ×.
intros H4 Fb; right.
cut (Fdigit radix (Float (oZ1 o1) (e + n)) precision);
 [ intros Le1 | idtac ].
case (le_lt_or_eq _ _ Le1); intros Le2.
right; repeat (split; simpl in |- *; auto).
fold dExp in |- *; auto with zarith.
case (Z_eq_dec (oZ1 o1) 0); intros Z3.
replace (radix × oZ1 o1)%Z with 0%Z; auto with zarith; rewrite Z3; ring.
rewrite pGivesBound; rewrite <- (Zabs_eq (Zpower_nat radix precision));
 auto with zarith.
apply (digit_anti_monotone_lt radix); auto.
replace (radix × oZ1 o1)%Z with (oZ1 o1 × Zpower_nat radix 1)%Z;
 [ idtac | rewrite Zpower_nat_1; ring ].
replace (Zpower_nat radix precision) with (1 × Zpower_nat radix precision)%Z;
 [ idtac | ring ].
repeat rewrite digitAdd; auto with zarith.
rewrite digit1; rewrite (fun xplus_comm x 1); simpl in |- *;
 auto with arith.
left; repeat (split; simpl in |- *; auto).
rewrite Zabs_Zmult; rewrite (Zabs_eq radix); auto with zarith.
rewrite (PosNormMin radix b precision); auto with arith;
 unfold nNormMin in |- ×.
apply Zle_Zmult_comp_l; auto with zarith.
rewrite <- Le2; unfold Fdigit in |- *; simpl in |- *; apply digitLess.
Contradict Le2; rewrite Le2; unfold Fdigit in |- *; simpl in |- *;
 auto with zarith.
apply pGivesDigit with (b := b); auto with arith.
intros p0 H; generalize H1 H2 H3; clear H1 H2 H3; case o1; simpl in |- ×.
intros x H1 H2 H3;
 generalize (Pdiv_correct x (positive_exp (Z2pos radix) p0));
 case (Pdiv x (positive_exp (Z2pos radix) p0)); simpl in |- ×.
intros o o0 H0 Fb; right.
cut (Fdigit radix (Float (oZ1 o) dExp) precision); [ intros Le1 | idtac ].
case (le_lt_or_eq _ _ Le1); intros Le2.
right; repeat (split; simpl in |- *; auto).
case (Z_eq_dec (oZ1 o) 0); intros Z3.
replace (radix × oZ1 o)%Z with 0%Z; auto with zarith; rewrite Z3; ring.
rewrite pGivesBound; rewrite <- (Zabs_eq (Zpower_nat radix precision));
 auto with zarith.
apply (digit_anti_monotone_lt radix); auto.
replace (radix × oZ1 o)%Z with (oZ1 o × Zpower_nat radix 1)%Z;
 [ idtac | rewrite Zpower_nat_1; ring ].
replace (Zpower_nat radix precision) with (1 × Zpower_nat radix precision)%Z;
 [ idtac | ring ].
repeat rewrite digitAdd; auto with zarith.
rewrite digit1; rewrite (fun xplus_comm x 1); simpl in |- *;
 auto with arith.
left; repeat (split; simpl in |- *; auto).
rewrite Zabs_Zmult; rewrite (Zabs_eq radix); auto with zarith.
rewrite (PosNormMin radix b precision); auto with arith;
 unfold nNormMin in |- ×.
apply Zle_Zmult_comp_l; auto with zarith.
rewrite <- Le2; unfold Fdigit in |- *; simpl in |- *; apply digitLess.
Contradict Le2; rewrite Le2; unfold Fdigit in |- *; simpl in |- *;
 auto with zarith.
apply pGivesDigit with (b := b); auto with arith.
intros H1 H2 H3; right; right;
 repeat (split; simpl in |- *; auto with zarith).
replace (radix × 0)%Z with 0%Z; [ auto with zarith | ring ].
intros p0 H Fb.
case (le_or_lt (nat_of_P (vNum b)) (nat_of_P a)); intros H4.
right; left.
repeat (split; simpl in |- *; auto).
rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith.
cut
 (nat_of_P (vNum b) (nat_of_P (Z2pos radix) × oZ o1)%nat)%Z;
 auto with zarith arith.
rewrite inj_mult;
 repeat rewrite (fun xinject_nat_convert (Zpos x) x);
 auto.
rewrite Z2pos_correct; auto; rewrite oZ1_oZ; auto.
apply inj_le; apply (H1 (Zabs_nat (nNormMin radix precision))); auto.
apply inject_nat_eq; rewrite inj_mult;
 repeat rewrite (fun xinject_nat_convert (Zpos x) x);
 auto.
rewrite Z2pos_correct; auto; rewrite inj_abs; auto with zarith.
apply PosNormMin; auto with zarith.
unfold nNormMin in |- *; auto with zarith.
case o1; simpl in |- *; auto; intros; red in |- *; intros; discriminate.
left; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring_simplify.
generalize (H2 H4); intros tmp; injection tmp.
intros H'1 H'2 H'3; rewrite H'2; simpl in |- *; auto.
ring.
Qed.

Theorem FminOp_correct5 :
  a e,
 snd (FindMin (vNum b) (Z2pos radix) a dExp e) = 0%R :>R
 (snd (FindMin (vNum b) (Z2pos radix) a dExp e) <
  Fulp b radix precision (fst (FindMin (vNum b) (Z2pos radix) a dExp e)))%R.
cut (1 < nat_of_P (Z2pos radix));
 [ intros Z2
 | apply lt_Zlt_inv; simpl in |- *; idtac;
    try
     rewrite (inject_nat_convert (Zpos (Z2pos radix)) (Z2pos radix));
    auto; rewrite Z2pos_correct; auto with zarith ].
intros a e; case (FminOp_correct4 a e); auto; intros C1.
right; unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
unfold FindMin in |- *;
 generalize (PdivBound_correct (vNum b) a (Z2pos radix));
 case (PdivBound (vNum b) a (Z2pos radix)); simpl in |- ×.
intros p; case p; simpl in |- ×.
intros o1 o2 n H1.
CaseEq (dExp - (e + n))%Z; simpl in |- ×.
intros H2; case H1.
apply lt_Zlt_inv; rewrite (fun xinject_nat_convert (Zpos x) x);
 auto; try rewrite Z2pos_correct; auto with zarith.
intros tmp ((tmp1, H3), tmp2); rewrite oZ1_oZ; unfold FtoRradix, FtoR in |- *;
 simpl in |- ×.
rewrite powerRZ_add; auto with real zarith.
rewrite (fun x yRmult_comm (powerRZ x y)).
apply Rlt_monotony_exp; auto with zarith.
rewrite <- Zpower_nat_Z_powerRZ; auto with zarith.
rewrite <- (Z2pos_correct radix); try rewrite <- Zpower_nat_exp;
 auto with real zarith arith.
intros p0 H; generalize H1; clear H1; case o1.
intros x H1; generalize (Pdiv_correct x (positive_exp (Z2pos radix) p0));
 case (Pdiv x (positive_exp (Z2pos radix) p0)).
intros q' r'; simpl in |- ×.
intros (H2, H3).
unfold Fplus in |- *; simpl in |- ×.
replace (Zmin (e + n) e) with e.
replace (Zabs_nat (e + n - e)) with n.
replace (Zabs_nat (e - e)) with 0.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
repeat rewrite oZ1_oZ.
rewrite Z2pos_correct; auto with zarith.
replace dExp with (Zpos p0 + (e + n))%Z.
repeat (rewrite powerRZ_add; auto with real arith).
replace
 (powerRZ radix (Zpos p0) × (powerRZ radix e × powerRZ radix n))%R
 with (powerRZ radix (Zpos p0) × powerRZ radix n × powerRZ radix e)%R;
 [ idtac | ring ].
apply Rlt_monotony_exp; auto with arith.
replace (oZ o2 × Zpower_nat radix 0)%Z with (Z_of_nat (oZ o2)).
rewrite <- (inject_nat_convert (Zpos p0) p0); auto.
repeat rewrite <- Zpower_nat_Z_powerRZ; auto with zarith.
replace radix with (Zpos (Z2pos radix)).
repeat rewrite <- Zpower_nat_exp; auto with zarith.
rewrite <- Rmult_IZR.
apply Rlt_IZR.
repeat rewrite <- inj_mult || rewrite <- inj_plus.
apply inj_lt.
apply
 lt_le_trans
  with
    (oZ r' × exp (nat_of_P (Z2pos radix)) n +
     exp (nat_of_P (Z2pos radix)) n).
case H1; auto with arith; intros tmp1 ((tmp2, H4), tmp3); auto with arith.
replace
 (oZ r' × exp (nat_of_P (Z2pos radix)) n +
  exp (nat_of_P (Z2pos radix)) n) with
 (S (oZ r') × exp (nat_of_P (Z2pos radix)) n).
apply lte_comp_mult; auto with arith.
rewrite positive_exp_correct in H3; auto with arith.
simpl in |- *; ring.
apply Z2pos_correct; auto.
rewrite Zpower_nat_O; idtac; simpl in |- *; auto with zarith.
auto with real zarith.
auto with real zarith.
rewrite <- H; ring.
replace (e - e)%Z with 0%Z; simpl in |- *; auto with zarith.
replace (e + n - e)%Z with (Z_of_nat n); simpl in |- *; auto with zarith.
apply sym_equal; apply absolu_INR.
apply sym_equal; apply Zmin_le2; auto with zarith.
intros H1; case H1; auto with arith; intros H2 ((H3, H4), H5).
rewrite oZ1_oZ; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto.
replace dExp with (Zpos p0 + (e + n))%Z.
repeat (rewrite powerRZ_add; auto with real arith).
replace
 (powerRZ radix (Zpos p0) × (powerRZ radix e × powerRZ radix n))%R
 with (powerRZ radix (Zpos p0) × powerRZ radix n × powerRZ radix e)%R;
 [ idtac | ring ].
apply Rlt_monotony_exp; auto with arith.
rewrite <- (inject_nat_convert (Zpos p0) p0); auto with arith.
replace radix with (Zpos (Z2pos radix)).
repeat rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith.
repeat rewrite <- Zpower_nat_exp; auto with zarith.
rewrite <- Rmult_IZR.
apply Rlt_IZR.
rewrite <- inj_mult.
apply inj_lt.
apply lt_le_trans with (1 × exp (nat_of_P (Z2pos radix)) n).
replace (1 × exp (nat_of_P (Z2pos radix)) n) with
 (exp (nat_of_P (Z2pos radix)) n); auto; ring.
apply lte_comp_mult; auto with arith.
elim (nat_of_P p0); simpl in |- *; auto with arith.
intros n0 H0; replace 1 with (1 × 1); auto with arith.
apply Z2pos_correct; auto with zarith.
auto with real zarith.
auto with real zarith.
rewrite <- H; ring.
intros p0 H; rewrite oZ1_oZ.
case H1; auto with arith; intros H2 ((H3, H4), H5).
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto.
repeat (rewrite powerRZ_add; auto with real arith).
replace (powerRZ radix e × powerRZ radix n)%R with
 (powerRZ radix n × powerRZ radix e)%R; [ idtac | ring ].
apply Rlt_monotony_exp; auto with arith.
replace radix with (Zpos (Z2pos radix)).
repeat rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith.
repeat rewrite <- Zpower_nat_exp; auto with real zarith arith.
apply Z2pos_correct; auto.
auto with real zarith arith.
Qed.

Theorem FminOp_correct6 :
  a e, (0 fst (FindMin (vNum b) (Z2pos radix) a dExp e))%R.
intros a e; unfold FindMin in |- *; case (PdivBound (vNum b) a (Z2pos radix)).
intros p; case p; simpl in |- ×.
intros o1 o2 n; case (dExp - (e + n))%Z; simpl in |- *; auto.
rewrite oZ1_oZ; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto.
replace 0%R with (0 × powerRZ radix (e + n))%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real zarith.
intros p0; case o1; simpl in |- ×.
intros o1'; case (Pdiv o1' (positive_exp (Z2pos radix) p0)); simpl in |- *;
 auto.
intros o o0; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace 0%R with (0 × powerRZ radix dExp)%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
rewrite oZ1_oZ; rewrite <- INR_IZR_INZ; auto with real arith.
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real arith.
intros o0; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace 0%R with (0 × powerRZ radix (e + n))%R; [ idtac | ring ].
apply Rmult_le_compat_r; auto with real arith.
rewrite oZ1_oZ; rewrite <- INR_IZR_INZ; auto with real arith.
Qed.

Theorem FSuccDiffPos :
  x : float,
 (0 x)%R
 Fminus radix (FSucc b radix precision x) x = Float 1%nat (Fexp x) :>R.
intros x H.
unfold FtoRradix in |- *; apply FSuccDiff1; auto with arith.
Contradict H; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H.
apply Rlt_not_le.
replace 0%R with (0 × powerRZ radix (Fexp x))%R; [ idtac | ring ].
apply Rlt_monotony_exp; auto with real arith.
generalize (nNormPos _ radixMoreThanOne precision);
 replace 0%R with (IZR (- 0%nat)); auto with real zarith arith.
Qed.

Theorem CanonicFulp :
  p : float,
 Fcanonic radix b pFulp b radix precision p = Float 1%nat (Fexp p).
intros p H; unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
Qed.

Theorem FSuccUlpPos :
  x : float,
 Fcanonic radix b x
 (0 x)%R
 Fminus radix (FSucc b radix precision x) x = Fulp b radix precision x :>R.
intros x H H0; rewrite CanonicFulp; auto.
apply FSuccDiffPos; auto.
Qed.

Theorem FNSuccUlpPos :
  x : float,
 Fcanonic radix b x
 (0 x)%R
 Fminus radix (FNSucc b radix precision x) x = Fulp b radix precision x :>R.
intros x H H0.
unfold FNSucc in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
apply FSuccUlpPos; auto.
Qed.

Theorem FminOp_correct7 :
  a e,
 isMin b radix (Float (Zpos a) e)
   (fst (FindMin (vNum b) (Z2pos radix) a dExp e)).
intros a e; apply MinBinade with (precision := precision); auto with arith.
apply FminOp_correct3.
rewrite FminOp_correct1; fold FtoRradix in |- *; auto with real.
apply
 Rle_trans
  with (FtoRradix (fst (FindMin (vNum b) (Z2pos radix) a dExp e)) + 0)%R;
 auto with real.
generalize (FminOp_correct2 a e); auto with real.
rewrite FminOp_correct1; fold FtoRradix in |- *; auto with real.
case (FminOp_correct5 a e); intros H1.
rewrite H1; auto with real float.
apply
 Rle_lt_trans
  with (FtoRradix (fst (FindMin (vNum b) (Z2pos radix) a dExp e)));
 auto with real.
unfold FtoRradix in |- *; apply FNSuccLt; auto with arith.
case (FminOp_correct4 a e); intros H2.
rewrite H2; auto with real float.
apply
 Rle_lt_trans
  with (FtoRradix (fst (FindMin (vNum b) (Z2pos radix) a dExp e)));
 auto with real.
unfold FtoRradix in |- *; apply FNSuccLt; auto with arith.
cut ( x y z, (y < z - x)%R → (x + y < z)%R);
 [ intros th1; apply th1 | auto with real ].
unfold FtoR in |- *; rewrite <- (Fminus_correct radix); auto with arith.
rewrite FNSuccUlpPos; auto with arith.
apply FminOp_correct6; auto with arith.
intros x y z H; replace z with (x + (z - x))%R; auto with real.
Qed.

Inductive rResult : Set :=
  | rExact : floatrResult
  | rRound : floatrResult.

Definition rFloat o := match o with
                       | rExact ee
                       | rRound ee
                       end.

Definition rFloor (f : float) :=
  match f with
  | Float Z0 erExact (Float 0 dExp)
  | Float (Zpos a) e
      match FindMin (vNum b) (Z2pos radix) a dExp e with
      | (r1, Float Z0 _)rExact r1
      | (r1, _)rRound r1
      end
  | Float (Zneg a) e
      match FindMin (vNum b) (Z2pos radix) a dExp e with
      | (r1, Float Z0 _)rExact (Fopp r1)
      | (r1, _)rRound (Fopp (FSucc b radix precision r1))
      end
  end.

Theorem NotR0NotZero : f : float, Fnum f 0%Zf 0%R :>R.
intros f H; Contradict H; auto with float arith.
unfold FtoRradix, FtoR in H; simpl in H.
case (Rmult_integral _ _ H); intros H1.
2: Contradict H1; auto with real zarith.
apply eq_IZR; simpl in |- *; auto.
Qed.

Theorem rFloor_correct :
  f : float,
 isMin b radix f (rFloat (rFloor f))
 match rFloor f with
 | rExact rr = f :>R
 | rRound rr f :>R Fcanonic radix b r
 end.
intros f; case f.
intros a e; case a; auto.
simpl in |- *; split.
replace (FtoRradix (Float 0 e)) with (FtoRradix (Float 0 dExp)).
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := isMin b radix);
 auto with float.
apply MinRoundedModeP with (precision := precision); auto with arith.
repeat (split; simpl in |- *; auto with arith zarith).
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
intros p; generalize (FminOp_correct1 p e); generalize (FminOp_correct4 p e);
 generalize (FminOp_correct7 p e); simpl in |- *;
 case (FindMin (vNum b) (Z2pos radix) p dExp e); simpl in |- *;
 auto.
intros f0 f1; case f1; simpl in |- *; auto.
intros a'; case a'; simpl in |- *; auto.
intros e' H1 H2 H3; split; auto; rewrite H3; unfold FtoRradix, FtoR in |- *;
 simpl in |- *; ring.
intros p' e' H1 H2 H3; split; auto.
split; auto.
Contradict H3; rewrite H3.
apply Rlt_not_eq; auto with real.
pattern (FtoRradix (Float (Zpos p) e)) at 1 in |- *;
 replace (FtoRradix (Float (Zpos p) e)) with
  (FtoRradix (Float (Zpos p) e) + 0)%R.
apply Rplus_lt_compat_l.
unfold FtoRradix, FtoR in |- *; simpl in |- *; apply Rmult_lt_0_compat;
 auto with real arith.
ring.
case H2; clear H2; auto; intros H2; Contradict H2.
apply NotR0NotZero; simpl in |- *; red in |- *; intros; discriminate.
intros p' e' H1 H2 H3; split; auto.
cut (Float (Zneg p') e' 0%R :>R); [ intros Rth1; split | idtac ].
Contradict H3; rewrite H3.
apply Rgt_not_eq; auto with real.
pattern (FtoRradix (Float (Zpos p) e)) at 1 in |- *;
 replace (FtoRradix (Float (Zpos p) e)) with
  (FtoRradix (Float (Zpos p) e) + 0)%R.
red in |- *; apply Rplus_lt_compat_l.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (- nat_of_P p' × powerRZ radix e')%R with
 (- (nat_of_P p' × powerRZ radix e'))%R; [ idtac | ring ].
replace 0%R with (-0)%R; [ idtac | ring ].
apply Ropp_lt_contravar; apply Rmult_lt_0_compat; auto with real arith.
ring.
case H2; auto; intros H4; Contradict Rth1; auto.
apply NotR0NotZero; simpl in |- *; red in |- *; intros; discriminate.
intros p;
 replace (FtoRradix (Float (Zneg p) e)) with
  (- FtoRradix (Float (Zpos p) e))%R.
2: rewrite <- (Fopp_correct radix); simpl in |- *; auto.
generalize (FminOp_correct1 p e); generalize (FminOp_correct3 p e);
 generalize (FminOp_correct4 p e); generalize (FminOp_correct5 p e);
 generalize (FminOp_correct6 p e); generalize (FminOp_correct7 p e);
 simpl in |- *; case (FindMin (vNum b) (Z2pos radix) p dExp e);
 simpl in |- *; auto.
intros f0 f1; case f1; simpl in |- *; auto.
intros a'; case a'; simpl in |- *; auto.
intros Fexp H H0 H1 H2 H3 H4; split; auto.
apply MaxOppMin; auto.
replace (FtoRradix (Float (Zpos p) e)) with (FtoRradix f0).
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := isMax b radix);
 auto with float.
apply MaxRoundedModeP with (precision := precision); auto with arith.
rewrite H4; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H4; rewrite (Fopp_correct radix); auto with arith;
 unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
intros p0 Fexp H H0 H1 H2 H3 H4;
 cut (FtoRradix (Float (Zpos p0) Fexp) 0%R :>R);
 [ intros Neq1; split | idtac ].
apply MaxOppMin; auto.
rewrite <-
 (FcanonicFnormalizeEq _ radixMoreThanOne b precision)
  with (p := f0); auto with zarith.
change
  (isMax b radix (FtoRradix (Float (Zpos p) e))
     (FNSucc b radix precision f0)) in |- ×.
apply MinMax; auto with arith.
rewrite H4.
Contradict Neq1.
replace 0%R with (FtoR radix f0 - f0)%R;
 [ rewrite <- Neq1 | fold FtoRradix in |- × ]; ring.
case H2; auto; intros H5; Contradict H5; apply NotR0NotZero; simpl in |- *;
 red in |- *; intros; discriminate.
case H2; clear H2; intros H2; [ Contradict Neq1; auto | idtac ].
rewrite H4.
split.
apply Rlt_not_eq; auto with real.
rewrite (Fopp_correct radix); auto with arith.
apply Ropp_lt_contravar.
cut ( x y z, (y < z - x)%R → (x + y < z)%R);
 [ intros Rt1; apply Rt1 | idtac ].
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with arith.
fold FtoRradix in |- *; rewrite (FSuccUlpPos f0); auto with arith.
case H1; auto; intros H5; Contradict H4; auto.
intros x y z H5; replace z with (x + (z - x))%R; auto with real; ring.
auto with float arith.
apply NotR0NotZero; simpl in |- *; red in |- *; intros; discriminate.
intros p0 Fexp H H0 H1 H2 H3 H4;
 cut (FtoRradix (Float (Zneg p0) Fexp) 0%R :>R);
 [ intros Neq1; split | idtac ].
apply MaxOppMin; auto.
rewrite <-
 (FcanonicFnormalizeEq _ radixMoreThanOne b precision)
  with (p := f0); auto with zarith.
change
  (isMax b radix (FtoRradix (Float (Zpos p) e))
     (FNSucc b radix precision f0)) in |- ×.
apply MinMax; auto with arith.
rewrite H4.
Contradict Neq1.
replace 0%R with (FtoR radix f0 - f0)%R;
 [ pattern (FtoR radix f0) at 1 in |- *; rewrite <- Neq1
 | fold FtoRradix in |- × ]; ring.
case H2; auto; intros H5; Contradict H5; apply NotR0NotZero; simpl in |- *;
 red in |- *; intros; discriminate.
case H2; clear H2; intros H2; [ Contradict Neq1; auto | idtac ].
rewrite H4.
split.
apply Rlt_not_eq; auto with real.
rewrite (Fopp_correct radix); auto with arith.
apply Ropp_lt_contravar.
cut ( x y z, (y < z - x)%R → (x + y < z)%R);
 [ intros Rt1; apply Rt1 | idtac ].
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with arith.
fold FtoRradix in |- *; rewrite (FSuccUlpPos f0); auto with arith.
case H1; auto; intros H5; Contradict H4; auto.
intros x y z H5; replace z with (x + (z - x))%R; auto with real; ring.
auto with float arith.
apply NotR0NotZero; simpl in |- *; red in |- *; intros; discriminate.
Qed.

Definition rCeil (f : float) :=
  match rFloor f with
  | rExact rrExact r
  | rRound rrRound (FSucc b radix precision r)
  end.

Theorem rCeil_correct :
  f : float,
 isMax b radix f (rFloat (rCeil f))
 match rCeil f with
 | rExact rr = f :>R
 | rRound rr f :>R Fcanonic radix b r
 end.
intros f; generalize (rFloor_correct f); unfold rCeil in |- *;
 case (rFloor f); simpl in |- ×.
intros r (H1, H2); split; auto.
rewrite <- H2.
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := isMax b radix);
 auto with float.
apply MaxRoundedModeP with (precision := precision); auto with arith.
case H1; auto.
intros r (H1, (H2, H3)); split; [ idtac | split ]; auto.
rewrite <- (FcanonicFnormalizeEq _ radixMoreThanOne b precision) with (p := r);
 auto with zarith.
change (isMax b radix (FtoRradix f) (FNSucc b radix precision r)) in |- ×.
apply MinMax; auto with arith.
Contradict H2; rewrite <- H2.
apply (MinUniqueP b radix) with (1 := H1).
rewrite <- H2.
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := isMin b radix).
apply MinRoundedModeP with (precision := precision); auto with arith.
apply FBoundedSuc; auto with arith.
apply FcanonicBound with radix; auto.
auto with float arith.
Qed.

Definition rToZero (f : float) :=
  match f with
  | Float Z0 erExact (Float 0 dExp)
  | Float (Zpos a) erFloor f
  | Float (Zneg a) erCeil f
  end.

Theorem rToZero_correct :
  f : float,
 ToZeroP b radix f (rFloat (rToZero f))
 match rToZero f with
 | rExact rr = f :>R
 | rRound rr f :>R Fcanonic radix b r
 end.
intros f; generalize (rFloor_correct f); generalize (rCeil_correct f);
 unfold rToZero in |- *; case f.
intros a e; case a; auto.
simpl in |- *; intros H H0; cut (Float 0 dExp = Float 0 e :>R);
 [ intros T1; split | idtac ]; auto.
rewrite <- T1; unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := ToZeroP b radix).
apply ToZeroRoundedModeP with (precision := precision); auto with arith.
repeat (split; simpl in |- *; auto with zarith).
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
intros p; case (rFloor (Float (Zpos p) e)).
intros f1 H1 (H2, H3); split; auto.
simpl in |- *; rewrite <- H3.
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := ToZeroP b radix).
apply ToZeroRoundedModeP with (precision := precision); auto with arith.
simpl in H2; case H2; auto.
intros f1 H1 (H2, H3); split; auto.
left; split; auto.
apply (LeFnumZERO radix); simpl in |- *; auto with zarith.
intros p; case (rCeil (Float (Zneg p) e)).
intros f1 (H2, H3) H1; split; auto.
simpl in |- *; rewrite <- H3.
unfold FtoRradix in |- *;
 apply RoundedModeProjectorIdem with (b := b) (P := ToZeroP b radix).
apply ToZeroRoundedModeP with (precision := precision); auto with arith.
simpl in H2; case H2; auto.
intros f1 (H2, H3) H1; split; auto.
right; split; auto.
apply (LeZEROFnum radix); simpl in |- *; auto with zarith.
Qed.

Definition ZevenP a :=
  match Fnum a with
  | Z0true
  | Zpos (xO _) ⇒ true
  | Zneg (xO _) ⇒ true
  | _false
  end.

Theorem ZevenP_correct :
  a, match ZevenP a with
           | trueFeven a
           | falseFodd a
           end.
intros a; case a; simpl in |- ×.
intros n e; case n; unfold ZevenP, Feven, Fodd in |- *; simpl in |- *;
 auto with arith.
apply EvenO.
intros p; case p; simpl in |- *; simpl in |- ×.
intros p1; (Zpos p1); rewrite Zpos_xI; ring.
intros p1; (Zpos p1); rewrite Zpos_xO; ring.
apply Odd1.
cut ( x, Zneg x = (- Zpos x)%Z);
 [ intros th1 | simpl in |- *; auto ].
intros p; case p; simpl in |- *; simpl in |- ×.
intros p1; (Zneg p1 + - (1))%Z; repeat rewrite th1;
 rewrite Zpos_xI; ring.
intros p1; (Zneg p1); repeat rewrite th1; rewrite Zpos_xO; ring.
(- (1))%Z; repeat rewrite th1; ring.
Qed.

Theorem Fcompare_correct :
  f1 f2 : float,
 match Fcompare radix f1 f2 with
 | Datatypes.Eqf1 = f2 :>R
 | Datatypes.Lt ⇒ (f1 < f2)%R
 | Datatypes.Gt ⇒ (f2 < f1)%R
 end.
intros f1 f2; generalize (Feq_bool_correct_t _ radixMoreThanOne f1 f2);
 generalize (Flt_bool_correct_t _ radixMoreThanOne f1 f2);
 generalize (Fle_bool_correct_f _ radixMoreThanOne f1 f2);
 unfold Flt_bool in |- *;
 unfold Flt_bool, Fle_bool, Feq_bool, Flt, Fle, Feq in |- *;
 case (Fcompare radix f1 f2); simpl in |- *; auto.
Qed.

Definition rClosestEvenPos (a : positive) (e : Z) :=
  match FindMin (vNum b) (Z2pos radix) a dExp e with
  | (r1, Float Z0 _)rExact r1
  | (r1, r2)
      match
        Fcompare radix (Float 1%nat (Fexp r1))
          (Float (2%nat × Fnum r2) (Fexp r2))
      with
      | Datatypes.LtrRound (FSucc b radix precision r1)
      | Datatypes.GtrRound r1
      | Datatypes.Eq
          match ZevenP r1 with
          | truerRound r1
          | falserRound (FSucc b radix precision r1)
          end
      end
  end.

Definition rOp a :=
  match a with
  | rExact frExact (Fopp f)
  | rRound frRound (Fopp f)
  end.

Definition rClosestEven (f : float) :=
  match f with
  | Float Z0 erExact (Float 0 dExp)
  | Float (Zpos a) erClosestEvenPos a e
  | Float (Zneg a) erOp (rClosestEvenPos a e)
  end.
Opaque FindMin.

Theorem RleR0Rminus : x y, (x y)%R → (0 y - x)%R.
intros x y; replace 0%R with (x - x)%R; auto with real.
unfold Rminus in |- *; auto with real.
Qed.

Theorem ClosestMin1 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max → (r - min max - r)%RClosest b radix r min.
intros r min max H H0 H1; (split; auto).
case H; auto.
intros f1 Hf1.
case (ClosestTotal b radix precision) with (r := r); auto with arith.
intros f2 Hf2; case (ClosestMinOrMax b radix) with (r := r) (p := f2);
 auto with arith.
intros H2.
replace (FtoR radix min) with (FtoRradix f2); auto.
case Hf2; auto.
apply (MinUniqueP b radix) with (r := r); auto with arith.
intros H2.
apply Rle_trans with (Rabs (FtoR radix f2 - r)).
2: case Hf2; auto.
replace (Rabs (FtoR radix min - r)) with (r - FtoRradix min)%R.
replace (Rabs (FtoR radix f2 - r)) with (FtoRradix max - r)%R; auto.
replace (FtoRradix max) with (FtoR radix f2).
apply sym_eq; apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H2; intros H3 (H4, H5); auto.
apply (MaxUniqueP b radix) with (r := r); auto with arith.
rewrite Rabs_minus_sym.
apply sym_eq; apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H; intros H3 (H4, H5); auto.
Qed.

Theorem ClosestMax1 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max → (max - r r - min)%RClosest b radix r max.
intros r min max H H0 H1; (split; auto).
case H0; auto.
intros f1 Hf1.
case (ClosestTotal b radix precision) with (r := r); auto with arith.
intros f2 Hf2; case (ClosestMinOrMax b radix) with (r := r) (p := f2);
 auto with arith.
intros H2.
apply Rle_trans with (Rabs (FtoR radix f2 - r)).
2: case Hf2; auto.
replace (Rabs (FtoR radix max - r)) with (FtoRradix max - r)%R.
replace (Rabs (FtoR radix f2 - r)) with (r - FtoRradix min)%R; auto.
replace (FtoRradix min) with (FtoR radix f2).
rewrite Rabs_minus_sym.
apply sym_eq; apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H2; intros H3 (H4, H5); auto.
apply (MinUniqueP b radix) with (r := r); auto with arith.
apply sym_eq; apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H0; intros H3 (H4, H5); auto.
intros H2.
replace (FtoR radix max) with (FtoRradix f2); auto.
case Hf2; auto.
apply (MaxUniqueP b radix) with (r := r); auto with arith.
Qed.

Theorem ClosestMin2 :
  (r : R) (min max f : float),
 isMin b radix r min
 isMax b radix r max
 (r - min < max - r)%RClosest b radix r ff = min :>R.
intros r min max f H H0 H1 H2.
case (ClosestMinOrMax b radix) with (r := r) (p := f); auto with arith;
 intros H3.
apply (MinUniqueP b radix) with (r := r); auto with arith.
Contradict H1; apply Rle_not_lt.
replace (FtoRradix max - r)%R with (Rabs (max - r)).
replace (r - FtoRradix min)%R with (Rabs (FtoRradix min - r)).
cut (Fbounded b min); [ intros Fmin | case H; auto ].
replace (FtoRradix max) with (FtoRradix f).
case H2; auto.
apply (MaxUniqueP b radix) with (r := r); auto with arith.
rewrite Rabs_minus_sym.
apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H; intros H4 (H5, H6); auto.
apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H0; intros H4 (H5, H6); auto.
Qed.

Theorem ClosestMax2 :
  (r : R) (min max f : float),
 isMin b radix r min
 isMax b radix r max
 (max - r < r - min)%RClosest b radix r ff = max :>R.
intros r min max f H H0 H1 H2.
case (ClosestMinOrMax b radix) with (r := r) (p := f); auto with arith;
 intros H3.
cut (Fbounded b max); [ intros Fmax | case H0; auto ].
Contradict H1; apply Rle_not_lt.
replace (FtoRradix max - r)%R with (Rabs (max - r)).
replace (r - FtoRradix min)%R with (Rabs (f - r)).
case H2; auto.
rewrite Rabs_minus_sym.
replace (FtoRradix min) with (FtoRradix f).
apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H3; intros H4 (H5, H6); auto.
apply (MinUniqueP b radix) with (r := r); auto with arith.
apply Rabs_pos_eq; auto.
apply RleR0Rminus.
case H0; intros H4 (H5, H6); auto.
apply (MaxUniqueP b radix) with (r := r); auto with arith.
Qed.

Theorem EvenClosestMin1 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max
 (r - min < max - r)%REvenClosest b radix precision r min.
intros r min max H H0 H1; split.
apply ClosestMin1 with (2 := H0); auto with real.
right; intros q H2; apply ClosestMin2 with (3 := H1); auto.
Qed.

Theorem EvenClosestMax1 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max
 (max - r < r - min)%REvenClosest b radix precision r max.
intros r min max H H0 H1; split.
apply ClosestMax1 with (1 := H); auto with real.
right; intros q H2; apply ClosestMax2 with (3 := H1); auto.
Qed.

Theorem EvenClosestMin2 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max
 (r - min)%R = (max - r)%R
 FNeven b radix precision minEvenClosest b radix precision r min.
intros r min max H H0 H1 H2; split; auto.
apply ClosestMin1 with (2 := H0); auto with real.
Qed.

Theorem EvenClosestMax2 :
  (r : R) (min max : float),
 isMin b radix r min
 isMax b radix r max
 (max - r)%R = (r - min)%R
 FNeven b radix precision maxEvenClosest b radix precision r max.
intros r min max H H0 H1; split; auto.
apply ClosestMax1 with (1 := H); auto with real.
Qed.

Theorem EqSpeTwice :
  x y z, (2%nat × (x - y))%R = (z - y)%R → (x - y)%R = (z - x)%R.
intros x y z H.
replace (x - y)%R with (2%nat × (x - y) - (x - y))%R;
 [ idtac | simpl in |- *; ring ].
rewrite H; ring.
Qed.

Theorem RltSpeTwice1 :
  x y z, (2%nat × (x - y) < z - y)%R → (x - y < z - x)%R.
intros x y z H.
replace (x - y)%R with (2%nat × (x - y) - (x - y))%R;
 [ idtac | simpl in |- *; ring ].
replace (z - x)%R with (z - y - (x - y))%R;
 [ unfold Rminus in |- *; auto with real | ring ].
Qed.

Theorem RltSpeTwice2 :
  x y z, (z - y < 2%nat × (x - y))%R → (z - x < x - y)%R.
intros x y z H.
replace (x - y)%R with (2%nat × (x - y) - (x - y))%R;
 [ idtac | simpl in |- *; ring ].
replace (z - x)%R with (z - y - (x - y))%R;
 [ unfold Rminus in |- *; auto with real | ring ].
Qed.

Theorem rClosestEvenPos_correct :
  (a : positive) (e : Z),
 EvenClosest b radix precision (Float (Zpos a) e)
   (rFloat (rClosestEvenPos a e))
 match rClosestEvenPos a e with
 | rExact rr = Float (Zpos a) e :>R
 | rRound rr Float (Zpos a) e :>R Fcanonic radix b r
 end.
intros a e; unfold rClosestEvenPos in |- *; generalize (FminOp_correct1 a e);
 generalize (FminOp_correct2 a e); generalize (FminOp_correct3 a e);
 generalize (FminOp_correct4 a e); generalize (FminOp_correct5 a e);
 generalize (FminOp_correct6 a e); generalize (FminOp_correct7 a e);
 simpl in |- *; case (FindMin (vNum b) (Z2pos radix) a dExp e);
 simpl in |- *; auto.
intros f0 f1; case f1; simpl in |- *; auto.
intros a'; case a'; simpl in |- *; auto.
intros e' H1 H2 H3 H4 H5 H6 H7; split; auto.
replace (FtoRradix (Float (Zpos a) e)) with (FtoRradix f0);
 auto with float arith.
unfold FtoRradix in |- *;
 apply
  RoundedModeProjectorIdem with (b := b) (P := EvenClosest b radix precision).
apply EvenClosestRoundedModeP; auto with arith.
case H1; simpl in |- *; auto.
rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
intros a'' e' H1 H2 H3 H4 H5 H6 H7.
cut (FtoRradix (Float (Zpos a'') e') 0%R :>R);
 [ intros NR1 | idtac ].
cut (Float (Zpos a) e f0 :>R); [ intros NR | idtac ].
case H4; clear H4; intros H4; [ Contradict NR1; auto | idtac ].
case H3; clear H3; intros H3; [ Contradict NR1; auto | idtac ].
generalize
 (Fcompare_correct (Float 1 (Fexp f0))
    (Float (Zpos (xO a'')) e'));
 case
  (Fcompare radix (Float 1 (Fexp f0))
     (Float (Zpos (xO a'')) e')).
generalize (ZevenP_correct f0); case (ZevenP f0); auto.
intros H8 H9; split; [ idtac | split ]; auto.
simpl in |- *;
 apply EvenClosestMin2 with (max := FNSucc b radix precision f0);
 auto.
apply MinMax; auto; auto with arith.
apply EqSpeTwice; auto.
apply sym_eq.
replace (2%nat × (FtoRradix (Float (Zpos a) e) - FtoRradix f0))%R with
 (FtoRradix (Float 1 (Fexp f0))).
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FNSuccUlpPos; auto.
unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H9; rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (INR (nat_of_P (xO a''))) with
 (nat_of_P a'' + nat_of_P a'')%R.
ring.
rewrite <- plus_INR; unfold nat_of_P in |- *; simpl in |- *;
 rewrite ZL6; auto.
unfold FNeven in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
intros H8 H9; split; [ idtac | split ]; auto.
simpl in |- *; apply EvenClosestMax2 with (min := f0); auto.
rewrite <-
 (FcanonicFnormalizeEq _ radixMoreThanOne b precision)
  with (p := f0); auto with arith.
change
  (isMax b radix (FtoRradix (Float (Zpos a) e))
     (FNSucc b radix precision f0)) in |- *; apply MinMax;
 auto with arith.
apply sym_eq; apply EqSpeTwice; auto.
apply sym_eq.
replace (2%nat × (FtoRradix (Float (Zpos a) e) - FtoRradix f0))%R with
 (FtoRradix (Float 1 (Fexp f0))).
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FSuccUlpPos; auto.
unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H9; rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (INR (nat_of_P (xO a''))) with
 (nat_of_P a'' + nat_of_P a'')%R.
ring.
rewrite <- plus_INR; unfold nat_of_P in |- *; simpl in |- *;
 rewrite ZL6; auto.
rewrite <-
 (FcanonicFnormalizeEq _ radixMoreThanOne b precision)
  with (p := f0); auto with arith.
change (FNeven b radix precision (FNSucc b radix precision f0)) in |- *;
 apply FNoddSuc; auto with arith.
unfold FNodd in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
apply Rgt_not_eq.
red in |- *; rewrite H7.
replace (FtoRradix (FSucc b radix precision f0)) with
 (FtoRradix f0 + (FSucc b radix precision f0 - FtoRradix f0))%R.
apply Rplus_lt_compat_l.
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FSuccUlpPos; auto.
ring.
auto with float arith.
intros H8; split; [ idtac | split ]; auto.
simpl in |- *; apply EvenClosestMax1 with (min := f0); auto with float arith.
rewrite <-
 (FcanonicFnormalizeEq _ radixMoreThanOne b precision)
  with (p := f0); auto with arith.
change
  (isMax b radix (FtoRradix (Float (Zpos a) e))
     (FNSucc b radix precision f0)) in |- *; apply MinMax;
 auto with arith.
apply RltSpeTwice2.
replace (2%nat × (FtoRradix (Float (Zpos a) e) - FtoRradix f0))%R with
 (FtoRradix (Float (Zpos (xO a'')) e')).
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FSuccUlpPos; auto.
unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
replace (powerRZ radix (Fexp f0)) with (FtoRradix (Float 1 (Fexp f0))); auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (INR (nat_of_P (xO a''))) with
 (nat_of_P a'' + nat_of_P a'')%R.
ring.
rewrite <- plus_INR; unfold nat_of_P in |- *; simpl in |- *;
 rewrite ZL6; auto.
apply Rgt_not_eq.
red in |- *; rewrite H7.
replace (FtoRradix (FSucc b radix precision f0)) with
 (FtoRradix f0 + (FSucc b radix precision f0 - FtoRradix f0))%R.
apply Rplus_lt_compat_l.
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FSuccUlpPos; auto.
ring.
auto with float arith.
intros H8; split; [ idtac | split ]; auto.
simpl in |- *;
 apply EvenClosestMin1 with (max := FNSucc b radix precision f0);
 auto with float arith.
apply RltSpeTwice1.
replace (2%nat × (FtoRradix (Float (Zpos a) e) - FtoRradix f0))%R with
 (FtoRradix (Float (Zpos (xO a'')) e')).
rewrite <- (Fminus_correct radix); auto with arith.
rewrite FNSuccUlpPos; auto.
unfold Fulp in |- ×.
rewrite FcanonicFnormalizeEq; auto with arith.
replace (powerRZ radix (Fexp f0)) with (FtoRradix (Float 1 (Fexp f0))); auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
rewrite H7; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace (INR (nat_of_P (xO a''))) with
 (nat_of_P a'' + nat_of_P a'')%R.
ring.
rewrite <- plus_INR; unfold nat_of_P in |- *; simpl in |- *;
 rewrite ZL6; auto.
Contradict NR1;
 replace 0%R with (Float (Zpos a) e - Float (Zpos a) e)%R;
 [ idtac | ring ].
pattern (Float (Zpos a) e) at 2 in |- *; rewrite H7; rewrite NR1; ring.
apply NotR0NotZero; simpl in |- *; red in |- *; intros; discriminate.
intros p Fexp H H0 H1 H2 H3 H4; Contradict H4.
apply Rlt_not_le.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
replace 0%R with (-0 × powerRZ radix Fexp)%R; auto with real arith.
Qed.

Theorem rClosestEven_correct :
  f : float,
 EvenClosest b radix precision f (rFloat (rClosestEven f))
 match rClosestEven f with
 | rExact rr = f :>R
 | rRound rr f :>R Fcanonic radix b r
 end.
intros f; case f; intros a e; case a; simpl in |- ×.
split; auto.
replace (FtoRradix (Float 0 e)) with (FtoRradix (Float 0 dExp)).
unfold FtoRradix in |- *;
 apply
  RoundedModeProjectorIdem with (b := b) (P := EvenClosest b radix precision);
 auto with float arith.
repeat (split; simpl in |- *; auto with zarith).
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
intros p; simpl in |- *; apply rClosestEvenPos_correct.
intros p; generalize (rClosestEvenPos_correct p e);
 case (rClosestEvenPos p e); simpl in |- *; auto.
intros f1 (H1, H2);
 replace (Float (Zneg p) e) with (Fopp (Float (Zpos p) e));
 try repeat rewrite (Fopp_correct radix); split; auto with real.
apply (EvenClosestSymmetric b radix precision); auto with arith.
intros f1 (H1, (H2, H3));
 replace (Float (Zneg p) e) with (Fopp (Float (Zpos p) e));
 try repeat rewrite (Fopp_correct radix); split; [ idtac | split ];
 auto with real float.
apply (EvenClosestSymmetric b radix precision); auto with arith zarith.
fold FtoRradix in |- *; Contradict H2; rewrite <- Ropp_involutive;
 rewrite <- H2; auto with real.
Qed.
End FminOp.
Transparent Pdiv.
Transparent PdivBound.
Transparent FindMin.