(****************************************************************************
                                                                             
          IEEE754  :  FroundProp                                                     
                                                                             
          Laurent Thery, Sylvie Boldo                                                      
                                                                             
  ******************************************************************************)
Require Export Fround.
Require Export MSB.
Section FRoundP.
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.
 
Definition Fulp (p : float) :=
  powerRZ radix (Fexp (Fnormalize radix b precision p)).
 
Theorem FulpComp :
 forall p q : float,
 Fbounded b p -> Fbounded b q -> p = q :>R -> Fulp p = Fulp q.
(* Goal: forall (p q : float) (_ : Fbounded b p) (_ : Fbounded b q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq R (Fulp p) (Fulp q) *)
intros p q H' H'0 H'1; unfold Fulp in |- *.
rewrite
 FcanonicUnique
                with
                (p := Fnormalize radix b precision p)
               (q := Fnormalize radix b precision q)
               (3 := pGivesBound); auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix (Fnormalize radix b precision q)) *)
apply trans_eq with (FtoR radix p).
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
apply FnormalizeCorrect; auto.
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
apply trans_eq with (FtoR radix q); auto.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
apply sym_eq; apply FnormalizeCorrect; auto.
Qed.
 
Theorem FulpLe :
 forall p : float, Fbounded b p -> (Fulp p <= Float 1 (Fexp p))%R.
intros p H'; unfold Fulp, FtoRradix, FtoR, Fnormalize in |- *; simpl in |- *;
(* Goal: Rle (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x))))))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
 rewrite Rmult_1_l.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (if Z_zerop (Fnum p) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p))) (powerRZ (IZR radix) (Fexp p)) *)
case (Z_zerop (Fnum p)); simpl in |- *; auto.
intros H'0; apply (Rle_powerRZ radix (- dExp b) (Fexp p));
 auto with float real zarith.
(* Goal: forall _ : not (@eq Z (Fnum p) Z0), Rle (powerRZ (IZR radix) (Z.sub (Fexp p) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (powerRZ (IZR radix) (Fexp p)) *)
intros H'0; apply Rle_powerRZ; auto with real zarith arith.
Qed.
 
Theorem Fulp_zero :
 forall x : float, is_Fzero x -> Fulp x = powerRZ radix (- dExp b).
intros x; unfold is_Fzero, Fulp, Fnormalize in |- *; case (Z_zerop (Fnum x));
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
 simpl in |- *; auto.
(* Goal: forall (_ : not (@eq Z (Fnum x) Z0)) (_ : @eq Z (Fnum x) Z0), @eq R (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x))))))) (powerRZ (IZR radix) (Z.opp (Z.of_N (dExp b)))) *)
intros H' H'0; Contradict H'; auto.
Qed.
 
Theorem FulpLe2 :
 forall p : float,
 Fbounded b p ->
 Fnormal radix b (Fnormalize radix b precision p) ->
 (Fulp p <= Rabs p * powerRZ radix (Zsucc (- precision)))%R.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Fnormal radix b (Fnormalize radix b precision p)), Rle (Fulp p) (Rmult (Rabs (FtoRradix p)) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision))))) *)
intros p H1 H2; unfold Fulp in |- *.
replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p));
 [ idtac | unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ].
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision p))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision))))) *)
apply Rmult_le_reg_l with (powerRZ radix (Zpred precision)).
(* Goal: Rlt (IZR Z0) (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) *)
(* Goal: Rle (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision p)))) (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision)))))) *)
apply powerRZ_lt; auto with real arith.
replace
 (powerRZ radix (Zpred precision) *
  (Rabs (Fnormalize radix b precision p) *
   powerRZ radix (Zsucc (- precision))))%R with
 (Rabs (Fnormalize radix b precision p)).
(* Goal: Rle (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (Rminus (powerRZ (IZR radix) (Z.of_nat precision)) (IZR (Zpos xH))) (Fulp p)) *)
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with arith real.
(* Goal: Rle (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision p)))) (FtoR radix (Fabs (Fnormalize radix b precision p))) *)
(* Goal: @eq R (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision)))))) *)
unfold Fabs, FtoR in |- *; simpl in |- *.
apply Rmult_le_compat_r; [ apply powerRZ_le | rewrite <- inj_pred ];
 auto with real arith zarith.
(* Goal: Rle (powerRZ (IZR radix) (Z.of_nat (Init.Nat.pred precision))) (IZR (Z.abs (Fnum (Fnormalize radix b precision p)))) *)
(* Goal: @eq R (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision)))))) *)
rewrite <- Zpower_nat_Z_powerRZ.
replace (Zpower_nat radix (pred precision)) with (nNormMin radix precision);
 auto; apply Rle_IZR.
(* Goal: Z.le (nNormMin radix precision) (Z.abs (Fnum (Fnormalize radix b precision p))) *)
(* Goal: @eq R (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision)))))) *)
apply pNormal_absolu_min with b; auto with arith zarith real.
apply
 trans_eq
  with
    (Rabs (Fnormalize radix b precision p) *
     (powerRZ radix (Zpred precision) * powerRZ radix (Zsucc (- precision))))%R;
 [ idtac | ring ].
(* Goal: @eq R (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (powerRZ (IZR radix) (Z.pred (Z.of_nat precision))) (powerRZ (IZR radix) (Z.succ (Z.opp (Z.of_nat precision)))))) *)
rewrite <- powerRZ_add; auto with zarith real.
replace (Zpred precision + Zsucc (- precision))%Z with 0%Z;
 [ simpl in |- *; ring | unfold Zsucc, Zpred in |- *; ring ];
 auto with real zarith.
Qed.
 
Theorem FulpGe :
 forall p : float,
 Fbounded b p -> (Rabs p <= (powerRZ radix precision - 1) * Fulp p)%R.
(* Goal: forall (p : float) (_ : Fbounded b p), Rle (Rabs (FtoRradix p)) (Rmult (Rminus (powerRZ (IZR radix) (Z.of_nat precision)) (IZR (Zpos xH))) (Fulp p)) *)
intros p H.
replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p));
 [ idtac | unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ].
(* Goal: Rle (Rabs (FtoRradix (Fnormalize radix b precision p))) (Rmult (Rminus (powerRZ (IZR radix) (Z.of_nat precision)) (IZR (Zpos xH))) (Fulp p)) *)
unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with arith real.
(* Goal: Rle (FtoR radix (Fabs (Fnormalize radix b precision p))) (Rmult (Rminus (powerRZ (IZR radix) (Z.of_nat precision)) (IZR (Zpos xH))) (Fulp p)) *)
unfold FtoR in |- *; simpl in |- *; unfold Fulp in |- *.
apply Rmult_le_compat_r; [ apply powerRZ_le | idtac ];
 auto with real arith zarith.
apply Rle_trans with (IZR (Zpred (Zpos (vNum b))));
 [ apply Rle_IZR; auto with float zarith | idtac ].
unfold Zpred in |- *; right; rewrite pGivesBound; replace 1%R with (IZR 1);
 auto with real.
(* Goal: @eq R (IZR (Z.add (Zpower_nat radix precision) (Zneg xH))) (Rminus (powerRZ (IZR radix) (Z.of_nat precision)) (IZR (Zpos xH))) *)
rewrite <- Zpower_nat_Z_powerRZ; rewrite Z_R_minus;auto.
Qed.
 
Theorem LeFulpPos :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y -> (0 <= x)%R -> (x <= y)%R -> (Fulp x <= Fulp y)%R.
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (IZR Z0) (FtoRradix x)) (_ : Rle (FtoRradix x) (FtoRradix y)), Rle (Fulp x) (Fulp y) *)
intros x y Hx Hy H1 H2; unfold Fulp in |- *.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Fexp p)) *)
apply Rle_powerRZ; auto with real zarith.
(* Goal: Z.le (Fexp (Fnormalize radix b precision x)) (Fexp (Fnormalize radix b precision y)) *)
apply Fcanonic_Rle_Zle with radix b precision; auto with zarith arith.
(* Goal: Fcanonic radix b (Fnormalize radix b precision y) *)
(* Goal: Rle (Rabs (FtoR radix (Fnormalize radix b precision x))) (Rabs (FtoR radix (Fnormalize radix b precision y))) *)
apply FnormalizeCanonic; auto with zarith arith.
(* Goal: Fcanonic radix b (Fnormalize radix b precision y) *)
(* Goal: Rle (Rabs (FtoR radix (Fnormalize radix b precision x))) (Rabs (FtoR radix (Fnormalize radix b precision y))) *)
apply FnormalizeCanonic; auto with zarith arith.
(* Goal: Rle (Rabs (FtoR radix (Fnormalize radix b precision x))) (Rabs (FtoR radix (Fnormalize radix b precision y))) *)
repeat rewrite FnormalizeCorrect; auto with zarith arith real.
(* Goal: Rle (Rabs (FtoR radix x)) (Rabs (FtoR radix y)) *)
repeat rewrite Rabs_right; auto with zarith arith real.
(* Goal: Rge (FtoR radix y) (IZR Z0) *)
apply Rge_trans with (FtoRradix x); auto with real.
Qed.
 
Theorem FulpSucCan :
 forall p : float,
 Fcanonic radix b p -> (FSucc b radix precision p - p <= Fulp p)%R.
(* Goal: forall (p : float) (_ : Fbounded b p), Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
intros p H'.
replace (Fulp p) with (powerRZ radix (Fexp p)).
2: unfold Fulp in |- *; replace (Fnormalize radix b precision p) with p; auto;
    apply sym_equal; apply FcanonicUnique with (3 := pGivesBound);
    auto with arith; apply FnormalizeCanonic || apply FnormalizeCorrect;
    auto with float zarith.
2: apply FcanonicBound with (1 := H'); auto with float zarith.
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with zarith.
case (Z_eq_dec (Fnum p) (- nNormMin radix precision)); intros H1'.
case (Z_eq_dec (Fexp p) (- dExp b)); intros H2'.
rewrite FSuccDiff2; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real.
rewrite FSuccDiff3; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l.
apply Rlt_le; apply Rlt_powerRZ; auto with real zarith.
unfold Zpred in |- *; auto with zarith.
rewrite FSuccDiff1; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real.
Qed.
 
Theorem FulpSuc :
 forall p : float,
 Fbounded b p -> (FNSucc b radix precision p - p <= Fulp p)%R.
(* Goal: forall (p : float) (_ : Fbounded b p), Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
intros p H'.
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
replace (Fulp p) with (Fulp (Fnormalize radix b precision p)).
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp (Fnormalize radix b precision p)) *)
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)).
(* Goal: Rle (Rminus (FtoRradix (FNSucc b radix precision p)) (FtoRradix (Fnormalize radix b precision p))) (Fulp (Fnormalize radix b precision p)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision p)) (FtoRradix p) *)
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
unfold FNSucc in |- *; apply FulpSucCan; auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
apply FulpComp; auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
Qed.
 
Theorem FulpPredCan :
 forall p : float,
 Fcanonic radix b p -> (p - FPred b radix precision p <= Fulp p)%R.
(* Goal: forall (p : float) (_ : Fbounded b p), Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
intros p H'.
replace (Fulp p) with (powerRZ radix (Fexp p)).
2: unfold Fulp in |- *; replace (Fnormalize radix b precision p) with p; auto;
    apply sym_equal; apply FcanonicUnique with (3 := pGivesBound);
    auto with arith; apply FnormalizeCanonic || apply FnormalizeCorrect;
    auto with arith.
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with arith.
case (Z_eq_dec (Fnum p) (nNormMin radix precision)); intros H1'.
case (Z_eq_dec (Fexp p) (- dExp b)); intros H2'.
rewrite FPredDiff2; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real.
rewrite FPredDiff3; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real.
apply Rlt_le; apply Rlt_powerRZ; auto with real zarith.
(* Goal: Rle (IZR (Zpos xH)) (IZR radix) *)
(* Goal: Z.le (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))))) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)) *)
replace 1%R with (INR 1); auto with real arith.
unfold Zpred in |- *; auto with zarith.
rewrite FPredDiff1; auto with arith.
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real.
apply FcanonicBound with (1 := H').
Qed.
 
Theorem FulpPred :
 forall p : float,
 Fbounded b p -> (p - FNPred b radix precision p <= Fulp p)%R.
(* Goal: forall (p : float) (_ : Fbounded b p), Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
intros p H'.
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp p) *)
replace (Fulp p) with (Fulp (Fnormalize radix b precision p)).
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix (FNPred b radix precision p))) (Fulp (Fnormalize radix b precision p)) *)
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)).
(* Goal: Rle (Rminus (FtoRradix (Fnormalize radix b precision p)) (FtoRradix (FNPred b radix precision p))) (Fulp (Fnormalize radix b precision p)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision p)) (FtoRradix p) *)
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
unfold FNPred in |- *; apply FulpPredCan; auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
(* Goal: @eq R (Fulp (Fnormalize radix b precision p)) (Fulp p) *)
apply FulpComp; auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
Qed.
 
Theorem FSuccDiffPos :
 forall x : float,
 (0 <= x)%R ->
 Fminus radix (FSucc b radix precision x) x = Float 1%nat (Fexp x) :>R.
(* Goal: forall (x : float) (_ : Rle (IZR Z0) (FtoRradix x)), @eq R (FtoRradix (Fminus radix (FSucc b radix precision x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
intros x H.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
unfold FtoRradix in |- *; apply FSuccDiff1; auto with arith.
(* Goal: not (@eq Z (Fnum x) (Z.opp (nNormMin radix precision))) *)
Contradict H; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H.
(* Goal: not (Rle (IZR Z0) (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Fexp x)))) *)
apply Rlt_not_le.
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Fexp x))) (IZR Z0) *)
replace 0%R with (0 * powerRZ radix (Fexp x))%R; [ idtac | ring ].
(* Goal: Rlt (Rmult (IZR (Z.opp (nNormMin radix precision))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR Z0) (powerRZ (IZR radix) (Fexp x))) *)
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 FulpFPredGePos :
 forall f : float,
 Fbounded b f ->
 Fcanonic radix b f ->
 (0 < f)%R -> (Fulp (FPred b radix precision f) <= Fulp f)%R.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Fcanonic radix b f) (_ : Rlt (IZR Z0) (FtoRradix f)), Rle (Fulp (FPred b radix precision f)) (Fulp f) *)
intros f Hf1 Hf2 H.
(* Goal: Rle (Fulp (FPred b radix precision f)) (Fulp f) *)
apply LeFulpPos; auto with zarith float; unfold FtoRradix in |- *.
(* Goal: Rle (IZR Z0) (FtoR radix (FPred b radix precision f)) *)
(* Goal: Rle (FtoR radix (FPred b radix precision f)) (FtoR radix f) *)
apply R0RltRlePred; auto with arith.
(* Goal: Rle (FtoR radix (FPred b radix precision f)) (FtoR radix f) *)
apply Rlt_le; apply FPredLt; auto with arith.
Qed.
 
Theorem CanonicFulp :
 forall p : float, Fcanonic radix b p -> Fulp p = Float 1%nat (Fexp p).
intros p H; unfold Fulp in |- *.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision x)) x)) (Fulp x) *)
rewrite FcanonicFnormalizeEq; auto with arith.
(* Goal: @eq R (powerRZ (IZR radix) e) (FtoRradix (Float (Z.of_nat (S O)) e)) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
Qed.
 
Theorem FSuccUlpPos :
 forall x : float,
 Fcanonic radix b x ->
 (0 <= x)%R -> Fminus radix (FSucc b radix precision x) x = Fulp x :>R.
(* Goal: forall (x : float) (_ : Fcanonic radix b x) (_ : Rle (IZR Z0) (FtoRradix x)), @eq R (FtoRradix (Fminus radix (FSucc b radix precision x) x)) (Fulp x) *)
intros x H H0; rewrite CanonicFulp; auto.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision x) x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) *)
apply FSuccDiffPos; auto.
Qed.
 
Theorem FNSuccUlpPos :
 forall x : float,
 Fcanonic radix b x ->
 (0 <= x)%R -> Fminus radix (FNSucc b radix precision x) x = Fulp x :>R.
(* Goal: forall (x : float) (_ : Fcanonic radix b x) (_ : Rle (IZR Z0) (FtoRradix x)), @eq R (FtoRradix (Fminus radix (FNSucc b radix precision x) x)) (Fulp x) *)
intros x H H0.
(* Goal: @eq R (FtoRradix (Fminus radix (FNSucc b radix precision x) x)) (Fulp x) *)
unfold FNSucc in |- *.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision (Fnormalize radix b precision x)) x)) (Fulp x) *)
rewrite FcanonicFnormalizeEq; auto with arith.
(* Goal: @eq R (FtoRradix (Fminus radix (FSucc b radix precision x) x)) (Fulp x) *)
apply FSuccUlpPos; auto.
Qed.
 
Theorem FulpFabs : forall f : float, Fulp f = Fulp (Fabs f) :>R.
(* Goal: forall f : float, @eq R (Fulp f) (Fulp (Fabs f)) *)
intros f; unfold Fulp in |- *; case (Rle_or_lt 0 f); intros H'.
replace (Fabs f) with f; auto; unfold Fabs in |- *; apply floatEq;
 simpl in |- *; auto with zarith real.
(* Goal: @eq Z (Fnum f) (Z.abs (Fnum f)) *)
(* Goal: @eq R (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision f))) (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision (Fabs f)))) *)
apply sym_eq; apply Zabs_eq; apply LeR0Fnum with radix; auto with zarith real.
replace (Fabs f) with (Fopp f);
 [ rewrite Fnormalize_Fopp | apply floatEq; simpl in |- * ]; 
 auto with arith.
apply sym_eq; apply Zabs_eq_opp; apply R0LeFnum with radix;
 auto with zarith real.
Qed.
 
Theorem RoundedModeUlp :
 forall P,
 RoundedModeP b radix P ->
 forall (p : R) (q : float), P p q -> (Rabs (p - q) < Fulp q)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (p : R) (q : float) (_ : P p q), Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
intros P H' p q H'0.
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
case (Req_dec p q); intros Eq1.
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
rewrite <- Eq1.
(* Goal: Rlt (Rabs (Rminus p p)) (Fulp q) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
replace (p - p)%R with 0%R; [ idtac | ring ].
(* Goal: Rlt (Rabs (IZR Z0)) (Fulp q) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
rewrite Rabs_R0; auto.
(* Goal: Rlt (IZR Z0) (Fulp q) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
unfold Fulp, FtoRradix, FtoR in |- *; simpl in |- *; auto with real arith.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'1 H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6;
 case H'5 with (1 := H'0); clear H'5 H'4 H'2; intros H'5.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Rabs_right; auto.
(* Goal: Rlt (Rminus (FtoRradix q) p) (Fulp q) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
cut (Fbounded b q); [ intros B0 | case H'5; auto ].
(* Goal: Rlt (Rminus p (FtoRradix q)) (Fulp q) *)
(* Goal: Rge (Rminus p (FtoRradix q)) (IZR Z0) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
apply Rlt_le_trans with (2 := FulpSuc q B0).
(* Goal: Rlt (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q)))) (Ropp (Rminus (FtoRradix q) p)) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply Rplus_lt_reg_l with (r := FtoR radix q).
(* Goal: Rle (Rplus (FtoR radix q) (Rminus p (FtoRradix q))) (Rplus (FtoR radix q) (IZR Z0)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rlt p (FtoRradix (FNSucc b radix precision q)) *)
(* Goal: Rge (Rminus p (FtoRradix q)) (IZR Z0) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
case (Rle_or_lt (FNSucc b radix precision q) p); auto.
(* Goal: forall _ : Rle (FtoRradix (FNSucc b radix precision q)) p, Rlt p (FtoRradix (FNSucc b radix precision q)) *)
(* Goal: Rge (Rminus p (FtoRradix q)) (IZR Z0) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
intros H'2; absurd (FNSucc b radix precision q <= q)%R; auto.
apply Rgt_not_le; red in |- *; unfold FtoRradix in |- *;
 auto with real float arith.
(* Goal: Rle (FtoRradix q) (FtoRradix (FNPred b radix precision q)) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
case H'5; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (Rle p (FtoR radix q)) (forall (f : float) (_ : Fbounded b f) (_ : Rle p (FtoR radix f)), Rle (FtoR radix q) (FtoR radix f))), Rle (FtoRradix q) (FtoRradix (FNPred b radix precision q)) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
intros H'4 H'7; elim H'7; intros H'8 H'9; apply H'9; clear H'7; auto.
(* Goal: Fbounded b (FNPred b radix precision q) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply (FcanonicBound radix b); auto with float arith.
(* Goal: Rge (Rminus p (FtoRradix q)) (IZR Z0) *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q).
(* Goal: Rle (Rplus (FtoR radix q) (Rminus p (FtoRradix q))) (Rplus (FtoR radix q) (IZR Z0)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rplus (FtoR radix q) (IZR Z0)) p *)
(* Goal: Rlt (Rabs (Rminus p (FtoRradix q))) (Fulp q) *)
rewrite Rplus_0_r; apply isMin_inv1 with (1 := H'5); auto.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Faux.Rabsolu_left1; auto.
(* Goal: Rlt (Ropp (Rminus p (FtoRradix q))) (Fulp q) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
rewrite Ropp_minus_distr; auto.
(* Goal: Rlt (Rminus (FtoRradix q) p) (Fulp q) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
cut (Fbounded b q); [ intros B0 | case H'5; auto ].
(* Goal: Rlt (Rminus (FtoRradix q) p) (Fulp q) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply Rlt_le_trans with (2 := FulpPred q B0).
(* Goal: Rlt (Rminus (FtoRradix q) p) (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply Ropp_lt_cancel; repeat rewrite Rminus_0_l.
(* Goal: Rlt (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q)))) (Ropp (Rminus (FtoRradix q) p)) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply Rplus_lt_reg_l with (r := FtoR radix q).
(* Goal: Rle (Rplus (FtoR radix q) (Rminus p (FtoRradix q))) (Rplus (FtoR radix q) (IZR Z0)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
case (Rle_or_lt p (FNPred b radix precision q)); auto.
(* Goal: forall _ : Rle p (FtoRradix (FNPred b radix precision q)), Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
intros H'2; absurd (q <= FNPred b radix precision q)%R; auto.
apply Rgt_not_le; red in |- *; unfold FtoRradix in |- *;
 auto with real float arith.
(* Goal: Rle (FtoRradix q) (FtoRradix (FNPred b radix precision q)) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
case H'5; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (Rle p (FtoR radix q)) (forall (f : float) (_ : Fbounded b f) (_ : Rle p (FtoR radix f)), Rle (FtoR radix q) (FtoR radix f))), Rle (FtoRradix q) (FtoRradix (FNPred b radix precision q)) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
intros H'4 H'7; elim H'7; intros H'8 H'9; apply H'9; clear H'7; auto.
(* Goal: Fbounded b (FNPred b radix precision q) *)
(* Goal: forall _ : Rlt (FtoRradix (FNPred b radix precision q)) p, Rlt (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) (FtoRradix (FNPred b radix precision q))))) (Rplus (FtoR radix q) (Ropp (Rminus (FtoRradix q) p))) *)
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply (FcanonicBound radix b); auto with float arith.
intros H1; apply Rplus_lt_compat_l; auto with real; apply Ropp_lt_contravar;
 unfold Rminus in |- *; auto with real.
(* Goal: Rle (Rminus p (FtoRradix q)) (IZR Z0) *)
apply Rplus_le_reg_l with (r := FtoR radix q).
(* Goal: Rle (Rplus (FtoR radix q) (Rminus p (FtoRradix q))) (Rplus (FtoR radix q) (IZR Z0)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle p (Rplus (FtoR radix q) (IZR Z0)) *)
rewrite Rplus_0_r; apply isMax_inv1 with (1 := H'5).
Qed.
 
Theorem RoundedModeErrorExpStrict :
 forall P,
 RoundedModeP b radix P ->
 forall (p q : float) (x : R),
 Fbounded b p ->
 Fbounded b q ->
 P x p -> q = (x - p)%R :>R -> q <> 0%R :>R -> (Fexp q < Fexp p)%Z.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (p q : float) (x : R) (_ : Fbounded b p) (_ : Fbounded b q) (_ : P x p) (_ : @eq R (FtoRradix q) (Rminus x (FtoRradix p))) (_ : not (@eq R (FtoRradix q) (IZR Z0))), Z.lt (Fexp q) (Fexp p) *)
intros P H p q x H0 H1 H2 H3 H4.
(* Goal: Z.lt (Fexp q) (Fexp p) *)
apply Zlt_powerRZ with (e := IZR radix); auto with real zarith.
(* Goal: Rlt (powerRZ (IZR radix) (Fexp q)) (powerRZ (IZR radix) (Fexp p)) *)
apply Rle_lt_trans with (FtoRradix (Fabs q)).
replace (powerRZ radix (Fexp q)) with (FtoRradix (Float 1%nat (Fexp q)));
 unfold FtoRradix in |- *;
 [ apply Fop.RleFexpFabs; auto with arith
 | unfold FtoR in |- *; simpl in |- *; ring ].
(* Goal: Rlt (FtoRradix (Fabs q)) (powerRZ (IZR radix) (Fexp p)) *)
rewrite (Fabs_correct radix); auto with zarith.
(* Goal: Rlt (Rabs (FtoR radix q)) (powerRZ (IZR radix) (Fexp p)) *)
fold FtoRradix in |- *; rewrite H3.
apply Rlt_le_trans with (Fulp p);
 [ apply RoundedModeUlp with P; auto | unfold Fulp in |- * ].
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fnormalize radix b precision p))) (powerRZ (IZR radix) (Fexp p)) *)
apply Rle_powerRZ; auto with real zarith.
(* Goal: Z.le (Fexp (Fnormalize radix b precision p)) (Fexp p) *)
apply FcanonicLeastExp with radix b precision; auto with real arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision p)) (FtoR radix p) *)
(* Goal: @eq R (FtoR radix p) (FtoR radix (Fnormalize radix b precision q)) *)
apply sym_eq; apply FnormalizeCorrect; auto.
(* Goal: Fcanonic radix b (Fnormalize radix b precision p) *)
apply FnormalizeCanonic; auto with zarith.
Qed.
 
Theorem RoundedModeProjectorIdem :
 forall P (p : float), RoundedModeP b radix P -> Fbounded b p -> P p p.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (_ : RoundedModeP b radix P) (_ : Fbounded b p), P (FtoRradix p) p *)
intros P p H' H.
elim H'; intros H'0 H'1; elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5;
 clear H'3 H'1.
(* Goal: P (FtoRradix p) p *)
case (H'0 p).
(* Goal: forall (x : float) (_ : P (FtoRradix p) x), P (FtoRradix p) p *)
intros x H'6.
(* Goal: P (FtoRradix p) p *)
apply (H'2 p p x); auto.
(* Goal: @eq R (FtoR radix x) (FtoR radix p) *)
apply sym_eq; apply (RoundedProjector _ _ P H'); auto.
Qed.
 
Theorem RoundedModeBounded :
 forall P (r : R) (q : float),
 RoundedModeP b radix P -> P r q -> Fbounded b q.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (r : R) (q : float) (_ : RoundedModeP b radix P) (_ : P r q), Fbounded b q *)
intros P r q H' H'0.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'1 H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6;
 case H'5 with (1 := H'0); clear H'4 H'2; intros H; 
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x) *)
(* Goal: Z.le (Fexp x) (LSB radix x) *)
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix x))) *)
 case H; auto.
Qed.
 
Theorem RoundedModeProjectorIdemEq :
 forall (P : R -> float -> Prop) (p q : float),
 RoundedModeP b radix P -> Fbounded b p -> P (FtoR radix p) q -> p = q :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p q : float) (_ : RoundedModeP b radix P) (_ : Fbounded b p) (_ : P (FtoR radix p) q), @eq R (FtoRradix p) (FtoRradix q) *)
intros P p q H' H'0 H'1.
cut (MinOrMaxP b radix P);
 [ intros Mn; case (Mn p q); auto; intros Mn1 | auto with inv ].
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply sym_eq; apply MinEq with (1 := Mn1); auto.
(* Goal: isMin b radix (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply (RoundedModeProjectorIdem (isMin b radix)); auto.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply MinRoundedModeP with (precision := precision); auto.
(* Goal: @eq R (FtoRradix p) (FtoRradix q) *)
apply sym_eq; apply MaxEq with (1 := Mn1); auto.
(* Goal: isMax b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply (RoundedModeProjectorIdem (isMax b radix)); auto.
(* Goal: RoundedModeP b radix (isMax b radix) *)
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply MaxRoundedModeP with (precision := precision); auto.
Qed.
 
Theorem RoundedModeMult :
 forall P,
 RoundedModeP b radix P ->
 forall (r : R) (q q' : float),
 P r q -> Fbounded b q' -> (r <= radix * q')%R -> (q <= radix * q')%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (r : R) (q q' : float) (_ : P r q) (_ : Fbounded b q') (_ : Rle (Rmult (IZR radix) (FtoRradix q')) r), Rle (Rmult (IZR radix) (FtoRradix q')) (FtoRradix q) *)
intros P H' r q q' H'0 H'1.
(* Goal: forall _ : Rle (Rmult (IZR radix) (FtoRradix q')) r, Rle (Rmult (IZR radix) (FtoRradix q')) (FtoRradix q) *)
replace (radix * q')%R with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat))).
(* Goal: forall _ : Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'2; case H'2.
intros H'3; case H'; intros H'4 H'5; elim H'5; intros H'6 H'7; elim H'7;
 intros H'8 H'9; apply H'9 with (1 := H'3); clear H'7 H'5; 
 auto.
(* Goal: P (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdem; auto.
(* Goal: Fbounded b (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O)))) *)
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply FBoundedScale; auto.
(* Goal: forall _ : @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'3.
replace (FtoRradix q) with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat)));
 auto with real.
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply (RoundedProjector _ _ P H'); auto.
(* Goal: Fbounded b (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O)))) *)
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply FBoundedScale; auto.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
(* Goal: forall (_ : TotalP P) (_ : and (CompatibleP b radix P) (and (MinOrMaxP b radix P) (MonotoneP radix P))), @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5.
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply (H'6 r (Float (Fnum q') (Fexp q' + 1%nat)) q); auto.
(* Goal: Fbounded b q *)
apply RoundedModeBounded with (P := P) (r := r); auto.
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
rewrite (FvalScale _ radixMoreThanOne b).
(* Goal: @eq R (Rmult (powerRZ (IZR radix) (Z.of_nat (S O))) (FtoR radix q')) (Rmult (IZR radix) (FtoR radix q')) *)
rewrite powerRZ_1; auto.
Qed.
 
Theorem RoundedModeMultLess :
 forall P,
 RoundedModeP b radix P ->
 forall (r : R) (q q' : float),
 P r q -> Fbounded b q' -> (radix * q' <= r)%R -> (radix * q' <= q)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (r : R) (q q' : float) (_ : P r q) (_ : Fbounded b q') (_ : Rle (Rmult (IZR radix) (FtoRradix q')) r), Rle (Rmult (IZR radix) (FtoRradix q')) (FtoRradix q) *)
intros P H' r q q' H'0 H'1.
(* Goal: forall _ : Rle (Rmult (IZR radix) (FtoRradix q')) r, Rle (Rmult (IZR radix) (FtoRradix q')) (FtoRradix q) *)
replace (radix * q')%R with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat))).
(* Goal: forall _ : Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'2; case H'2.
intros H'3; case H'; intros H'4 H'5; elim H'5; intros H'6 H'7; elim H'7;
 intros H'8 H'9; apply H'9 with (1 := H'3); clear H'7 H'5; 
 auto.
(* Goal: P (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdem; auto.
(* Goal: Fbounded b (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O)))) *)
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply FBoundedScale; auto.
(* Goal: forall _ : @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'3.
replace (FtoRradix q) with (FtoRradix (Float (Fnum q') (Fexp q' + 1%nat)));
 auto with real.
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply (RoundedProjector _ _ P H'); auto.
(* Goal: Fbounded b (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O)))) *)
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
apply FBoundedScale; auto.
(* Goal: P (FtoR radix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) q *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
unfold FtoRradix in H'3; rewrite H'3; auto.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
(* Goal: forall (_ : TotalP P) (_ : and (CompatibleP b radix P) (and (MinOrMaxP b radix P) (MonotoneP radix P))), @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5.
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
unfold FtoRradix in |- *; rewrite FvalScale; auto.
(* Goal: @eq R (Rmult (powerRZ (IZR radix) (Z.of_nat (S O))) (FtoR radix q')) (Rmult (IZR radix) (FtoR radix q')) *)
rewrite powerRZ_1; auto.
Qed.
 
Theorem RleMinR0 :
 forall (r : R) (min : float),
 (0 <= r)%R -> isMin b radix r min -> (0 <= min)%R.
(* Goal: forall (r : R) (min : float) (_ : Rle (IZR Z0) r) (_ : isMin b radix r min), Rle (IZR Z0) (FtoRradix min) *)
intros r min H' H'0.
(* Goal: Rle (FtoRradix max) (IZR Z0) *)
rewrite <- (FzeroisZero radix b).
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
case H'; intros H'1.
apply (MonotoneMin b radix) with (p := FtoRradix (Fzero (- dExp b))) (q := r);
 auto.
(* Goal: Rlt (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) r *)
(* Goal: isMin b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
unfold FtoRradix in |- *; rewrite (FzeroisZero radix b); auto.
(* Goal: isMin b radix (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply (RoundedModeProjectorIdem (isMin b radix)); auto.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
apply MinRoundedModeP with (precision := precision); auto with float.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: isMax b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) max *)
apply FboundedFzero; auto.
(* Goal: Rle (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
replace (FtoR radix (Fzero (- dExp b))) with (FtoRradix min); auto with real.
(* Goal: @eq R (FtoRradix min) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply sym_eq; apply (ProjectMin b radix).
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: isMax b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) max *)
apply FboundedFzero; auto.
(* Goal: isMin b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) min *)
rewrite <- H'1 in H'0; rewrite <- (FzeroisZero radix b) in H'0; auto.
Qed.
 
Theorem RleRoundedR0 :
 forall (P : R -> float -> Prop) (p : float) (r : R),
 RoundedModeP b radix P -> P r p -> (0 <= r)%R -> (0 <= p)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (r : R) (_ : RoundedModeP b radix P) (_ : P r p) (_ : Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r), Rle (FtoRradix p) (Rmult (IZR radix) r) *)
intros P p r H' H'0 H'1.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5;
 case (H'4 r p); auto; intros H'6.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply RleMinR0 with (r := r); auto.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply Rle_trans with r; auto; apply isMax_inv1 with (1 := H'6).
Qed.
 
Theorem RleMaxR0 :
 forall (r : R) (max : float),
 (r <= 0)%R -> isMax b radix r max -> (max <= 0)%R.
(* Goal: forall (r : R) (max : float) (_ : Rle r (IZR Z0)) (_ : isMax b radix r max), Rle (FtoRradix max) (IZR Z0) *)
intros r max H' H'0.
(* Goal: Rle (FtoRradix max) (IZR Z0) *)
rewrite <- (FzeroisZero radix b).
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
case H'; intros H'1.
apply (MonotoneMax b radix) with (q := FtoRradix (Fzero (- dExp b))) (p := r);
 auto.
(* Goal: Rlt r (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: isMax b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
unfold FtoRradix in |- *; rewrite FzeroisZero; auto.
(* Goal: isMax b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply (RoundedModeProjectorIdem (isMax b radix)); auto.
(* Goal: RoundedModeP b radix (isMax b radix) *)
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply MaxRoundedModeP with (precision := precision); auto.
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: isMax b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) max *)
apply FboundedFzero; auto.
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
replace (FtoR radix (Fzero (- dExp b))) with (FtoRradix max); auto with real.
(* Goal: @eq R (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply sym_eq; apply (ProjectMax b radix).
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: isMax b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) max *)
apply FboundedFzero; auto.
(* Goal: isMax b radix (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) max *)
rewrite H'1 in H'0; rewrite <- (FzeroisZero radix b) in H'0; auto.
Qed.
 
Theorem RleRoundedLessR0 :
 forall (P : R -> float -> Prop) (p : float) (r : R),
 RoundedModeP b radix P -> P r p -> (r <= 0)%R -> (p <= 0)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (r : R) (_ : RoundedModeP b radix P) (_ : P r p) (_ : Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r), Rle (FtoRradix p) (Rmult (IZR radix) r) *)
intros P p r H' H'0 H'1.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5;
 case (H'4 r p); auto; intros H'6.
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
apply Rle_trans with r; auto; apply isMin_inv1 with (1 := H'6).
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
apply RleMaxR0 with (r := r); auto.
Qed.
 
Theorem PminPos :
 forall p min : float,
 (0 <= p)%R ->
 Fbounded b p ->
 isMin b radix (/ 2%nat * p) min ->
 exists c : float, Fbounded b c /\ c = (p - min)%R :>R.
(* Goal: forall (p min : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fbounded b p) (_ : isMin b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) min), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
intros p min H' H'0 H'1.
cut (min <= / 2%nat * p)%R;
 [ intros Rl1; Casec Rl1; intros Rl1
 | apply isMin_inv1 with (1 := H'1); auto ].
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
case (eqExpMax _ radixMoreThanOne b min p); auto.
(* Goal: Fbounded b max *)
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix max)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
case H'1; auto.
(* Goal: Rle (FtoR radix (Fabs min)) (FtoR radix p) *)
(* Goal: forall (x : float) (_ : and (Fbounded b x) (and (@eq R (FtoR radix x) (FtoR radix min)) (Z.le (Fexp x) (Fexp p)))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Fabs_correct; auto with arith.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Rabs_right; auto.
(* Goal: Rle (FtoR radix min) (FtoR radix p) *)
(* Goal: Rge (FtoR radix min) (IZR Z0) *)
(* Goal: forall (x : float) (_ : and (Fbounded b x) (and (@eq R (FtoR radix x) (FtoR radix min)) (Z.le (Fexp x) (Fexp p)))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Rle_trans with (/ 2%nat * p)%R; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_ne_r;
 auto with real.
(* Goal: Rge (FtoR radix min) (IZR Z0) *)
(* Goal: forall (x : float) (_ : and (Fbounded b x) (and (@eq R (FtoR radix x) (FtoR radix min)) (Z.le (Fexp x) (Fexp p)))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Rle_ge; apply RleMinR0 with (r := (/ 2%nat * p)%R); auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l;
 rewrite Rmult_0_r; auto with real.
intros min' H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6;
 clear H'4 H'2.
case (FboundNext _ radixMoreThanOne b precision) with (p := min');
 auto with arith; fold FtoRradix in |- *.
(* Goal: forall (x : float) (_ : and (Fbounded b x) (@eq R (FtoRradix x) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min'))))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
intros Smin H'2; elim H'2; intros H'4 H'7; clear H'2.
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
exists Smin; split; auto.
(* Goal: @eq R (FtoRradix Smin) (Rminus (FtoRradix p) (FtoRradix min)) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite H'7; auto.
(* Goal: @eq R (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min'))) (Rminus (FtoRradix p) (FtoRradix min)) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
unfold FtoRradix in |- *.
(* Goal: @eq R (FtoR radix (Float (Z.succ (Fnum min')) (Fexp min'))) (Rminus (FtoR radix p) (FtoR radix min)) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite <- H'5; auto.
replace (Float (Zsucc (Fnum min')) (Fexp min')) with
 (Float (Fnum (Fshift radix (Zabs_nat (Fexp p - Fexp min')) p) - Fnum min')
    (Fexp min')); auto.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min'))) (powerRZ (IZR radix) (Fexp min'))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite <- Z_R_minus.
rewrite (fun x y z : R => Rmult_comm (x - y) z); rewrite Rmult_minus_distr_l;
 repeat rewrite (fun x : Z => Rmult_comm (powerRZ radix x)).
(* Goal: @eq R (Rminus (Rmult (IZR (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min')))))) (powerRZ (IZR radix) (Fexp min'))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Rmult_IZR.
(* Goal: @eq R (Rminus (Rmult (Rmult (IZR (Fnum p)) (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min')))))) (powerRZ (IZR radix) (Fexp min'))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Zpower_nat_powerRZ_absolu; auto with zarith.
(* Goal: @eq R (Rminus (Rmult (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Z.sub (Fexp p) (Fexp min')))) (powerRZ (IZR radix) (Fexp min'))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Rmult_assoc.
(* Goal: @eq R (Rminus (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Z.sub (Fexp p) (Fexp min'))) (powerRZ (IZR radix) (Fexp min')))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite <- (powerRZ_add radix); auto with real zarith.
(* Goal: @eq R (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Z.add (Z.sub (Fexp p) (Fexp min')) (Fexp min')))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) (Rminus (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Fnum min')) (powerRZ (IZR radix) (Fexp min')))) *)
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Fexp p - Fexp min' + Fexp min')%Z with (Fexp p); [ auto | ring ].
(* Goal: @eq float (Float (Z.sub (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) (Fnum min')) (Fexp min')) (Float (Z.succ (Fnum min')) (Fexp min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply floatEq; auto; simpl in |- *.
(* Goal: @eq Z (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) (Z.succ (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_antisym.
(* Goal: Z.le (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) (Z.succ (Fnum min')) *)
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zlt_succ_le.
(* Goal: Z.lt (Fnum min') (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zplus_lt_reg_l with (p := Fnum min'); auto.
cut (forall x y : Z, (x + (y - x))%Z = y);
 [ intros tmp; rewrite tmp; clear tmp | intros; ring ].
replace (Fnum min' + Zsucc (Zsucc (Fnum min')))%Z with
 (2%nat * Zsucc (Fnum min'))%Z.
apply (Rlt_Float_Zlt radix) with (r := Fexp min'); auto;
 fold FtoRradix in |- *.
replace (FtoRradix (Float (2%nat * Zsucc (Fnum min')) (Fexp min'))) with
 (2%nat * Float (Zsucc (Fnum min')) (Fexp min'))%R.
(* Goal: Rlt (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min'))) (Rmult (INR (S (S O))) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min')))) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Z.add (Fnum min') (Z.succ (Z.succ (Fnum min')))) *)
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite <- H'7.
replace
 (Float (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p - Fexp min')))
    (Fexp min')) with (Fshift radix (Zabs_nat (Fexp p - Fexp min')) p).
(* Goal: Rlt (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
(* Goal: Rlt (Rmult (INR (S (S O))) (FtoR radix (Float (Fnum min') (Fexp min')))) (FtoR radix p) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Rmult_lt_reg_l with (r := (/ 2%nat)%R); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l;
 auto with real.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoR radix Smin) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Z.add (Fnum min') (Z.succ (Z.succ (Fnum min')))) *)
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
case (Rle_or_lt Smin (/ 2%nat * FtoR radix p)); auto.
(* Goal: forall _ : Rle (FtoRradix Smin) (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)), Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoR radix Smin) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Z.add (Fnum min') (Z.succ (Z.succ (Fnum min')))) *)
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
intros H'2; absurd (min < Smin)%R.
(* Goal: not (Rlt (FtoRradix min) (FtoR radix f)) *)
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
apply Rle_not_lt.
(* Goal: Fbounded b max *)
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix max)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
case H'1; auto.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoRradix Smin) (FtoRradix min) *)
(* Goal: Rlt (FtoRradix min) (FtoRradix Smin) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Z.succ (Fnum min')) (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Z.succ (Fnum min'))) (Z.add (Fnum min') (Z.succ (Z.succ (Fnum min')))) *)
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
intros H'8 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto.
(* Goal: @eq R (FtoR radix (Float (Z.succ (Fnum min')) (Fexp min'))) (Rminus (FtoR radix p) (FtoR radix min)) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite H'7; unfold FtoRradix in |- *; rewrite <- H'5; auto.
unfold FtoR in |- *; simpl in |- *; apply Rlt_monotony_exp;
 auto with real zarith.
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq float (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp min')))))) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Fexp p - Zabs_nat (Fexp p - Fexp min'))%Z with (Fexp min'); auto.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite inj_abs; auto.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
ring.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
auto with zarith.
replace (FtoRradix (Float (2%nat * Zsucc (Fnum min')) (Fexp min'))) with
 ((2%nat * Zsucc (Fnum min'))%Z * powerRZ radix (Fexp min'))%R.
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (Rmult (IZR (Z.mul (Z.of_nat (S (S O))) (Fnum min'))) (powerRZ (IZR radix) (Fexp min'))) *)
(* Goal: @eq R (Rmult (IZR (Z.mul (Z.of_nat (S (S O))) (Fnum min'))) (powerRZ (IZR radix) (Fexp min'))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Rmult_IZR; auto.
(* Goal: @eq R (powerRZ (IZR radix) e) (FtoRradix (Float (Z.of_nat (S O)) e)) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
simpl in |- *; auto.
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Z_of_nat 2) with (Zsucc (Zsucc 0)).
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
repeat rewrite <- Zmult_succ_l_reverse; unfold Zsucc in |- *; ring.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
simpl in |- *; auto.
(* Goal: Z.le (Z.succ (Fnum min')) (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zlt_le_succ; auto.
(* Goal: Z.lt (Fnum min') (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zplus_lt_reg_l with (p := Fnum min'); auto.
cut (forall x y : Z, (x + (y - x))%Z = y);
 [ intros tmp; rewrite tmp; clear tmp | intros; ring ].
(* Goal: Z.lt (Z.add (Fnum min') (Fnum min')) (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Fnum min' + Fnum min')%Z with (2%nat * Fnum min')%Z.
apply (Rlt_Float_Zlt radix) with (r := Fexp min'); auto;
 fold FtoRradix in |- *.
replace (FtoRradix (Float (2%nat * Fnum min') (Fexp min'))) with
 (2%nat * Float (Fnum min') (Fexp min'))%R.
replace
 (Float (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p - Fexp min')))
    (Fexp min')) with (Fshift radix (Zabs_nat (Fexp p - Fexp min')) p).
(* Goal: Rlt (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p)) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
(* Goal: Rlt (Rmult (INR (S (S O))) (FtoR radix (Float (Fnum min') (Fexp min')))) (FtoR radix p) *)
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Rmult_lt_reg_l with (r := (/ 2%nat)%R); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l;
 auto with real.
replace (FtoR radix (Float (Fnum min') (Fexp min'))) with (FtoR radix min);
 auto.
(* Goal: @eq float (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))) p) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq float (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp min')))))) (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Fexp p - Zabs_nat (Fexp p - Fexp min'))%Z with (Fexp min'); auto.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite inj_abs; auto.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
ring.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
auto with zarith.
replace (FtoRradix (Float (2%nat * Fnum min') (Fexp min'))) with
 ((2%nat * Fnum min')%Z * powerRZ radix (Fexp min'))%R.
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (Rmult (IZR (Z.mul (Z.of_nat (S (S O))) (Fnum min'))) (powerRZ (IZR radix) (Fexp min'))) *)
(* Goal: @eq R (Rmult (IZR (Z.mul (Z.of_nat (S (S O))) (Fnum min'))) (powerRZ (IZR radix) (Fexp min'))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite Rmult_IZR; auto.
(* Goal: @eq R (powerRZ (IZR radix) e) (FtoRradix (Float (Z.of_nat (S O)) e)) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
simpl in |- *; auto.
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
replace (Z_of_nat 2) with (Zsucc (Zsucc 0)).
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
repeat rewrite <- Zmult_succ_l_reverse; unfold Zsucc in |- *; ring.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
simpl in |- *; auto.
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
exists min; split; auto.
(* Goal: Fbounded b max *)
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix max)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
case H'1; auto.
(* Goal: @eq R (FtoRradix min) (Rminus (FtoRradix p) (FtoRradix min)) *)
rewrite Rl1.
pattern (FtoRradix p) at 2 in |- *;
 replace (FtoRradix p) with (2%nat * (/ 2%nat * p))%R.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; ring.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_ne_r;
 auto with real.
Qed.
 
Theorem div2IsBetweenPos :
 forall p min max : float,
 (0 <= p)%R ->
 Fbounded b p ->
 isMin b radix (/ 2%nat * p) min ->
 isMax b radix (/ 2%nat * p) max -> p = (min + max)%R :>R.
(* Goal: forall (p min max : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fbounded b p) (_ : isMin b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) min) (_ : isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) max), @eq R (FtoRradix p) (Rplus (FtoRradix min) (FtoRradix max)) *)
intros p min max P H' H'0 H'1; apply Rle_antisym.
(* Goal: Rle (FtoRradix p) (Rplus (FtoRradix min) (FtoRradix max)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rplus_le_reg_l with (r := (- max)%R).
(* Goal: Rle (Rplus (Ropp (FtoRradix max)) (FtoRradix p)) (Rplus (Ropp (FtoRradix max)) (Rplus (FtoRradix min) (FtoRradix max))) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
replace (- max + p)%R with (p - max)%R; [ idtac | ring ].
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix max)) (Rplus (Ropp (FtoRradix max)) (Rplus (FtoRradix min) (FtoRradix max))) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
replace (- max + (min + max))%R with (FtoRradix min); [ idtac | ring ].
(* Goal: Rle (Rminus (FtoRradix p) (FtoRradix max)) (FtoRradix min) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
rewrite <- (Fminus_correct radix); auto with arith.
(* Goal: Rle (FtoRradix max) (FtoR radix f) *)
(* Goal: Rlt (FtoR radix f) (FtoRradix max) *)
case H'0.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoR radix (Fminus radix p max)) (FtoRradix min) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3; auto.
(* Goal: Fbounded b (Fminus radix p max) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Sterbenz; auto.
(* Goal: Fbounded b max *)
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix max)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
case H'1; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix max)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rle_trans with (FtoRradix max); auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l;
 auto with real.
(* Goal: Rle (FtoR radix max) (Rmult (INR (S (S O))) (FtoRradix max)) *)
(* Goal: Rle (FtoRradix max) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rledouble; auto.
(* Goal: Rle (IZR Z0) (FtoRradix max) *)
(* Goal: Rle (FtoRradix max) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rle_trans with (FtoRradix min); auto.
(* Goal: Rle (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix min) (FtoRradix max) *)
(* Goal: Rle (FtoRradix max) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply RleMinR0 with (r := (/ 2%nat * p)%R); auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l;
 rewrite Rmult_0_r; auto with real.
(* Goal: Rle (FtoRradix min) (FtoRradix max) *)
(* Goal: Rle (FtoRradix max) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rle_trans with (/ 2%nat * p)%R; auto; apply isMax_inv1 with (1 := H'1).
(* Goal: Rle (FtoRradix max) (FtoRradix x) *)
case H'1.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
intros H'3 H'6; elim H'6; intros H'7 H'8; apply H'8; clear H'6; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix p) *)
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := INR 2); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l;
 auto with real.
(* Goal: Rle (FtoR radix p) (Rmult (INR (S (S O))) (FtoR radix max)) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rmult_le_reg_l with (r := (/ 2%nat)%R); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l;
 auto with real.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoR radix max) *)
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply isMax_inv1 with (1 := H'1).
(* Goal: Rle (FtoR radix (Fminus radix p max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
rewrite Fminus_correct; auto with arith.
(* Goal: Rle (Rminus (FtoR radix p) (FtoR radix max)) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rplus_le_reg_l with (r := FtoR radix max).
replace (FtoR radix max + (FtoR radix p - FtoR radix max))%R with
 (FtoR radix p); [ idtac | ring ].
(* Goal: Rle (Rplus (FtoRradix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoRradix p) *)
apply Rplus_le_reg_l with (r := (- (/ 2%nat * p))%R).
(* Goal: Rle (Rplus (Ropp (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoR radix p)) (Rplus (Ropp (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (Rplus (FtoR radix max) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)))) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
replace (- (/ 2%nat * p) + FtoR radix p)%R with (/ 2%nat * p)%R.
replace (- (/ 2%nat * p) + (FtoR radix max + / 2%nat * p))%R with
 (FtoR radix max); [ apply isMax_inv1 with (1 := H'1) | ring ].
(* Goal: @eq R (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (Rplus (Ropp (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoR radix p)) *)
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
replace (FtoR radix p) with (2%nat * (/ 2%nat * p))%R.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; ring.
(* Goal: @eq R (Rmult (INR (S (S O))) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoRradix p) *)
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (FtoRradix p) *)
apply Rplus_le_reg_l with (r := (- min)%R).
(* Goal: Rle (Rplus (Ropp (FtoRradix min)) (Rplus (FtoRradix min) (FtoRradix max))) (Rplus (Ropp (FtoRradix min)) (FtoRradix p)) *)
replace (- min + p)%R with (p - min)%R; [ idtac | ring ].
(* Goal: Rle (Rplus (Ropp (FtoRradix min)) (Rplus (FtoRradix min) (FtoRradix max))) (Rminus (FtoRradix p) (FtoRradix min)) *)
replace (- min + (min + max))%R with (FtoRradix max); [ idtac | ring ].
(* Goal: Rle (FtoRradix max) (Rminus (FtoRradix p) (FtoRradix min)) *)
case (PminPos p min); auto.
(* Goal: forall (x : float) (_ : and (Fbounded b x) (@eq R (FtoRradix x) (Rminus (FtoRradix p) (FtoRradix min)))), Rle (FtoRradix max) (Rminus (FtoRradix p) (FtoRradix min)) *)
intros x H'2; elim H'2; intros H'3 H'4; elim H'4; clear H'2.
(* Goal: Rle (FtoRradix max) (FtoRradix x) *)
case H'1.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix x) *)
intros H'2 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (FtoR radix x) *)
unfold FtoRradix in H'4; rewrite H'4; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) (Rminus (FtoR radix p) (FtoR radix min)) *)
fold FtoRradix in |- *; apply Rplus_le_reg_l with (r := FtoRradix min).
(* Goal: Rle (Rplus (FtoRradix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (Rplus (FtoRradix min) (Rminus (FtoRradix p) (FtoRradix min))) *)
replace (min + (p - min))%R with (FtoRradix p); [ idtac | ring ].
(* Goal: Rle (Rplus (FtoRradix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoRradix p) *)
apply Rplus_le_reg_l with (r := (- (/ 2%nat * p))%R).
(* Goal: Rle (Rplus (Ropp (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (Rplus (FtoRradix min) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)))) (Rplus (Ropp (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoRradix p)) *)
replace (- (/ 2%nat * p) + p)%R with (/ 2%nat * p)%R.
replace (- (/ 2%nat * p) + (min + / 2%nat * p))%R with (FtoRradix min);
 [ apply isMin_inv1 with (1 := H'0) | ring ].
pattern (FtoRradix p) at 3 in |- *;
 replace (FtoRradix p) with (2%nat * (/ 2%nat * p))%R.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; ring.
(* Goal: @eq R (Rmult (INR (S (S O))) (Rmult (Rinv (INR (S (S O)))) (FtoRradix p))) (FtoRradix p) *)
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real.
Qed.
 
Theorem div2IsBetween :
 forall p min max : float,
 Fbounded b p ->
 isMin b radix (/ 2%nat * p) min ->
 isMax b radix (/ 2%nat * p) max -> p = (min + max)%R :>R.
(* Goal: forall (p min max : float) (_ : Fbounded b p) (_ : isMin b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) min) (_ : isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix p)) max), @eq R (FtoRradix p) (Rplus (FtoRradix min) (FtoRradix max)) *)
intros p min max H' H'0 H'1; case (Rle_or_lt 0 p); intros H'2.
(* Goal: @eq R (FtoRradix p) (Rplus (FtoRradix min) (FtoRradix max)) *)
(* Goal: @eq R (FtoRradix p) (Rplus (FtoRradix min) (FtoRradix max)) *)
apply div2IsBetweenPos; auto.
cut (forall x y : R, (- x)%R = (- y)%R -> x = y);
 [ intros H'3; apply H'3; clear H'3 | idtac ].
(* Goal: @eq R (Ropp (FtoRradix p)) (Ropp (Rplus (FtoRradix min) (FtoRradix max))) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
replace (- (min + max))%R with (- max + - min)%R; [ idtac | ring ].
(* Goal: @eq R (Ropp (FtoRradix p)) (Rplus (Ropp (FtoRradix max)) (Ropp (FtoRradix min))) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
repeat rewrite <- (Fopp_correct radix); auto with float.
(* Goal: @eq R (FtoR radix (Fopp p)) (Rplus (FtoR radix (Fopp max)) (FtoR radix (Fopp min))) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
apply div2IsBetweenPos; auto with float.
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp p)) *)
(* Goal: isMin b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp max) *)
(* Goal: isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp min) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
rewrite (Fopp_correct radix); auto.
(* Goal: Rle (IZR Z0) (Ropp (FtoR radix p)) *)
(* Goal: isMin b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp max) *)
(* Goal: isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp min) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
replace 0%R with (-0)%R; try apply Rlt_le; auto with real.
(* Goal: isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp min) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
replace (/ 2%nat * Fopp p)%R with (- (/ 2%nat * p))%R; auto with float.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite (Fopp_correct radix); auto; fold FtoRradix; ring.
(* Goal: isMax b radix (Rmult (Rinv (INR (S (S O)))) (FtoRradix (Fopp p))) (Fopp min) *)
(* Goal: forall (x y : R) (_ : @eq R (Ropp x) (Ropp y)), @eq R x y *)
replace (/ 2%nat * Fopp p)%R with (- (/ 2%nat * p))%R; auto with float.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite (Fopp_correct radix); auto; fold FtoRradix;ring.
intros x y H'3; rewrite <- (Ropp_involutive x);
 rewrite <- (Ropp_involutive y); rewrite H'3; auto.
Qed.
 
Theorem RoundedModeMultAbs :
 forall P,
 RoundedModeP b radix P ->
 forall (r : R) (q q' : float),
 P r q ->
 Fbounded b q' -> (Rabs r <= radix * q')%R -> (Rabs q <= radix * q')%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (r : R) (q q' : float) (_ : P r q) (_ : Fbounded b q') (_ : Rle (Rabs r) (Rmult (IZR radix) (FtoRradix q'))), Rle (Rabs (FtoRradix q)) (Rmult (IZR radix) (FtoRradix q')) *)
intros P H' r q q' H'0 H'1 H'2.
(* Goal: Rle (Rabs (FtoRradix q)) (Rmult (IZR radix) (FtoRradix q')) *)
case (Rle_or_lt 0 r); intros Rl0.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Rabs_right; auto.
(* Goal: Rle (FtoRradix q) (Rmult (IZR radix) (FtoRradix q')) *)
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix q)) (Rmult (IZR radix) (FtoRradix q')) *)
apply RoundedModeMult with (P := P) (r := r); auto.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r *)
(* Goal: Rge (FtoRradix p) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
rewrite <- (Rabs_right r); auto with real.
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix q)) (Rmult (IZR radix) (FtoRradix q')) *)
apply Rle_ge; apply RleRoundedR0 with (P := P) (r := r); auto.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Faux.Rabsolu_left1; auto.
replace (radix * q')%R with (- (radix * - q'))%R;
 [ apply Ropp_le_contravar | ring ].
(* Goal: Rle (Rmult (IZR radix) (Ropp (FtoRradix q'))) (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Fopp_correct radix).
(* Goal: Rle (Rmult (IZR radix) (FtoR radix (Fopp q'))) (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
apply RoundedModeMultLess with (P := P) (r := r); auto.
(* Goal: Fbounded b (Fopp q') *)
(* Goal: Rle (Rmult (IZR radix) (FtoRradix (Fopp q'))) r *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp f1)) *)
(* Goal: isMin b radix (FtoRradix (Fopp f1)) (Fopp f2) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (Rmult (IZR radix) (Ropp (FtoR radix q'))) r *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Ropp_involutive r).
replace (radix * - FtoR radix q')%R with (- (radix * q'))%R;
 [ apply Ropp_le_contravar | fold FtoRradix;ring ]; auto.
(* Goal: Rle (Ropp r) (Rmult (IZR radix) (FtoRradix q')) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Faux.Rabsolu_left1 r); auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
apply RleRoundedLessR0 with (P := P) (r := r); auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
Qed.
 
Theorem isMinComp :
 forall (r1 r2 : R) (min max : float),
 isMin b radix r1 min ->
 isMax b radix r1 max -> (min < r2)%R -> (r2 < max)%R -> isMin b radix r2 min.
(* Goal: forall (r1 r2 : R) (min max : float) (_ : isMin b radix r1 min) (_ : isMax b radix r1 max) (_ : Rlt (FtoRradix min) r2) (_ : Rlt r2 (FtoRradix max)), isMax b radix r2 max *)
intros r1 r2 min max H' H'0 H'1 H'2; split.
(* Goal: Rle (FtoR radix f) (FtoR radix min) *)
case H'; auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
split.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f) *)
intros f H'3 H'4.
(* Goal: Rle (FtoR radix f) (FtoR radix min) *)
case H'; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r1 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r1 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoR radix max) (FtoR radix f) *)
intros H'5 H'6; elim H'6; intros H'7 H'8; apply H'8; clear H'6; auto.
(* Goal: Rle (FtoR radix f) r1 *)
case (Rle_or_lt (FtoR radix f) r1); auto; intros C1.
(* Goal: Rle (FtoR radix f) r1 *)
absurd (FtoR radix f < max)%R.
(* Goal: not (Rlt (FtoRradix min) (FtoR radix f)) *)
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
apply Rle_not_lt.
(* Goal: Rle (FtoRradix max) (FtoR radix f) *)
(* Goal: Rlt (FtoR radix f) (FtoRradix max) *)
case H'0.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) r1) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) r1), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoR radix f) (FtoRradix min) *)
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
intros H'6 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rlt (FtoR radix f) (FtoRradix max) *)
apply Rle_lt_trans with (2 := H'2); auto.
Qed.
 
Theorem isMaxComp :
 forall (r1 r2 : R) (min max : float),
 isMin b radix r1 min ->
 isMax b radix r1 max -> (min < r2)%R -> (r2 < max)%R -> isMax b radix r2 max.
(* Goal: forall (r1 r2 : R) (min max : float) (_ : isMin b radix r1 min) (_ : isMax b radix r1 max) (_ : Rlt (FtoRradix min) r2) (_ : Rlt r2 (FtoRradix max)), isMax b radix r2 max *)
intros r1 r2 min max H' H'0 H'1 H'2; split.
(* Goal: Rle (FtoR radix max) (FtoR radix f) *)
case H'0; auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
split.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f) *)
intros f H'3 H'4.
(* Goal: Rle (FtoR radix max) (FtoR radix f) *)
case H'0; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r1 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r1 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoR radix max) (FtoR radix f) *)
intros H'5 H'6; elim H'6; intros H'7 H'8; apply H'8; clear H'6; auto.
(* Goal: Rle r1 (FtoR radix f) *)
case (Rle_or_lt r1 (FtoR radix f)); auto; intros C1.
(* Goal: Rle r1 (FtoR radix f) *)
absurd (min < FtoR radix f)%R.
(* Goal: not (Rlt (FtoRradix min) (FtoR radix f)) *)
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
apply Rle_not_lt.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) r1) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) r1), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoR radix f) (FtoRradix min) *)
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
intros H'6 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rlt (FtoRradix min) (FtoR radix f) *)
apply Rlt_le_trans with (1 := H'1); auto.
Qed.
 
Theorem roundedModeLessMult :
 forall (P : R -> float -> Prop) (p : float) (r : R),
 RoundedModeP b radix P ->
 P r p -> (Float 1%nat (- dExp b) <= r)%R -> (p <= radix * r)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (r : R) (_ : RoundedModeP b radix P) (_ : P r p) (_ : Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r), Rle (FtoRradix p) (Rmult (IZR radix) r) *)
intros P p r H' H'0 H'1.
cut (0 < Float 1%nat (- dExp b))%R;
 [ intros Rl0
 | unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_l;
    auto with real arith ].
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
cut (0 < r)%R; [ intros Rl1 | apply Rlt_le_trans with (1 := Rl0) ]; auto.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
cut (0 <= r)%R; [ intros Rl2 | apply Rlt_le; auto ].
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5;
 case (H'4 r p); auto; intros H'6.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
apply Rle_trans with r; auto with real.
(* Goal: Rle (FtoRradix p) r *)
(* Goal: Rle r (Rmult (IZR radix) r) *)
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
apply isMin_inv1 with (1 := H'6).
rewrite Rmult_comm; pattern r at 1 in |- *; replace r with (r * 1%nat)%R;
 [ apply Rmult_le_compat_l | simpl; ring ]; auto with real arith.
case (MinEx b radix precision) with (r := r); auto with arith;
 intros min Hmin.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
cut (Fbounded b (Float (Fnum min) (Zsucc (Fexp min)))); [ intros F2 | idtac ].
cut (FtoRradix (Float (Fnum min) (Zsucc (Fexp min))) = (radix * min)%R :>R);
 [ intros F2Eq | idtac ].
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rle_trans with (FtoRradix (Float (Fnum min) (Zsucc (Fexp min)))).
(* Goal: Rle (FtoRradix p) (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
case H'6.
(* Goal: forall (_ : Fbounded b p) (_ : and (Rle r (FtoR radix p)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix p) (FtoR radix f))), Rle (FtoRradix p) (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'7 H'8; elim H'8; intros H'9 H'10; apply H'10; clear H'8; auto.
(* Goal: Rle r (FtoR radix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
case (Rle_or_lt r (Float (Fnum min) (Zsucc (Fexp min)))); auto; intros Rlt0.
(* Goal: Rle r (FtoR radix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
absurd (Float (Fnum min) (Zsucc (Fexp min)) <= min)%R.
(* Goal: not (Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min)) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rgt_not_le.
(* Goal: Rgt (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite F2Eq; auto with real.
(* Goal: Rgt (Rmult (IZR radix) (FtoRradix min)) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite Rmult_comm.
pattern (FtoRradix min) at 2 in |- *;
 replace (FtoRradix min) with (min * 1%nat)%R; auto with real.
(* Goal: Rgt (Rmult (FtoRradix min) (IZR radix)) (Rmult (FtoRradix min) (INR (S O))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
red in |- *; apply Rmult_lt_compat_l; auto with real arith.
(* Goal: Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
case (RleMinR0 r min); auto.
(* Goal: Rle (FtoRradix max) (FtoRradix x) *)
intros H'8; case H'1.
(* Goal: forall _ : Rlt (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: forall _ : @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'11; absurd (Float 1%nat (- dExp b) <= min)%R.
(* Goal: not (Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min)) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
(* Goal: forall _ : @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rgt_not_le; auto.
(* Goal: Rgt (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
(* Goal: forall _ : @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite <- H'8; auto.
apply
 (MonotoneMin b radix)
  with (p := FtoRradix (Float 1%nat (- dExp b))) (q := r); 
 auto.
(* Goal: isMin b radix (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply (RoundedModeProjectorIdem (isMin b radix)); auto.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply MinRoundedModeP with (precision := precision); auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
repeat split.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 auto with zarith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
(* Goal: forall _ : @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'11; absurd (min = Float 1%nat (- dExp b) :>R).
(* Goal: not (@eq R (FtoRradix min) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))))) *)
(* Goal: @eq R (FtoRradix min) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite <- H'8.
(* Goal: not (@eq R (IZR Z0) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))))) *)
(* Goal: @eq R (FtoRradix min) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rlt_dichotomy_converse; left; auto.
(* Goal: @eq R (FtoRradix min) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply (MinUniqueP b radix r); auto.
(* Goal: isMin b radix r (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite <- H'11.
(* Goal: isMin b radix (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply (RoundedModeProjectorIdem (isMin b radix)); auto.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply MinRoundedModeP with (precision := precision); auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
repeat split.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 auto with zarith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
case Hmin.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) r), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'8 H'11; elim H'11; intros H'12 H'13; apply H'13; clear H'11; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite F2Eq.
(* Goal: Rle (Rmult (IZR radix) (FtoRradix min)) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rmult_le_compat_l; auto with real arith.
(* Goal: Rle (IZR Z0) (INR n) *)
replace 0%R with (INR 0); auto with real arith.
(* Goal: Rle (FtoRradix min) r *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply isMin_inv1 with (1 := Hmin).
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite powerRZ_Zs; auto with real zarith; ring.
cut (Fbounded b min);
 [ unfold Fbounded in |- *; intros Fb0 | case Hmin; auto ].
(* Goal: and (Z.lt (Z.abs (Fnum (Float (Fnum min) (Z.succ (Fexp min))))) (Zpos (vNum b))) (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Float (Fnum min) (Z.succ (Fexp min))))) *)
elim Fb0; intros H H0; auto.
(* Goal: and (Z.lt (Z.abs (Fnum (Float (Fnum min) (Z.succ (Fexp min))))) (Zpos (vNum b))) (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Float (Fnum min) (Z.succ (Fexp min))))) *)
repeat (split; simpl in |- *); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_trans with (Fexp min); auto with zarith.
Qed.
 
Theorem roundedModeMoreMult :
 forall (P : R -> float -> Prop) (p : float) (r : R),
 RoundedModeP b radix P ->
 P r p -> (r <= Float (- 1%nat) (- dExp b))%R -> (radix * r <= p)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (r : R) (_ : RoundedModeP b radix P) (_ : P r p) (_ : Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r), Rle (FtoRradix p) (Rmult (IZR radix) r) *)
intros P p r H' H'0 H'1.
cut (Float (- 1%nat) (- dExp b) < 0)%R;
 [ intros Rl0
 | unfold FtoRradix, FtoR in |- *; simpl in |- *; unfold IZR at 1; rewrite Ropp_mult_distr_l_reverse;
   rewrite Rmult_1_l;
    auto with real arith ].
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
2: replace 0%R with (-0)%R; auto with real arith; ring.
cut (r < 0)%R; [ intros Rl1 | apply Rle_lt_trans with (2 := Rl0) ]; auto.
cut (r <= 0)%R; [ intros Rl2 | apply Rlt_le; auto ].
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
case H'.
intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5;
 case (H'4 r p); auto; intros H'6.
case (MaxEx b radix precision) with (r := r); auto with arith;
 intros max Hmax.
cut (Fbounded b (Float (Fnum max) (Zsucc (Fexp max)))); [ intros F2 | idtac ].
cut (FtoRradix (Float (Fnum max) (Zsucc (Fexp max))) = (radix * max)%R :>R);
 [ intros F2Eq | idtac ].
apply Rle_trans with (FtoRradix (Float (Fnum max) (Zsucc (Fexp max)))).
(* Goal: Rgt (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite F2Eq; auto with real.
(* Goal: Rle (Rmult (IZR radix) (FtoRradix min)) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rmult_le_compat_l; auto with real arith.
(* Goal: Rle (IZR Z0) (INR n) *)
replace 0%R with (INR 0); auto with real arith.
apply isMax_inv1 with (1 := Hmax); auto.
(* Goal: Rle (FtoRradix p) (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
case H'6.
(* Goal: forall (_ : Fbounded b p) (_ : and (Rle r (FtoR radix p)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix p) (FtoR radix f))), Rle (FtoRradix p) (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'7 H'8; elim H'8; intros H'9 H'10; apply H'10; clear H'8; auto.
case (Rle_or_lt (Float (Fnum max) (Zsucc (Fexp max))) r); auto; intros Rlt0.
absurd (max <= Float (Fnum max) (Zsucc (Fexp max)))%R.
(* Goal: not (Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min)) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rgt_not_le.
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
rewrite F2Eq.
replace (radix * max)%R with (- (- max * radix))%R; [ idtac | ring ].
pattern (FtoRradix max) at 1 in |- *;
 replace (FtoRradix max) with (- (- max * 1%nat))%R;
 [ idtac | simpl in |- *; ring ].
apply Ropp_lt_gt_contravar; apply Rmult_lt_compat_l; auto with real.
replace 0%R with (-0)%R; [ apply Ropp_lt_contravar | ring ].
case (RleMaxR0 r max); auto.
(* Goal: Rle (FtoRradix max) (FtoRradix x) *)
intros H'8; case H'1.
intros H'11; absurd (max <= Float (- 1%nat) (- dExp b))%R.
(* Goal: not (Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min)) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (FtoRradix min) *)
(* Goal: forall _ : @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r, Rlt (IZR Z0) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rgt_not_le; auto.
rewrite H'8; auto.
apply
 (MonotoneMax b radix)
  with (q := FtoRradix (Float (- 1%nat) (- dExp b))) (p := r); 
 auto.
(* Goal: isMax b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply (RoundedModeProjectorIdem (isMax b radix)); auto.
(* Goal: RoundedModeP b radix (isMax b radix) *)
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply MaxRoundedModeP with (precision := precision); auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
repeat split.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 auto with zarith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
intros H'11; absurd (Float (- 1%nat) (- dExp b) = max :>R).
rewrite H'8; auto.
(* Goal: not (@eq R (IZR Z0) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))))) *)
(* Goal: @eq R (FtoRradix min) (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rlt_dichotomy_converse; left; auto.
apply (MaxUniqueP b radix r); auto.
rewrite H'11.
(* Goal: isMax b radix (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply (RoundedModeProjectorIdem (isMax b radix)); auto.
(* Goal: RoundedModeP b radix (isMax b radix) *)
(* Goal: Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix max) (FtoR radix (Fzero (Z.opp (Z.of_N (dExp b))))) *)
apply MaxRoundedModeP with (precision := precision); auto.
(* Goal: and (Rle r2 (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r2 (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f)) *)
repeat split.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 auto with zarith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
simpl in |- *; auto with zarith.
case Hmax.
(* Goal: forall (_ : Fbounded b min) (_ : and (Rle (FtoR radix min) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoR radix f) r), Rle (FtoR radix f) (FtoR radix min))), Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
intros H'8 H'11; elim H'11; intros H'12 H'13; apply H'13; clear H'11; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite powerRZ_Zs; auto with real zarith; ring.
cut (Fbounded b max);
 [ unfold Fbounded in |- *; intros Fb0 | case Hmax; auto ].
(* Goal: and (Z.lt (Z.abs (Fnum (Float (Fnum min) (Z.succ (Fexp min))))) (Zpos (vNum b))) (Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Float (Fnum min) (Z.succ (Fexp min))))) *)
elim Fb0; intros H H0; repeat (split; simpl in |- *); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_trans with (Fexp max); auto with zarith.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
apply Rle_trans with r; auto with real.
pattern r at 2 in |- *; replace r with (- (- r * 1%nat))%R; [ idtac | simpl; ring ].
replace (radix * r)%R with (- (- r * radix))%R; [ idtac | ring ].
(* Goal: Rle (Rmult (IZR radix) (FtoRradix min)) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Ropp_le_contravar; apply Rmult_le_compat_l; auto with real arith.
replace 0%R with (-0)%R; auto with real arith.
apply isMax_inv1 with (1 := H'6).
Qed.
 
Theorem roundedModeAbsMult :
 forall (P : R -> float -> Prop) (p : float) (r : R),
 RoundedModeP b radix P ->
 P r p ->
 (Float 1%nat (- dExp b) <= Rabs r)%R -> (Rabs p <= radix * Rabs r)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : float) (r : R) (_ : RoundedModeP b radix P) (_ : P r p) (_ : Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Rabs r)), Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
intros P p r H' H'0 H'1; case (Rle_or_lt 0 r); intros H'2.
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle (FtoRradix p) (Rmult (IZR radix) r) *)
(* Goal: Rge (FtoRradix p) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
apply roundedModeLessMult with (P := P); auto.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) r *)
(* Goal: Rge (FtoRradix p) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
rewrite <- (Rabs_right r); auto with real.
(* Goal: Rge (FtoRradix p) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR radix) (Rabs r)) *)
apply Rle_ge; apply (RleRoundedR0 P) with (r := r); auto.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
repeat rewrite Faux.Rabsolu_left1; auto.
replace (radix * - r)%R with (- (radix * r))%R;
 [ apply Ropp_le_contravar | ring ].
(* Goal: Rle (Rmult (IZR radix) r) (FtoRradix p) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
apply roundedModeMoreMult with (P := P); auto.
(* Goal: Rle (Ropp r) (Rmult (IZR radix) (FtoRradix q')) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Ropp_involutive r); rewrite <- (Faux.Rabsolu_left1 r); auto.
(* Goal: Rle (Ropp (Rabs r)) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
replace (Float (- 1%nat) (- dExp b)) with (Fopp (Float 1%nat (- dExp b))).
(* Goal: Rle (Ropp (Rabs r)) (FtoRradix (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))))) *)
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
simpl in |- *; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
apply (RleRoundedLessR0 P) with (r := r); auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
Qed.
 
Theorem RleBoundRoundl :
 forall P,
 RoundedModeP b radix P ->
 forall (p q : float) (r : R),
 Fbounded b p -> (p <= r)%R -> P r q -> (p <= q)%R.
(* Goal: forall _ : @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros P H' p q r H'0 H'1 H'2; case H'1; intros H'3.
cut (MonotoneP radix P);
 [ intros Mn | apply RoundedModeP_inv4 with (1 := H'); auto ].
apply (Mn p r); auto.
(* Goal: P (FtoRradix p) p *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply RoundedModeProjectorIdem with (P := P); auto.
rewrite RoundedModeProjectorIdemEq with (P := P) (p := p) (q := q);
 auto with real.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ].
(* Goal: P (FtoR radix p) q *)
apply (Cp r p q); auto.
(* Goal: Fbounded b q *)
apply RoundedModeBounded with (P := P) (r := r); auto.
Qed.
 
Theorem RleBoundRoundr :
 forall P,
 RoundedModeP b radix P ->
 forall (p q : float) (r : R),
 Fbounded b p -> (r <= p)%R -> P r q -> (q <= p)%R.
(* Goal: forall _ : @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) r, Rle (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Fnum q') (Z.add (Fexp q') (Z.of_nat (S O))))) (Rmult (IZR radix) (FtoRradix q')) *)
intros P H' p q r H'0 H'1 H'2; case H'1; intros H'3.
cut (MonotoneP radix P);
 [ intros Mn | apply RoundedModeP_inv4 with (1 := H'); auto ].
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply (Mn r p); auto.
(* Goal: P (FtoRradix p) p *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply RoundedModeProjectorIdem with (P := P); auto.
rewrite RoundedModeProjectorIdemEq with (P := P) (p := p) (q := q);
 auto with real.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ].
(* Goal: P (FtoR radix p) q *)
apply (Cp r p q); auto.
(* Goal: Fbounded b q *)
apply RoundedModeBounded with (P := P) (r := r); auto.
Qed.
 
Theorem RoundAbsMonotoner :
 forall (P : R -> float -> Prop) (p : R) (q r : float),
 RoundedModeP b radix P ->
 Fbounded b r -> P p q -> (Rabs p <= r)%R -> (Rabs q <= r)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : R) (q r : float) (_ : RoundedModeP b radix P) (_ : Fbounded b r) (_ : P p q) (_ : Rle (FtoRradix r) (Rabs p)), Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
intros P p q r H' H'0 H'1 H'2.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
case (Rle_or_lt 0 p); intros Rl1.
(* Goal: Rle (Rabs (FtoRradix q)) (FtoRradix r) *)
(* Goal: Rle (Rabs (FtoRradix q)) (FtoRradix r) *)
rewrite Rabs_right; auto with real.
(* Goal: Rle (FtoRradix q) (FtoRradix r) *)
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (Rabs (FtoRradix q)) (FtoRradix r) *)
apply RleBoundRoundr with (P := P) (r := p); auto with real.
(* Goal: Rle (FtoRradix r) p *)
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite <- (Rabs_right p); auto with real.
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
apply Rle_ge; apply RleRoundedR0 with (P := P) (r := p); auto.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Faux.Rabsolu_left1; auto.
(* Goal: Rle (FtoRradix r) (Ropp (FtoRradix q)) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Ropp_involutive r); apply Ropp_le_contravar.
(* Goal: Rle (FtoRradix q) (Ropp (FtoRradix r)) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Fopp_correct radix); auto.
(* Goal: Rle (FtoR radix (Fopp r)) (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
apply RleBoundRoundl with (P := P) (r := p); auto with float.
rewrite (Fopp_correct radix); rewrite <- (Ropp_involutive p);
 rewrite <- (Faux.Rabsolu_left1 p); auto with real; 
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
 apply Rlt_le; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply RleRoundedLessR0 with (P := P) (r := p); auto; apply Rlt_le; auto.
Qed.
 
Theorem RoundAbsMonotonel :
 forall (P : R -> float -> Prop) (p : R) (q r : float),
 RoundedModeP b radix P ->
 Fbounded b r -> P p q -> (r <= Rabs p)%R -> (r <= Rabs q)%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p : R) (q r : float) (_ : RoundedModeP b radix P) (_ : Fbounded b r) (_ : P p q) (_ : Rle (FtoRradix r) (Rabs p)), Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
intros P p q r H' H'0 H'1 H'2.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
case (Rle_or_lt 0 p); intros Rl1.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Rabs_right; auto.
(* Goal: Rle (FtoRradix r) (FtoRradix q) *)
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
apply RleBoundRoundl with (P := P) (r := p); auto.
(* Goal: Rle (FtoRradix r) p *)
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite <- (Rabs_right p); auto with real.
(* Goal: Rge (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
apply Rle_ge; apply RleRoundedR0 with (P := P) (r := p); auto.
(* Goal: Rle (FtoRradix r) (Rabs (FtoRradix q)) *)
rewrite Faux.Rabsolu_left1; auto.
(* Goal: Rle (FtoRradix r) (Ropp (FtoRradix q)) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Ropp_involutive r); apply Ropp_le_contravar.
(* Goal: Rle (FtoRradix q) (Ropp (FtoRradix r)) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
rewrite <- (Fopp_correct radix); auto.
(* Goal: Rle (FtoRradix q) (FtoR radix (Fopp r)) *)
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
apply RleBoundRoundr with (P := P) (r := p); auto with float.
rewrite (Fopp_correct radix); rewrite <- (Ropp_involutive p);
 rewrite <- (Faux.Rabsolu_left1 p); auto with real; 
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
 apply Rlt_le; auto.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply RleRoundedLessR0 with (P := P) (r := p); auto; apply Rlt_le; auto.
Qed.
(* Rounded of natural numbers are natural *)
 
Theorem ZroundZ :
 forall (P : R -> float -> Prop) (z : Z) (p : float),
 RoundedModeP b radix P -> P z p -> exists z' : Z, p = z' :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (z : Z) (p : float) (_ : RoundedModeP b radix P) (_ : P (IZR z) p), @ex Z (fun z' : Z => @eq R (FtoRradix p) (IZR z')) *)
intros P z p HP H'.
case
 (RoundedModeRep b radix precision)
  with (P := P) (p := Float z 0%nat) (q := p); auto.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := HP); auto ]; 
 auto.
(* Goal: P (FtoR radix (Float z (Z.of_nat O))) p *)
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix p) (FtoR radix (Float x (Fexp (Float z (Z.of_nat O)))))), @ex Z (fun z' : Z => @eq R (FtoRradix p) (IZR z')) *)
apply Cp with (1 := H'); auto.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR x) (IZR (Zpos xH))) (IZR x) *)
rewrite Rmult_1_r; auto.
(* Goal: Fbounded b p *)
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix p) (FtoR radix (Float x (Fexp (Float z (Z.of_nat O)))))), @ex Z (fun z' : Z => @eq R (FtoRradix p) (IZR z')) *)
apply RoundedModeBounded with (P := P) (r := IZR z); auto.
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix p) (FtoR radix (Float x (Fexp (Float z (Z.of_nat O)))))), @ex Z (fun z' : Z => @eq R (FtoRradix p) (IZR z')) *)
intros x H'0; exists x; auto.
(* Goal: @eq R (FtoRradix p) (IZR x) *)
unfold FtoRradix in |- *; rewrite H'0.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR x) (IZR (Zpos xH))) (IZR x) *)
rewrite Rmult_1_r; auto.
Qed.
 
Theorem NroundN :
 forall (P : R -> float -> Prop) (n : nat) (p : float),
 RoundedModeP b radix P -> P n p -> exists n' : nat, p = n' :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (n : nat) (p : float) (_ : RoundedModeP b radix P) (_ : P (INR n) p), @ex nat (fun n' : nat => @eq R (FtoRradix p) (INR n')) *)
intros P n p HP H'.
(* Goal: @ex nat (fun n' : nat => @eq R (FtoRradix p) (INR n')) *)
case (ZroundZ P (Z_of_nat n) p); auto.
(* Goal: @eq R (IZR (Z.of_nat (Z.abs_nat x))) (INR (Z.abs_nat x)) *)
(* Goal: Z.le Z0 x *)
repeat rewrite <- INR_IZR_INZ; auto.
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix p) (IZR x)), @ex nat (fun n' : nat => @eq R (FtoRradix p) (INR n')) *)
intros x H'0; exists (Zabs_nat x).
(* Goal: @eq R (FtoRradix p) (INR (Z.abs_nat x)) *)
rewrite <- (inj_abs x) in H'0.
(* Goal: @eq R (FtoRradix p) (INR (Z.abs_nat x)) *)
(* Goal: Z.le Z0 x *)
rewrite H'0.
(* Goal: @eq R (IZR (Z.of_nat (Z.abs_nat x))) (INR (Z.abs_nat x)) *)
(* Goal: Z.le Z0 x *)
repeat rewrite <- INR_IZR_INZ; auto.
(* Goal: Z.le Z0 x *)
apply le_IZR; simpl in |- *.
(* Goal: Rle (IZR Z0) (IZR x) *)
rewrite <- H'0; auto.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply RleRoundedR0 with (P := P) (r := INR n); auto.
(* Goal: Rle (IZR Z0) (INR n) *)
replace 0%R with (INR 0); auto with real arith.
Qed.
(* Properties of LSB and MSB *)
 
Theorem FUlp_Le_LSigB :
 forall x : float, Fbounded b x -> (Fulp x <= Float 1%nat (LSB radix x))%R.
intros x H; unfold is_Fzero, Fulp, Fnormalize in |- *;
 case (Z_zerop (Fnum x)); intros ZH.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: Rle (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x))))))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
rewrite Rmult_1_l.
(* Goal: Rle (powerRZ (IZR radix) (Z.opp (Z.of_N (dExp b)))) (powerRZ (IZR radix) (LSB radix x)) *)
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix x))) *)
apply Rle_powerRZ.
(* Goal: Rle (IZR (Zpos xH)) (IZR radix) *)
(* Goal: Z.le (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))))) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)) *)
replace 1%R with (INR 1); auto with real arith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (LSB radix x) *)
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix x))) *)
apply Zle_trans with (Fexp x); auto.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp x) *)
(* Goal: Z.le (Fexp x) (LSB radix x) *)
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix x))) *)
case H; auto.
(* Goal: Z.le (Fexp x) (LSB radix x) *)
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix x))) *)
apply Fexp_le_LSB; auto.
rewrite
 LSB_shift
           with
           (n := 
             min (precision - Fdigit radix x) (Zabs_nat (dExp b + Fexp x)));
 auto.
(* Goal: Rle (powerRZ (IZR radix) (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: Rle (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x))))))) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)))) *)
rewrite Rmult_1_l.
(* Goal: Rle (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x))))))) (powerRZ (IZR radix) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x))) *)
apply Rle_powerRZ; auto with arith.
(* Goal: Rle (IZR (Zpos xH)) (IZR radix) *)
(* Goal: Z.le (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))))) (LSB radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))) x)) *)
replace 1%R with (INR 1); auto with real arith.
exact
 (Fexp_le_LSB radix
    (Fshift radix
       (min (precision - Fdigit radix x) (Zabs_nat (dExp b + Fexp x))) x)).
Qed.
 
Theorem MSBisMin :
 forall f1 f2 : float,
 (0 <= f1)%R ->
 isMin b radix f1 f2 ->
 ~ is_Fzero f1 -> ~ is_Fzero f2 -> MSB radix f1 = MSB radix f2.
intros f1 f2 H' H'0 H'1 H'2.
(* Goal: @eq Z (Z.sub (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp min'))))) (Fnum min')) (Z.succ (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_antisym.
2: apply MSB_monotone; auto.
2: repeat rewrite Fabs_correct1; auto with arith.
2: apply isMin_inv1 with (1 := H'0).
2: apply RleRoundedR0 with (P := isMin b radix) (r := FtoRradix f1); auto.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
2: apply MinRoundedModeP with (precision := precision); auto.
case (Zle_or_lt (MSB radix f1) (MSB radix f2)); auto.
intros H'3; absurd (Float 1%nat (Zsucc (MSB radix f2)) <= f2)%R.
(* Goal: not (Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min)) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply Rgt_not_le.
red in |- *; unfold FtoRradix in |- *; rewrite <- Fabs_correct1;
 auto with float arith.
apply abs_lt_MSB; auto.
apply RleRoundedR0 with (P := isMin b radix) (r := FtoRradix f1);
 auto with float.
(* Goal: RoundedModeP b radix (isMin b radix) *)
(* Goal: Fbounded b (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (FtoRradix min) *)
(* Goal: Rle (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) r) *)
(* Goal: @eq R (FtoRradix (Float (Fnum min) (Z.succ (Fexp min)))) (Rmult (IZR radix) (FtoRradix min)) *)
(* Goal: Fbounded b (Float (Fnum min) (Z.succ (Fexp min))) *)
apply MinRoundedModeP with (precision := precision); auto.
(* Goal: Rle (FtoRradix max) (FtoR radix f) *)
(* Goal: Rlt (FtoR radix f) (FtoRradix max) *)
case H'0.
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
apply (FboundedOne _ radixMoreThanOne b precision); auto with arith.
apply Zle_trans with (Fexp f2).
case H'4; auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_trans with (MSB radix f2); auto with zarith.
apply Fexp_le_MSB; auto.
apply Rle_trans with (FtoR radix (Float 1%nat (MSB radix f1))); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply oneExp_le; auto with zarith.
unfold FtoRradix in |- *; rewrite <- Fabs_correct1 with (x := f1);
 auto with float arith.
apply MSB_le_abs; auto.
Qed.
 
Theorem MSBtoZero :
 forall f1 f2 : float,
 ToZeroP b radix f1 f2 ->
 ~ is_Fzero f1 -> ~ is_Fzero f2 -> MSB radix f1 = MSB radix f2.
(* Goal: forall (f1 f2 : float) (_ : ToZeroP b radix (FtoRradix f1) f2) (_ : not (is_Fzero f1)) (_ : not (is_Fzero f2)), @eq Z (MSB radix f1) (MSB radix f2) *)
intros f1 f2 H' H'0 H'1; Casec H'; intros tmp; Elimc tmp; intros H1 H2.
(* Goal: @eq Z (MSB radix f1) (MSB radix f2) *)
(* Goal: @eq Z (MSB radix f1) (MSB radix f2) *)
apply MSBisMin; auto.
(* Goal: @eq Z (MSB radix f1) (MSB radix f2) *)
rewrite (MSB_opp radix f1).
(* Goal: @eq Z (MSB radix (Fopp f1)) (MSB radix f2) *)
rewrite (MSB_opp radix f2).
(* Goal: @eq Z (MSB radix (Fopp f1)) (MSB radix (Fopp f2)) *)
apply MSBisMin; auto with float.
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp f1)) *)
(* Goal: isMin b radix (FtoRradix (Fopp f1)) (Fopp f2) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (IZR Z0) (Ropp (FtoR radix f1)) *)
(* Goal: isMin b radix (FtoRradix (Fopp f1)) (Fopp f2) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMin b radix (FtoRradix (Fopp f1)) (Fopp f2) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with float.
Qed.
 
Theorem MSBBoundNotZero :
 forall P : R -> float -> Prop,
 RoundedModeP b radix P ->
 forall f1 f2 : float,
 P f1 f2 -> f1 <> 0%R :>R -> (- dExp b <= MSB radix f1)%Z -> f2 <> 0%R :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b radix P) (f1 f2 : float) (_ : P (FtoRradix f1) f2) (_ : not (@eq R (FtoRradix f1) (IZR Z0))) (_ : Z.le (Z.opp (Z.of_N (dExp b))) (MSB radix f1)), not (@eq R (FtoRradix f2) (IZR Z0)) *)
intros P H' f1 f2 H'0 H'1 H'2.
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
case (Rle_or_lt 0 f1); intros Rl1.
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
apply Rlt_dichotomy_converse; right; red in |- *.
(* Goal: Rlt (IZR Z0) (FtoRradix f2) *)
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
apply Rlt_le_trans with (r2 := FtoRradix (Float 1%nat (MSB radix f1))); auto.
unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite Rmult_1_l;
 auto with real arith.
cut (Float 1%nat (MSB radix f1) <= Fabs f1)%R; unfold FtoRradix in |- *;
 [ rewrite Fabs_correct; auto with arith; rewrite Rabs_right; auto with real;
    intros Rl2; Casec Rl2; intros Rl2
 | apply MSB_le_abs ]; auto.
cut (MonotoneP radix P);
 [ intros Mn | apply RoundedModeP_inv4 with (1 := H'); auto ].
(* Goal: Rle (FtoR radix (Float (Z.of_nat (S O)) (MSB radix f1))) (FtoR radix f2) *)
(* Goal: Rle (FtoR radix (Float (Z.of_nat (S O)) (MSB radix f1))) (FtoR radix f2) *)
(* Goal: not (is_Fzero f1) *)
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
apply (Mn (Float 1%nat (MSB radix f1)) f1); auto.
(* Goal: P (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdem; auto.
apply (FboundedOne radix) with (precision := precision);
 auto with real zarith arith.
replace (FtoR radix f2) with (FtoR radix (Float 1%nat (MSB radix f1)));
 auto with float real.
(* Goal: @eq R (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (FtoRradix f2) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdemEq with (P := P); auto.
apply (FboundedOne radix) with (precision := precision);
 auto with real zarith arith.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ].
(* Goal: P (FtoR radix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply (Cp f1) with (p := f2); auto.
(* Goal: Fbounded b f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeBounded with (P := P) (r := FtoRradix f1); auto.
(* Goal: not (is_Fzero p) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
Contradict H'1; unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
(* Goal: not (@eq R (FtoRradix f2) (IZR Z0)) *)
apply Rlt_dichotomy_converse; left.
apply Rle_lt_trans with (r2 := FtoRradix (Float (- 1%nat) (MSB radix f1)));
 auto.
cut (MonotoneP radix P);
 [ intros Mn | apply RoundedModeP_inv4 with (1 := H'); auto ].
cut (f1 <= Float (- 1%nat) (MSB radix f1))%R;
 [ intros Rle1; Casec Rle1; intros Rle1 | idtac ].
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply (Mn f1 (Float (- 1%nat) (MSB radix f1))); auto.
(* Goal: P (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: Rle (FtoRradix f2) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdem; auto.
(* Goal: Fbounded b (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: P (FtoR radix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply oppBoundedInv; unfold Fopp in |- *; simpl in |- *.
apply (FboundedOne radix) with (precision := precision);
 auto with real zarith arith.
replace (FtoRradix f2) with (FtoRradix (Float (- 1%nat) (MSB radix f1)));
 auto with real.
(* Goal: @eq R (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (FtoRradix f2) *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeProjectorIdemEq with (P := P); auto.
(* Goal: Fbounded b (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: P (FtoR radix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply oppBoundedInv; unfold Fopp in |- *; simpl in |- *.
apply (FboundedOne _ radixMoreThanOne b precision);
 auto with real zarith arith.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ].
(* Goal: P (FtoR radix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply (Cp f1) with (p := f2); auto.
(* Goal: Fbounded b f2 *)
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
apply RoundedModeBounded with (P := P) (r := FtoRradix f1); auto.
(* Goal: Rle (FtoRradix f1) (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
replace (FtoRradix f1) with (- FtoRradix (Fabs f1))%R.
replace (Float (- 1%nat) (MSB radix f1)) with
 (Fopp (Float 1%nat (MSB radix f1))).
(* Goal: Rle (Ropp (FtoRradix (Fabs f1))) (FtoRradix (Fopp (Float (Z.of_nat (S O)) (MSB radix f1)))) *)
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (MSB radix f1))) (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1)) *)
(* Goal: @eq R (Ropp (FtoRradix (Fabs f1))) (FtoRradix f1) *)
(* Goal: Rlt (FtoRradix (Float (Z.opp (Z.of_nat (S O))) (MSB radix f1))) (IZR Z0) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto.
apply Ropp_le_contravar; apply MSB_le_abs; auto.
(* Goal: not (is_Fzero p) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
Contradict H'1; unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
unfold Fopp in |- *; simpl in |- *; auto.
unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith;
 rewrite Faux.Rabsolu_left1; try apply Rlt_le; auto; 
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 ring.
replace (Float (- 1%nat) (MSB radix f1)) with
 (Fopp (Float 1%nat (MSB radix f1)));
 [ idtac | unfold Fopp in |- *; simpl in |- *; auto ].
(* Goal: Rlt (FtoRradix (Fopp (Float (Z.of_nat (S O)) (MSB radix f1)))) (IZR Z0) *)
replace 0%R with (-0)%R; [ idtac | ring ].
unfold FtoRradix in |- *; repeat rewrite Fopp_correct;
 apply Ropp_lt_contravar.
(* Goal: Rlt (IZR Z0) (FtoR radix (Float (Z.of_nat (S O)) (MSB radix f1))) *)
unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real arith.
Qed.
 
Theorem RoundMSBmax :
 forall (P : R -> float -> Prop) (p q : float),
 RoundedModeP b radix P ->
 P p q ->
 p <> 0%R :>R ->
 (- dExp b <= MSB radix p)%Z -> (MSB radix q <= Zsucc (MSB radix p))%Z.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p q : float) (_ : RoundedModeP b radix P) (_ : P (FtoRradix p) q) (_ : not (@eq R (FtoRradix p) (IZR Z0))) (_ : Z.le (Z.opp (Z.of_N (dExp b))) (MSB radix p)), Z.le (MSB radix p) (MSB radix q) *)
intros P p q H' H'0 H'1 H'2.
(* Goal: Z.le (MSB radix q) (Z.succ (MSB radix p)) *)
apply (oneExp_Zle radix); auto.
(* Goal: Rle (FtoR radix (Float (Z.of_nat (S O)) (MSB radix q))) (FtoR radix (Float (Z.of_nat (S O)) (Z.succ (MSB radix p)))) *)
apply Rle_trans with (FtoRradix (Fabs q)).
unfold FtoRradix in |- *; apply MSB_le_abs; auto.
(* Goal: not (is_Fzero q) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
red in |- *; intros H'3; absurd (q = 0%R :>R).
(* Goal: not (@eq R (FtoRradix q) (IZR Z0)) *)
(* Goal: @eq R (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
apply MSBBoundNotZero with (P := P) (f1 := p); auto.
(* Goal: @eq R (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix (Fabs q)) (FtoR radix (Float (Z.of_nat (S O)) (Z.succ (MSB radix p)))) *)
apply (is_Fzero_rep1 radix); auto.
unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith;
 fold FtoRradix in |- *.
(* Goal: Rle (Rabs (FtoRradix q)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB radix p)))) *)
apply RoundAbsMonotoner with (P := P) (p := FtoRradix p); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply (FboundedOne _ radixMoreThanOne b precision); auto with zarith.
(* Goal: Rle (Rabs (FtoRradix p)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB radix p)))) *)
unfold FtoRradix in |- *; rewrite <- (Fabs_correct radix); auto with arith.
apply Rlt_le; apply abs_lt_MSB; auto.
Qed.
 
Theorem RoundMSBmin :
 forall (P : R -> float -> Prop) (p q : float),
 RoundedModeP b radix P ->
 P p q ->
 p <> 0%R :>R ->
 (- dExp b <= MSB radix p)%Z -> (MSB radix p <= MSB radix q)%Z.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p q : float) (_ : RoundedModeP b radix P) (_ : P (FtoRradix p) q) (_ : not (@eq R (FtoRradix p) (IZR Z0))) (_ : Z.le (Z.opp (Z.of_N (dExp b))) (MSB radix p)), Z.le (MSB radix p) (MSB radix q) *)
intros P p q H' H'0 H'1 H'2.
(* Goal: Z.le (MSB radix p) (MSB radix q) *)
replace (MSB radix p) with (MSB radix (Float 1%nat (MSB radix p))).
(* Goal: Z.le (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix q) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
apply MSB_monotone; auto.
(* Goal: not (is_Fzero (Float (Z.of_nat (S O)) (MSB radix p))) *)
(* Goal: not (is_Fzero q) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
unfold is_Fzero in |- *; simpl in |- *; red in |- *; intros; discriminate.
(* Goal: not (is_Fzero q) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
red in |- *; intros H'3; absurd (q = 0%R :>R).
(* Goal: not (@eq R (FtoRradix q) (IZR Z0)) *)
(* Goal: @eq R (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
apply MSBBoundNotZero with (P := P) (f1 := p); auto.
(* Goal: @eq R (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoR radix (Fabs (Float (Z.of_nat (S O)) (MSB radix p)))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
replace (Fabs (Float 1%nat (MSB radix p))) with (Float 1%nat (MSB radix p));
 [ idtac | unfold Fabs in |- *; simpl in |- *; auto ].
(* Goal: Rle (FtoR radix (Float (Z.of_nat (S O)) (MSB radix p))) (FtoR radix (Fabs q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
rewrite Fabs_correct; auto with arith; fold FtoRradix in |- *.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB radix p))) (Rabs (FtoRradix q)) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
apply RoundAbsMonotonel with (P := P) (p := FtoRradix p); auto.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply (FboundedOne _ radixMoreThanOne b precision); auto with zarith.
unfold FtoRradix in |- *; rewrite <- (Fabs_correct radix); auto with arith;
 apply MSB_le_abs; auto.
(* Goal: not (is_Fzero p) *)
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
Contradict H'1; unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
(* Goal: @eq Z (MSB radix (Float (Z.of_nat (S O)) (MSB radix p))) (MSB radix p) *)
unfold MSB, Fdigit in |- *; simpl in |- *.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
case (Zpred (digit radix (Fnum p) + Fexp p)); simpl in |- *; auto with zarith.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
intros p0; case p0; simpl in |- *; auto.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
intros p1; elim p1; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : @eq Z (Zpos (Pos.pred_double (Pos.succ p))) (Zpos (xI p))), @eq Z (Zpos (xI (Pos.pred_double (Pos.succ p)))) (Zpos (xI (xI p))) *)
(* Goal: forall p : positive, @eq Z (Z.pred (Z.pos_sub xH p)) (Zneg p) *)
intros p2 H; injection H; intros H1; rewrite <- H1; auto.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
intros p0; case p0; simpl in |- *; auto.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
intros p1; case p1; simpl in |- *; auto.
(* Goal: @eq float (Fopp (Float (Z.of_nat (S O)) (Z.opp (Z.of_N (dExp b))))) (Float (Z.opp (Z.of_nat (S O))) (Z.opp (Z.of_N (dExp b)))) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle r (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
intros p2; elim p2; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : @eq Z (Zneg (xO (Pos.succ (Pos.pred_double p)))) (Zneg (xO (xO p)))), @eq Z (Zneg (xO (xO (Pos.succ (Pos.pred_double p))))) (Zneg (xO (xO (xO p)))) *)
intros p3 H; injection H; intros H1; rewrite H1; auto.
Qed.
 
Theorem RoundLSBMax :
 forall (P : R -> float -> Prop) (p q : float),
 RoundedModeP b radix P ->
 P p q -> ~ is_Fzero q -> (LSB radix p <= LSB radix q)%Z.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p q : float) (_ : RoundedModeP b radix P) (_ : P (FtoRradix p) q) (_ : not (is_Fzero q)), Z.le (LSB radix p) (LSB radix q) *)
intros P p q H' H'0 H'2.
(* Goal: Z.le (LSB radix p) (LSB radix q) *)
elim (LSB_rep_min radix) with (p := p); auto; intros z E.
case
 (RoundedModeRep b radix precision)
  with (P := P) (p := Float z (LSB radix p)) (q := q); 
 auto.
cut (CompatibleP b radix P);
 [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ].
(* Goal: P (FtoR radix (Float z (LSB radix p))) q *)
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix q) (FtoR radix (Float x (Fexp (Float z (LSB radix p)))))), Z.le (LSB radix p) (LSB radix q) *)
apply (Cp p (Float z (LSB radix p)) q); auto.
(* Goal: Fbounded b q *)
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix q) (FtoR radix (Float x (Fexp (Float z (LSB radix p)))))), Z.le (LSB radix p) (LSB radix q) *)
apply RoundedModeBounded with (P := P) (r := FtoRradix p); auto.
(* Goal: forall (x : Z) (_ : @eq R (FtoR radix q) (FtoR radix (Float x (Fexp (Float z (LSB radix p)))))), Z.le (LSB radix p) (LSB radix q) *)
intros x H'3.
replace (LSB radix p) with (Fexp (Float x (LSB radix p)));
 [ idtac | simpl in |- *; auto ].
(* Goal: Z.le (Fexp (Float x (LSB radix p))) (LSB radix q) *)
replace (LSB radix q) with (LSB radix (Float x (LSB radix p))).
(* Goal: Z.le (Fexp (Float x (LSB radix p))) (LSB radix (Float x (LSB radix p))) *)
(* Goal: @eq Z (LSB radix (Float x (LSB radix p))) (LSB radix q) *)
apply Fexp_le_LSB.
(* Goal: @eq Z (LSB radix (Float x (LSB radix p))) (LSB radix q) *)
apply LSB_comp; auto.
(* Goal: not (is_Fzero (Float x (LSB radix p))) *)
apply NisFzeroComp with (radix := radix) (x := q); auto.
Qed.
(* General theorem about the binade *)
 
Theorem InBinade :
 forall (P : R -> float -> Prop) (p q r : float) (e : Z),
 RoundedModeP b radix P ->
 Fbounded b p ->
 Fbounded b q ->
 P (p + q)%R r ->
 (- dExp b <= e)%Z ->
 (Float (Zpower_nat radix (pred precision)) e <= p)%R ->
 (p <= Float (pPred (vNum b)) e)%R ->
 (0%nat < q)%R ->
 (q < powerRZ radix e)%R -> r = p :>R \/ r = (p + powerRZ radix e)%R :>R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (p q r : float) (e : Z) (_ : RoundedModeP b radix P) (_ : Fbounded b p) (_ : Fbounded b q) (_ : P (Rplus (FtoRradix p) (FtoRradix q)) r) (_ : Z.le (Z.opp (Z.of_N (dExp b))) e) (_ : Rle (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) e)) (FtoRradix p)) (_ : Rle (FtoRradix p) (FtoRradix (Float (pPred (vNum b)) e))) (_ : Rlt (INR O) (FtoRradix q)) (_ : Rlt (FtoRradix q) (powerRZ (IZR radix) e)), or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
intros P p q r e Rp H' H'0 H'1 H'2 H'3 H'4 H'5 H'6.
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
cut (p < p + q)%R; [ intros Rlt1 | idtac ].
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
cut (p + q < FNSucc b radix precision p)%R; [ intros Rlt2 | idtac ].
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
cut (isMin b radix (p + q) p); [ intros Min1 | idtac ].
cut (isMax b radix (p + q) (FNSucc b radix precision p));
 [ intros Max1 | idtac ].
cut (MinOrMaxP b radix P);
 [ intros MinOrMax | apply RoundedModeP_inv3 with (1 := Rp); auto ].
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
case (MinOrMax (p + q)%R r); auto; intros H1.
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
left.
(* Goal: @eq R (FtoRradix r) (FtoRradix p) *)
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply (MinUniqueP b radix (p + q)%R); auto.
(* Goal: or (@eq R (FtoRradix r) (FtoRradix p)) (@eq R (FtoRradix r) (Rplus (FtoRradix p) (powerRZ (IZR radix) e))) *)
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
right.
cut ((p + powerRZ radix e)%R = FNSucc b radix precision p);
 [ intros Eq1; rewrite Eq1 | idtac ].
(* Goal: @eq R (FtoRradix r) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: @eq R (Rplus (FtoRradix p) (powerRZ (IZR radix) e)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply (MaxUniqueP b radix (p + q)%R); auto.
replace (FtoRradix (FNSucc b radix precision p)) with
 (Fnormalize radix b precision p +
  (FNSucc b radix precision p - Fnormalize radix b precision p))%R;
 [ idtac | ring ].
unfold FNSucc in |- *; rewrite <- (Fminus_correct radix); auto with arith;
 rewrite (FSuccDiff1 b radix precision); auto with arith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite (boundedNorMinGivesExp radix) with (x := e); auto with zarith.
rewrite (FnormalizeCorrect radix); auto; unfold FtoRradix, FtoR in |- *;
(* Goal: @eq Z (Fexp min') (Z.sub (Fexp p) (Z.sub (Fexp p) (Fexp min'))) *)
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 simpl in |- *; ring.
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply sym_not_equal; apply Zlt_not_eq.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_lt_trans with 0%Z; auto with zarith.
replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp;
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 apply Zlt_le_weak; apply nNormPos; auto with zarith.
(* Goal: Z.lt Z0 (Fnum (Fnormalize radix b precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply (LtR0Fnum radix); auto.
(* Goal: Rlt (IZR Z0) (FtoR radix (Fnormalize radix b precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
rewrite FnormalizeCorrect; fold FtoRradix in |- *; auto.
(* Goal: Rlt (IZR Z0) (FtoRradix p) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le_trans with (2 := H'3).
apply (LtFnumZERO radix); simpl in |- *;
 (replace 0%Z with (Z_of_nat 0); auto with zarith arith).
(* Goal: isMax b radix (Rplus (FtoRradix p) (FtoRradix q)) (FNSucc b radix precision p) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply MinMax; auto with arith.
(* Goal: not (@eq R (Rplus (FtoRradix p) (FtoRradix q)) (FtoR radix p)) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
Contradict Rlt1.
(* Goal: not (Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q))) *)
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
rewrite Rlt1; auto with real.
(* Goal: isMin b radix (Rplus (FtoRradix p) (FtoRradix q)) p *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply MinBinade with (precision := precision); auto with arith.
(* Goal: Rle (FtoR radix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le; auto.
replace (FtoRradix (FNSucc b radix precision p)) with
 (Fnormalize radix b precision p +
  (FNSucc b radix precision p - Fnormalize radix b precision p))%R;
 [ idtac | ring ].
unfold FNSucc in |- *; rewrite <- (Fminus_correct radix); auto with arith;
 rewrite (FSuccDiff1 b radix precision); auto with arith.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
rewrite (boundedNorMinGivesExp radix) with (x := e); auto with zarith.
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (Rplus (FtoRradix (Fnormalize radix b precision p)) (FtoR radix (Float (Z.of_nat (S O)) e))) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
rewrite (FnormalizeCorrect radix); auto; fold FtoRradix in |- *.
(* Goal: Rlt (Rplus (FtoRradix p) (FtoRradix q)) (Rplus (FtoRradix p) (FtoRradix (Float (Z.of_nat (S O)) e))) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
replace (FtoRradix (Float 1%nat e)) with (powerRZ radix e); auto with real.
(* Goal: @eq R (powerRZ (IZR radix) e) (FtoRradix (Float (Z.of_nat (S O)) e)) *)
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
(* Goal: not (@eq Z (Fnum (Fnormalize radix b precision p)) (Z.opp (nNormMin radix precision))) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply sym_not_equal; apply Zlt_not_eq.
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
apply Zle_lt_trans with 0%Z; auto with zarith.
replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp;
(* Goal: Z.le Z0 (Z.sub (Fexp p) (Fexp min')) *)
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix (Float (Fnum min') (Fexp min')))) (FtoRradix (Float (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Fexp min'))) *)
(* Goal: @eq Z (Z.mul (Z.of_nat (S (S O))) (Fnum min')) (Z.add (Fnum min') (Fnum min')) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rminus (FtoRradix p) (FtoRradix min)))) *)
 apply Zlt_le_weak; apply nNormPos; auto with zarith.
(* Goal: Z.lt Z0 (Fnum (Fnormalize radix b precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply (LtR0Fnum radix); auto.
(* Goal: Rlt (IZR Z0) (FtoR radix (Fnormalize radix b precision p)) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
rewrite FnormalizeCorrect; fold FtoRradix in |- *; auto.
(* Goal: Rlt (IZR Z0) (FtoRradix p) *)
(* Goal: Rlt (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rlt_le_trans with (2 := H'3).
apply (LtFnumZERO radix); simpl in |- *;
 (replace 0%Z with (Z_of_nat 0); auto with zarith arith).
pattern (FtoRradix p) at 1 in |- *; replace (FtoRradix p) with (p + 0)%R;
 [ idtac | ring ].
(* Goal: Rlt (Rplus (FtoRradix p) (IZR Z0)) (Rplus (FtoRradix p) (FtoRradix q)) *)
apply Rplus_lt_compat_l; auto.
Qed.
 
End FRoundP.
Hint Resolve FulpSucCan FulpSuc FulpPredCan FulpPred: float.