(****************************************************************************
                                                                             
          IEEE754  :  Fmin                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Zenum.
Require Export FPred.
 
Section FMinMax.
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 precisionNotZero : precision <> 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
(* a function that returns a boundd greater than a given nat *)
 
Definition boundNat (n : nat) := Float 1%nat (digit radix n).
 
Theorem boundNatCorrect : forall n : nat, (n < boundNat n)%R.
(* Goal: forall n : nat, Rlt (INR n) (FtoRradix (boundNat n)) *)
intros n; unfold FtoRradix, FtoR, boundNat in |- *; simpl in |- *.
(* Goal: Rlt (INR n) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.of_nat (digit radix (Z.of_nat n))))) *)
rewrite Rmult_1_l.
(* Goal: Rlt (INR n) (powerRZ (IZR radix) (Z.of_nat (digit radix (Z.of_nat n)))) *)
rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith.
(* Goal: Rle (IZR (up r)) (INR (Z.abs_nat (up r))) *)
(* Goal: @eq R r (Rabs r) *)
rewrite INR_IZR_INZ; auto with real zarith.
(* Goal: Rlt (IZR (Z.of_nat n)) (IZR (Zpower_nat radix (digit radix (Z.of_nat n)))) *)
apply Rle_lt_trans with (Zabs n); [rewrite (Zabs_eq (Z_of_nat n))|idtac];auto with real zarith.
Qed.
 
Theorem boundBoundNat : forall n : nat, Fbounded b (boundNat n).
intros n; repeat split; unfold boundNat in |- *; simpl in |- *;
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
 auto with zarith.
apply vNumbMoreThanOne with (radix := radix) (precision := precision);
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
 auto with zarith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.of_nat (digit radix (Z.of_nat n))) *)
apply Zle_trans with 0%Z;[case (dExp b)|idtac]; auto with zarith.
Qed.
(* A function that returns a bounded greater than a given r *)
 
Definition boundR (r : R) := boundNat (Zabs_nat (up (Rabs r))).
 
Theorem boundRCorrect1 : forall r : R, (r < boundR r)%R.
(* Goal: forall r : R, Rlt (FtoRradix (Fopp (boundR r))) r *)
intros r; case (Rle_or_lt r 0); intros H'.
(* Goal: Rlt r (FtoRradix (boundR r)) *)
(* Goal: Rlt r (FtoRradix (boundR r)) *)
apply Rle_lt_trans with (1 := H').
unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *;
 auto with real.
(* Goal: Rlt (IZR Z0) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))))) *)
(* Goal: Rlt r (FtoRradix (boundR r)) *)
rewrite Rmult_1_l; auto with real zarith.
(* Goal: Rlt r (FtoRradix (boundR r)) *)
apply Rlt_trans with (2 := boundNatCorrect (Zabs_nat (up (Rabs r)))).
(* Goal: Rlt r (INR (Z.abs_nat (up (Rabs r)))) *)
replace (Rabs r) with r; auto with real.
(* Goal: Rlt r (INR (Z.abs_nat (up r))) *)
(* Goal: @eq R r (Rabs r) *)
apply Rlt_le_trans with (r2 := IZR (up r)); auto with real zarith.
(* Goal: Rlt r (IZR (up r)) *)
(* Goal: Rle (IZR (up r)) (INR (Z.abs_nat (up r))) *)
(* Goal: @eq R r (Rabs r) *)
case (archimed r); auto.
(* Goal: Rle (IZR (up r)) (INR (Z.abs_nat (up r))) *)
(* Goal: @eq R r (Rabs r) *)
rewrite INR_IZR_INZ; auto with real zarith.
(* Goal: @eq R r (Rabs r) *)
unfold Rabs in |- *; case (Rcase_abs r); auto with real.
(* Goal: forall _ : Rlt r (IZR Z0), @eq R r (Ropp r) *)
intros H'0; Contradict H'0; auto with real.
Qed.
 
Theorem boundRrOpp : forall r : R, boundR r = boundR (- r).
(* Goal: forall r : R, @eq float (boundR r) (boundR (Ropp r)) *)
intros R; unfold boundR in |- *.
(* Goal: @eq float (boundNat (Z.abs_nat (up (Rabs R)))) (boundNat (Z.abs_nat (up (Rabs (Ropp R))))) *)
rewrite Rabs_Ropp; auto.
Qed.
 
Theorem boundRCorrect2 : forall r : R, (Fopp (boundR r) < r)%R.
(* Goal: forall r : R, Rlt (FtoRradix (Fopp (boundR r))) r *)
intros r; case (Rle_or_lt r 0); intros H'.
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
rewrite boundRrOpp.
(* Goal: Rlt (FtoRradix (Fopp (boundR (Ropp r)))) r *)
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
pattern r at 2 in |- *; rewrite <- (Ropp_involutive r).
(* Goal: isMin (FtoRradix (Fopp p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rlt (Ropp (FtoR radix (boundR (Ropp r)))) (Ropp (Ropp r)) *)
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
apply Ropp_lt_contravar; apply boundRCorrect1; auto.
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
apply Rle_lt_trans with 0%R; auto.
(* Goal: Rle (FtoRradix (Fopp (boundR r))) (IZR Z0) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: isMin (FtoRradix (Fopp p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (Ropp (Ropp (FtoR radix f))) (Ropp (FtoR radix p)) *)
apply Ropp_le_contravar.
unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *;
 auto with real zarith.
(* Goal: Rle (IZR Z0) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))))) *)
rewrite Rmult_1_l; apply Rlt_le; auto with real zarith arith.
Qed.
(* A function that returns a list containing all the bounded smaller than a given real *)
 
Definition mBFloat (p : R) :=
  map (fun p : Z * Z => Float (fst p) (snd p))
    (mProd Z Z (Z * Z)
       (mZlist (- pPred (vNum b)) (pPred (vNum b)))
       (mZlist (- dExp b) (Fexp (boundR p)))).
 
Theorem mBFadic_correct1 :
 forall (r : R) (q : float),
 ~ is_Fzero q ->
 (Fopp (boundR r) < q)%R ->
 (q < boundR r)%R -> Fbounded b q -> In q (mBFloat r).
(* Goal: forall (r : R) (q : float) (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
intros r q.
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
case (Zle_or_lt (Fexp (boundR r)) (Fexp q)); intros H'.
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
intros H'0 H'1 H'2 H'3; case H'0.
(* Goal: is_Fzero q *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
apply is_Fzero_rep2 with (radix := radix); auto.
rewrite <-
 FshiftCorrect with (n := Zabs_nat (Fexp q - Fexp (boundR r))) (x := q);
 auto with arith.
(* Goal: @eq R (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (IZR Z0) *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
apply is_Fzero_rep1 with (radix := radix).
(* Goal: is_Fzero (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q) *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
unfold is_Fzero in |- *.
cut (forall p : Z, (- 1%nat < p)%Z -> (p < 1%nat)%Z -> p = 0%Z);
 [ intros tmp; apply tmp | idtac ].
(* Goal: Z.lt (Z.opp (Z.of_nat (S O))) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
replace (- 1%nat)%Z with (Fnum (Fopp (boundR r))).
(* Goal: Z.lt (Fnum (Fopp (boundR r))) (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) *)
(* Goal: @eq Z (Fnum (Fopp (boundR r))) (Z.opp (Z.of_nat (S O))) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with real zarith.
(* Goal: Rlt (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (FtoR radix (boundR r)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Fexp (boundR r)) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
rewrite FshiftCorrect; auto.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Fexp (boundR r)) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))) (Z.sub (Fexp q) (Z.of_nat (Z.abs_nat (Z.sub (Fexp q) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))))))) *)
(* Goal: @eq Z (Fnum (Fopp (boundR r))) (Z.opp (Z.of_nat (S O))) *)
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
rewrite (fun x y => inj_abs (x - y)); auto with zarith.
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
simpl in |- *; auto.
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
replace (Z_of_nat 1) with (Fnum (boundR r)).
(* Goal: Z.lt (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Fnum (boundR r)) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith.
(* Goal: Rlt (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (FtoR radix (boundR r)) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Fexp (boundR r)) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
rewrite FshiftCorrect; auto.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp (boundR r)))) q)) (Fexp (boundR r)) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.sub (Fexp q) (Z.of_nat (Z.abs_nat (Z.sub (Fexp q) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))))))) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
rewrite inj_abs; auto with zarith.
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
generalize H'; simpl in |- *; auto with zarith.
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
simpl in |- *; auto.
(* Goal: forall (p : Z) (_ : Z.lt (Zneg xH) p) (_ : Z.lt p (Zpos xH)), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
intros p0; case p0; simpl in |- *; auto with zarith.
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
intros H'0 H'1 H'2 H'3; unfold mBFloat in |- *.
replace q with
 ((fun p : Z * Z => Float (fst p) (snd p)) (Fnum q, Fexp q)).
apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: @In (prod Z Z) (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p)))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mProd_correct; auto.
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply mZlist_correct; auto with float.
(* Goal: Z.le (Z.opp (pPred (vNum b))) (Fnum q) *)
(* Goal: Z.le (Fnum q) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zle_Zabs_inv1; auto with float.
(* Goal: Z.le (Z.abs (Fnum q)) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold pPred in |- *; apply Zle_Zpred; auto with float.
(* Goal: Z.le (Fnum q) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zle_Zabs_inv2; auto with float.
(* Goal: Z.le (Z.abs (Fnum q)) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold pPred in |- *; apply Zle_Zpred; auto with float.
(* Goal: @In Z (Fexp q) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply mZlist_correct; auto with float.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case q; simpl in |- *; auto with zarith.
Qed.
 
Theorem mBFadic_correct2 : forall r : R, In (boundR r) (mBFloat r).
(* Goal: forall r : R, @In float (Fopp (boundR r)) (mBFloat r) *)
intros r; unfold mBFloat in |- *.
replace (boundR r) with
 ((fun p : Z * Z => Float (fst p) (snd p))
    (Fnum (boundR r), Fexp (boundR r))).
apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: @In (prod Z Z) (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p)))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mProd_correct; auto.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zle_trans with (- (0))%Z; auto with zarith.
(* Goal: Z.le (Z.opp (pPred (vNum b))) (Z.opp Z0) *)
(* Goal: Z.le (Fnum (boundR r)) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (boundR r)) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))) (boundR r) *)
apply Zle_Zopp; unfold pPred in |- *; apply Zle_Zpred; simpl in |- *.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zlt_trans with 1%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
(* Goal: @In Z (Fexp (boundR r)) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))) (boundR r) *)
apply vNumbMoreThanOne with (3 := pGivesBound); auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fnum (Fopp (boundR r))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Fopp (boundR r))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r))))) (@snd Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r)))))) (Fopp (boundR r)) *)
unfold pPred in |- *; apply Zle_Zpred; simpl in |- *.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
(* Goal: @In Z (Fexp (boundR r)) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))) (boundR r) *)
apply vNumbMoreThanOne with (3 := pGivesBound); auto.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))) *)
(* Goal: Z.le (Fexp (boundR r)) (Fexp (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r)))) (@snd Z Z (@pair Z Z (Fnum (boundR r)) (Fexp (boundR r))))) (boundR r) *)
apply Zle_trans with 0%Z; auto with zarith arith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (dExp b); auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (boundR r); simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (boundR r); simpl in |- *; auto with zarith.
Qed.
 
Theorem mBFadic_correct3 : forall r : R, In (Fopp (boundR r)) (mBFloat r).
(* Goal: forall r : R, @In float (Fopp (boundR r)) (mBFloat r) *)
intros r; unfold mBFloat in |- *.
replace (Fopp (boundR r)) with
 ((fun p : Z * Z => Float (fst p) (snd p))
    (Fnum (Fopp (boundR r)), Fexp (Fopp (boundR r)))).
apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: @In (prod Z Z) (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p)))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mProd_correct; auto.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
replace (-1)%Z with (- Z_of_nat 1)%Z; auto with zarith.
(* Goal: Z.le (Z.opp (pPred (vNum b))) (Z.opp (Z.of_nat (S O))) *)
(* Goal: Z.le (Fnum (Fopp (boundR r))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Fopp (boundR r))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r))))) (@snd Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r)))))) (Fopp (boundR r)) *)
apply Zle_Zopp.
(* Goal: Z.le (Fnum (Fopp (boundR r))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Fopp (boundR r))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r))))) (@snd Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r)))))) (Fopp (boundR r)) *)
unfold pPred in |- *; apply Zle_Zpred; simpl in |- *.
apply (vNumbMoreThanOne radix) with (precision := precision);
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
 auto with zarith.
(* Goal: Z.le (Fnum (Fopp (boundR r))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Fopp (boundR r))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r))))) (@snd Z Z (@pair Z Z (Fnum (Fopp (boundR r))) (Fexp (Fopp (boundR r)))))) (Fopp (boundR r)) *)
unfold pPred in |- *; apply Zle_Zpred; simpl in |- *.
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
red in |- *; simpl in |- *; auto.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zle_trans with 0%Z; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (dExp b); auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (boundR r); simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (boundR r); simpl in |- *; auto with zarith.
Qed.
 
Theorem mBFadic_correct4 :
 forall r : R, In (Float 0%nat (- dExp b)) (mBFloat r).
(* Goal: forall r : R, @In float (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) (mBFloat r) *)
intros p; unfold mBFloat in |- *.
replace (Float 0%nat (- dExp b)) with
 ((fun p : Z * Z => Float (fst p) (snd p))
    (Fnum (Float 0%nat (- dExp b)), Fexp (Float 0%nat (- dExp b)))).
apply in_map with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: @In (prod Z Z) (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p)))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mProd_correct; auto.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.opp (pPred (vNum b))) Z0 *)
(* Goal: Z.le (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
replace 0%Z with (- (0))%Z; [ idtac | simpl in |- *; auto ].
(* Goal: Z.le (Z.opp (pPred (vNum b))) (Z.opp Z0) *)
(* Goal: Z.le (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply Zle_Zopp; unfold pPred in |- *; apply Zle_Zpred.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
red in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
simpl in |- *; auto with zarith.
(* Goal: Z.le Z0 (pPred (vNum b)) *)
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
unfold pPred in |- *; apply Zle_Zpred.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
red in |- *; simpl in |- *; auto with zarith.
(* Goal: @In Z (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR p))) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))))) (@snd Z Z (@pair Z Z (Fnum (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (Fexp (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))))))) (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) *)
apply mZlist_correct; auto.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
apply Zle_trans with 0%Z; auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
case (dExp b); auto with zarith.
(* Goal: Z.le (Fexp q) (Fexp (boundR r)) *)
(* Goal: @eq float (Float (@fst Z Z (@pair Z Z (Fnum q) (Fexp q))) (@snd Z Z (@pair Z Z (Fnum q) (Fexp q)))) q *)
simpl in |- *; auto with zarith.
Qed.
 
Theorem mBPadic_Fbounded :
 forall (p : float) (r : R), In p (mBFloat r) -> Fbounded b p.
(* Goal: forall (p : float) (r : R) (_ : @In float p (mBFloat r)), Fbounded b p *)
intros p r H'; red in |- *; repeat (split; auto).
(* Goal: Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp p) *)
apply Zpred_Zle_Zabs_intro.
apply mZlist_correct_rev1 with (q := Zpred (Zpos (vNum b)));
 auto with real.
apply
 mProd_correct_rev1
  with
    (l2 := mZlist (- dExp b) (Fexp (boundR r)))
    (C := (Z * Z)%type)
    (b := Fexp p); auto.
apply
 in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: forall (a b : prod Z Z) (_ : @eq float (Float (@fst Z Z a) (@snd Z Z a)) (Float (@fst Z Z b) (@snd Z Z b))), @eq (prod Z Z) a b *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros a1 b1; case a1; case b1; simpl in |- *.
(* Goal: forall (z z0 z1 z2 : Z) (_ : @eq float (Float z1 z2) (Float z z0)), @eq (prod Z Z) (@pair Z Z z1 z2) (@pair Z Z z z0) *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros z z0 z1 z2 H'0; inversion H'0; auto.
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
generalize H'; case p; auto.
apply mZlist_correct_rev2 with (p := (- Zpred (Zpos (vNum b)))%Z);
 auto.
apply
 mProd_correct_rev1
  with
    (l2 := mZlist (- dExp b) (Fexp (boundR r)))
    (C := (Z * Z)%type)
    (b := Fexp p); auto.
apply
 in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: forall (a b : prod Z Z) (_ : @eq float (Float (@fst Z Z a) (@snd Z Z a)) (Float (@fst Z Z b) (@snd Z Z b))), @eq (prod Z Z) a b *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros a1 b1; case a1; case b1; simpl in |- *.
(* Goal: forall (z z0 z1 z2 : Z) (_ : @eq float (Float z1 z2) (Float z z0)), @eq (prod Z Z) (@pair Z Z z1 z2) (@pair Z Z z z0) *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros z z0 z1 z2 H'0; inversion H'0; auto.
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
generalize H'; case p; auto.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp p) *)
apply mZlist_correct_rev1 with (q := Fexp (boundR r)); auto.
apply
 mProd_correct_rev2
  with
    (l1 := mZlist (- pPred (vNum b)) (pPred (vNum b)))
    (C := (Z * Z)%type)
    (a := Fnum p); auto.
apply
 in_map_inv with (f := fun p : Z * Z => Float (fst p) (snd p));
 auto.
(* Goal: forall (a b : prod Z Z) (_ : @eq float (Float (@fst Z Z a) (@snd Z Z a)) (Float (@fst Z Z b) (@snd Z Z b))), @eq (prod Z Z) a b *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros a1 b1; case a1; case b1; simpl in |- *.
(* Goal: forall (z z0 z1 z2 : Z) (_ : @eq float (Float z1 z2) (Float z z0)), @eq (prod Z Z) (@pair Z Z z1 z2) (@pair Z Z z z0) *)
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
intros z z0 z1 z2 H'0; inversion H'0; auto.
(* Goal: @In float (Float (@fst Z Z (@pair Z Z (Fnum p) (Fexp p))) (@snd Z Z (@pair Z Z (Fnum p) (Fexp p)))) (@map (prod Z Z) float (fun p : prod Z Z => Float (@fst Z Z p) (@snd Z Z p)) (mProd Z Z (prod Z Z) (mZlist (Z.opp (pPred (vNum b))) (pPred (vNum b))) (mZlist (Z.opp (Z.of_N (dExp b))) (Fexp (boundR r))))) *)
generalize H'; case p; auto.
Qed.
(* Some general properties of rounded predicate :
   -Projector A bounded is rounded to something equal to itself 
  - Monotone : the rounded predicate is monotone *)
 
Definition ProjectorP (P : R -> float -> Prop) :=
  forall p q : float, Fbounded b p -> P p q -> p = q :>R.
 
Definition MonotoneP (P : R -> float -> Prop) :=
  forall (p q : R) (p' q' : float),
  (p < q)%R -> P p p' -> P q q' -> (p' <= q')%R.
(* What it is to be a minimum*)
 
Definition isMin (r : R) (min : float) :=
  Fbounded b min /\
  (min <= r)%R /\
  (forall f : float, Fbounded b f -> (f <= r)%R -> (f <= min)%R).
(* Min is a projector *)
 
Theorem isMin_inv1 : forall (p : float) (r : R), isMin r p -> (p <= r)%R.
(* Goal: forall (p : float) (r : R) (_ : isMax r p), Rle r (FtoRradix p) *)
intros p r H; case H; intros H1 H2; case H2; auto.
Qed.
 
Theorem ProjectMin : ProjectorP isMin.
(* Goal: MonotoneP isMax *)
red in |- *.
(* Goal: forall (p q : float) (_ : Fbounded b p) (_ : isMax (FtoRradix p) q), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
 auto with real.
(* Goal: Rle (FtoRradix q) r *)
apply isMin_inv1 with (1 := H'0); auto.
Qed.
(* It is monotone *)
 
Theorem MonotoneMin : MonotoneP isMin.
(* Goal: MonotoneP isMax *)
red in |- *.
(* Goal: forall (p q : R) (p' q' : float) (_ : Rlt p q) (_ : isMax p p') (_ : isMax q q'), Rle (FtoRradix p') (FtoRradix q') *)
intros p q p' q' H' H'0 H'1.
elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3 H'1;
 auto.
(* Goal: Fbounded b q *)
(* Goal: Rle r (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
case H'0; auto.
(* Goal: Rle (FtoRradix p') q *)
apply Rle_trans with p; auto.
(* Goal: Rle (FtoRradix q) r *)
apply isMin_inv1 with (1 := H'0); auto.
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
apply Rlt_le; auto.
Qed.
(* What it is to be a maximum *)
 
Definition isMax (r : R) (max : float) :=
  Fbounded b max /\
  (r <= max)%R /\
  (forall f : float, Fbounded b f -> (r <= f)%R -> (max <= f)%R).
(* It is a projector *)
 
Theorem isMax_inv1 : forall (p : float) (r : R), isMax r p -> (r <= p)%R.
(* Goal: forall (p : float) (r : R) (_ : isMax r p), Rle r (FtoRradix p) *)
intros p r H; case H; intros H1 H2; case H2; auto.
Qed.
 
Theorem ProjectMax : ProjectorP isMax.
(* Goal: MonotoneP isMax *)
red in |- *.
(* Goal: forall (p q : float) (_ : Fbounded b p) (_ : isMax (FtoRradix p) q), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q H' H'0; apply Rle_antisym.
(* Goal: Rle r (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply isMax_inv1 with (1 := H'0); auto.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
 auto with real.
Qed.
(* It is monotone *)
 
Theorem MonotoneMax : MonotoneP isMax.
(* Goal: MonotoneP isMax *)
red in |- *.
(* Goal: forall (p q : R) (p' q' : float) (_ : Rlt p q) (_ : isMax p p') (_ : isMax q q'), Rle (FtoRradix p') (FtoRradix q') *)
intros p q p' q' H' H'0 H'1.
(* Goal: Rle (FtoRradix p') (FtoRradix q') *)
elim H'0; intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3 H'0.
(* Goal: Fbounded b q' *)
(* Goal: Rle p (FtoRradix q') *)
case H'1; auto.
(* Goal: Rle p (FtoRradix q') *)
apply Rle_trans with q; auto.
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
apply Rlt_le; auto.
(* Goal: Rle q (FtoRradix q') *)
apply isMax_inv1 with (1 := H'1); auto.
Qed.
(* Minimun is defined upto equality *)
 
Theorem MinEq :
 forall (p q : float) (r : R), isMin r p -> isMin r q -> p = q :>R.
(* Goal: forall (p q : float) (r : R) (_ : isMax r p) (_ : isMax r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q r H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'0;
 auto.
(* Goal: Fbounded b p *)
(* Goal: Rle r (FtoRradix p) *)
case H'; auto.
(* Goal: Rle (FtoRradix p) r *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply isMin_inv1 with (1 := H'); auto.
elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H';
 auto.
(* Goal: Fbounded b q *)
(* Goal: Rle r (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
case H'0; auto.
(* Goal: Rle (FtoRradix q) r *)
apply isMin_inv1 with (1 := H'0); auto.
Qed.
(* Maximum is defined upto equality *)
 
Theorem MaxEq :
 forall (p q : float) (r : R), isMax r p -> isMax r q -> p = q :>R.
(* Goal: forall (p q : float) (r : R) (_ : isMax r p) (_ : isMax r q), @eq R (FtoRradix p) (FtoRradix q) *)
intros p q r H' H'0; apply Rle_antisym.
elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H';
 auto.
(* Goal: Fbounded b q *)
(* Goal: Rle r (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
case H'0; auto.
(* Goal: Rle r (FtoRradix q) *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply isMax_inv1 with (1 := H'0); auto.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'0;
 auto.
(* Goal: Fbounded b p *)
(* Goal: Rle r (FtoRradix p) *)
case H'; auto.
(* Goal: Rle r (FtoRradix p) *)
apply isMax_inv1 with (1 := H'); auto.
Qed.
(* Min and Max are related *)
 
Theorem MinOppMax :
 forall (p : float) (r : R), isMin r p -> isMax (- r) (Fopp p).
(* Goal: forall (p : float) (r : R) (_ : isMax r p), isMin (Ropp r) (Fopp p) *)
intros p r H'; split.
(* Goal: Fbounded b p *)
(* Goal: Rle r (FtoRradix p) *)
apply oppBounded; case H'; auto.
(* Goal: and (Rle r (FtoRradix (FNSucc b radix precision p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f)) *)
split.
(* Goal: isMin (FtoRradix (Fopp p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (FtoRradix p) r *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply Ropp_le_contravar; apply isMin_inv1 with (1 := H'); auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) (Ropp r)), Rle (FtoRradix f) (FtoRradix (Fopp p)) *)
intros f H'0 H'1.
(* Goal: Rle (FtoRradix f) (FtoRradix (Fopp p)) *)
rewrite <- (Fopp_Fopp f).
(* Goal: Rle (FtoRradix (Fopp p)) (FtoRradix (Fopp (Fopp f))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; rewrite Fopp_correct.
(* Goal: Rle (Ropp (Ropp (FtoR radix f))) (Ropp (FtoR radix p)) *)
apply Ropp_le_contravar.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fopp f)) *)
elim H'.
(* Goal: forall (_ : Fbounded b p) (_ : and (Rle r (FtoRradix p)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix p) (FtoRradix f))), Rle (FtoR radix p) (FtoR radix (Fopp f)) *)
intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3.
(* Goal: Fbounded b p *)
(* Goal: Rle r (FtoRradix p) *)
apply oppBounded; case H'; auto.
(* Goal: isMin r (Fopp (Fopp (FNPred b radix precision p))) *)
rewrite <- (Ropp_involutive r).
(* Goal: Rle (FtoRradix (Fopp p)) (Ropp r) *)
(* Goal: Rlt (Ropp r) (FtoRradix (FNSucc b radix precision (Fopp p))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
Qed.
(* Max and Min are related *)
 
Theorem MaxOppMin :
 forall (p : float) (r : R), isMax r p -> isMin (- r) (Fopp p).
(* Goal: forall (p : float) (r : R) (_ : isMax r p), isMin (Ropp r) (Fopp p) *)
intros p r H'; split.
(* Goal: Fbounded b p *)
(* Goal: Rle r (FtoRradix p) *)
apply oppBounded; case H'; auto.
(* Goal: and (Rle r (FtoRradix (FNSucc b radix precision p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f)) *)
split.
(* Goal: isMin (FtoRradix (Fopp p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle r (FtoRradix p) *)
apply Ropp_le_contravar; apply isMax_inv1 with (1 := H'); auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) (Ropp r)), Rle (FtoRradix f) (FtoRradix (Fopp p)) *)
intros f H'0 H'1.
(* Goal: Rle (FtoRradix f) (FtoRradix (Fopp p)) *)
rewrite <- (Fopp_Fopp f).
(* Goal: Rle (FtoRradix (Fopp (Fopp f))) (FtoRradix (Fopp p)) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
(* Goal: Rle (Ropp (Ropp (FtoR radix f))) (Ropp (FtoR radix p)) *)
apply Ropp_le_contravar.
(* Goal: Rle (FtoR radix p) (Ropp (FtoR radix f)) *)
rewrite <- (Fopp_correct radix f).
(* Goal: Rle (FtoR radix p) (FtoR radix (Fopp f)) *)
elim H'.
(* Goal: forall (_ : Fbounded b p) (_ : and (Rle r (FtoRradix p)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix p) (FtoRradix f))), Rle (FtoR radix p) (FtoR radix (Fopp f)) *)
intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3.
(* Goal: Fbounded b (Fopp f) *)
(* Goal: Rle r (FtoRradix (Fopp f)) *)
apply oppBounded; auto.
(* Goal: isMin r (Fopp (Fopp (FNPred b radix precision p))) *)
rewrite <- (Ropp_involutive r).
(* Goal: Rle (FtoRradix (Fopp p)) (Ropp r) *)
(* Goal: Rlt (Ropp r) (FtoRradix (FNSucc b radix precision (Fopp p))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
Qed.
(* If I have a strict min I can get a max using FNSucc *)
 
Theorem MinMax :
 forall (p : float) (r : R),
 isMin r p -> r <> p :>R -> isMax r (FNSucc b radix precision p).
(* Goal: forall (p : float) (r : R) (_ : isMax r p) (_ : not (@eq R r (FtoRradix p))), isMin r (FNPred b radix precision p) *)
intros p r H' H'0.
(* Goal: and (Rle r (FtoRradix (FNSucc b radix precision p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f)) *)
split.
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply FcanonicBound with (radix := radix); auto with float.
(* Goal: Fcanonic radix b (FNSucc b radix precision p) *)
(* Goal: and (Rle r (FtoRradix (FNSucc b radix precision p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f)) *)
apply FNSuccCanonic; auto.
(* Goal: Fbounded b p *)
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
inversion H'; auto.
(* Goal: and (Rle r (FtoRradix (FNSucc b radix precision p))) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f)) *)
split.
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
case (Rle_or_lt (FNSucc b radix precision p) r); intros H'2; auto.
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
absurd (FNSucc b radix precision p <= p)%R.
(* Goal: not (Rle (FtoRradix f) r) *)
apply Rlt_not_le.
(* Goal: Rlt (FtoRradix p) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix p) *)
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
unfold FtoRradix in |- *; apply FNSuccLt; auto.
(* Goal: Fbounded b p *)
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
inversion H'; auto.
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix p) *)
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
elim H0; intros H'1 H'3; apply H'3; auto.
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply FcanonicBound with (radix := radix); auto with float.
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
apply Rlt_le; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix p) *)
intros f H'2 H'3.
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
replace (FtoRradix f) with (FtoRradix (Fnormalize radix b precision f)).
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
unfold FtoRradix in |- *; apply FNSuccProp; auto.
(* Goal: Fbounded b p *)
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
inversion H'; auto.
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply FcanonicBound with (radix := radix); auto with float.
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply Rlt_le_trans with r; auto.
(* Goal: Rlt (FtoR radix p) r *)
(* Goal: Rle r (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
case (Rle_or_lt r p); auto.
(* Goal: forall _ : Rle r (FtoRradix p), Rlt (FtoR radix p) r *)
(* Goal: Rle r (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
intros H'4; Contradict H'0.
(* Goal: Rle (FtoRradix p) r *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply Rle_antisym; auto; apply isMin_inv1 with (1 := H'); auto.
(* Goal: Rle r (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
rewrite FnormalizeCorrect; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
Qed.
(* Find a minimun in a given list if it exists *)
 
Theorem MinExList :
 forall (r : R) (L : list float),
 (forall f : float, In f L -> (r < f)%R) \/
 (exists min : float,
    In min L /\
    (min <= r)%R /\ (forall f : float, In f L -> (f <= r)%R -> (f <= min)%R)).
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
intros r L; elim L; simpl in |- *; auto.
(* Goal: Rle (FtoR radix p) (FtoR radix (Fopp f)) *)
left; intros f H'; elim H'.
(* Goal: forall (a : float) (l : list float) (_ : or (forall (f : float) (_ : @In float f l), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (@In float min l) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : @In float f l) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min)))))), or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
intros a l H'.
elim H';
 [ intros H'0; clear H'
 | intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2;
    intros H'3 H'4; try exact H'4; clear H'2 E H'0 H' ].
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
case (Rle_or_lt a r); intros H'1.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
right; exists a; repeat split; auto.
intros f H'; elim H';
 [ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ];
 auto with real.
(* Goal: forall _ : Rle (FtoRradix f) r, Rle (FtoRradix f) (FtoRradix a) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
intros H'; Contradict H'; auto with real.
(* Goal: not (Rle (FtoRradix f) r) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
apply Rlt_not_le; auto with real.
left; intros f H'; elim H';
 [ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ]; 
 auto.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
case (Rle_or_lt a min); intros H'5.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
right; exists min; repeat split; auto.
intros f H'; elim H';
 [ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ]; 
 auto.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
case (Rle_or_lt a r); intros H'6.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
right; exists a; repeat split; auto.
intros f H'; elim H';
 [ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ];
 auto with real.
(* Goal: forall _ : Rle (FtoRradix f) r, Rle (FtoRradix f) (FtoRradix a) *)
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
intros H'; apply Rle_trans with (FtoRradix min); auto with real.
(* Goal: or (forall (f : float) (_ : or (@eq float a f) (@In float f l)), Rlt r (FtoRradix f)) (@ex float (fun min : float => and (or (@eq float a min) (@In float min l)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : or (@eq float a f) (@In float f l)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min))))) *)
right; exists min; split; auto; split; auto.
intros f H'; elim H';
 [ intros H'0; elim H'0; clear H' | intros H'0; clear H' ]; 
 auto.
(* Goal: forall _ : Rle (FtoRradix a) r, Rle (FtoRradix a) (FtoRradix min) *)
intros H'; Contradict H'6; auto with real.
(* Goal: not (Rlt r (FtoRradix a)) *)
apply Rle_not_lt; auto.
Qed.
 
Theorem MinEx : forall r : R, exists min : float, isMin r min.
(* Goal: forall r : R, @ex float (fun min : float => isMin r min) *)
intros r.
(* Goal: @ex float (fun min : float => isMin r min) *)
case (MinExList r (mBFloat r)).
(* Goal: forall _ : forall (f : float) (_ : @In float f (mBFloat r)), Rlt r (FtoRradix f), @ex float (fun min : float => isMin r min) *)
(* Goal: forall _ : @ex float (fun min : float => and (@In float min (mBFloat r)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : @In float f (mBFloat r)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min)))), @ex float (fun min : float => isMin r min) *)
intros H'0; absurd (Fopp (boundR r) <= r)%R; auto.
(* Goal: not (Rle (FtoRradix f) r) *)
apply Rlt_not_le.
(* Goal: Rlt r (FtoRradix (Fopp (boundR r))) *)
(* Goal: Rle (FtoRradix (Fopp (boundR r))) r *)
(* Goal: forall _ : @ex float (fun min : float => and (@In float min (mBFloat r)) (and (Rle (FtoRradix min) r) (forall (f : float) (_ : @In float f (mBFloat r)) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min)))), @ex float (fun min : float => isMin r min) *)
apply H'0.
(* Goal: @In float (Fopp (boundR r)) (mBFloat r) *)
(* Goal: Rle (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply mBFadic_correct3; auto.
(* A minimum always exists *)
(* Goal: Rle (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply Rlt_le.
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply boundRCorrect2; auto.
intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2;
 intros H'3 H'4; clear H'2 E H'0.
(* Goal: @ex float (fun min : float => isMin r min) *)
exists min; split; auto.
(* Goal: Fbounded b min *)
(* Goal: and (Rle (FtoRradix min) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min)) *)
apply mBPadic_Fbounded with (r := r); auto.
(* Goal: and (Rle (FtoRradix p) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix p)) *)
split; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix min) *)
intros f H'0 H'2.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
case (Req_dec f 0); intros H'6.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
replace (FtoRradix f) with (FtoRradix (Float 0%nat (- dExp b))).
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply H'4; auto.
(* Goal: @In float (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b)))) (mBFloat r) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) r *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (FtoRradix f) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply mBFadic_correct4; auto.
(* Goal: Rle (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) r *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (FtoRradix f) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
replace (FtoRradix (Float 0%nat (- dExp b))) with (FtoRradix f); auto.
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (FtoRradix f) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
rewrite H'6.
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (IZR Z0) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (FtoRradix f) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
rewrite H'6.
(* Goal: @eq R (FtoRradix (Float (Z.of_nat O) (Z.opp (Z.of_N (dExp b))))) (IZR Z0) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
case (Rle_or_lt f (Fopp (boundR r))); intros H'5.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply Rle_trans with (FtoRradix (Fopp (boundR r))); auto.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply H'4; auto.
(* Goal: @In float (Fopp (boundR r)) (mBFloat r) *)
(* Goal: Rle (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply mBFadic_correct3; auto.
(* Goal: Rle (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply Rlt_le.
(* Goal: Rlt (FtoRradix (Fopp (boundR r))) r *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply boundRCorrect2; auto.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
case (Rle_or_lt (boundR r) f); intros H'7.
(* Goal: not (Rle (FtoRradix f) r) *)
Contradict H'2; apply Rlt_not_le.
(* Goal: Rlt r (FtoRradix f) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply Rlt_le_trans with (FtoRradix (boundR r)); auto.
(* Goal: Rlt r (FtoRradix (boundR r)) *)
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply boundRCorrect1; auto.
(* Goal: Rle (FtoRradix f) (FtoRradix min) *)
apply H'4; auto.
(* Goal: @In float f (mBFloat r) *)
apply mBFadic_correct1; auto.
(* Goal: not (is_Fzero f) *)
Contradict H'6; unfold FtoRradix in |- *; apply is_Fzero_rep1; auto.
Qed.
 
Theorem MaxEx : forall r : R, exists max : float, isMax r max.
(* Goal: forall r : R, @ex float (fun max : float => isMax r max) *)
intros r; case (MinEx r).
(* Goal: forall (x : float) (_ : isMin r x), @ex float (fun max : float => isMax r max) *)
intros x H'.
(* Goal: @ex float (fun max : float => isMax r max) *)
case (Req_dec x r); intros H'1.
(* Goal: @ex float (fun max : float => isMax r max) *)
(* Goal: @ex float (fun max : float => isMax r max) *)
exists x.
(* Goal: isMax r x *)
(* Goal: @ex float (fun max : float => isMax r max) *)
rewrite <- H'1.
(* Goal: isMax (FtoRradix x) x *)
(* Goal: @ex float (fun max : float => isMax r max) *)
red in |- *; split; [ case H' | split ]; auto with real.
(* A maximum always exists *)
(* Goal: @ex float (fun max : float => isMax r max) *)
exists (FNSucc b radix precision x).
(* Goal: isMax (Ropp r) (FNSucc b radix precision (Fopp p)) *)
apply MinMax; auto.
Qed.
 
Theorem MinBinade :
 forall (r : R) (p : float),
 Fbounded b p ->
 (p <= r)%R -> (r < FNSucc b radix precision p)%R -> isMin r p.
(* Goal: forall (r : R) (p : float) (_ : Fbounded b p) (_ : Rle r (FtoRradix p)) (_ : Rlt (FtoRradix (FNPred b radix precision p)) r), isMax r p *)
intros r p H' H'0 H'1.
(* Goal: and (Rle (FtoRradix p) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix p)) *)
split; auto.
(* Goal: and (Rle (FtoRradix p) r) (forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix p)) *)
split; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle (FtoRradix f) r), Rle (FtoRradix f) (FtoRradix p) *)
intros f H'2 H'3.
(* Goal: Rle (FtoRradix f) (FtoRradix p) *)
case (Rle_or_lt f p); auto; intros H'5.
(* Goal: Rle (FtoRradix f) (FtoRradix p) *)
Contradict H'3.
(* If we are between a bound and its successor, it is our minimum *)
(* Goal: not (Rle (FtoRradix f) r) *)
apply Rlt_not_le.
(* Goal: Rlt r (FtoRradix f) *)
apply Rlt_le_trans with (1 := H'1); auto with real.
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
replace (FtoRradix f) with (FtoRradix (Fnormalize radix b precision f)).
unfold FtoRradix in |- *; apply FNSuccProp; auto; try apply FnormalizeCanonic;
 auto.
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto with real.
(* Goal: Fbounded b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: Fcanonic radix b (Fnormalize radix b precision f) *)
(* Goal: Rlt (FtoR radix p) (FtoR radix (Fnormalize radix b precision f)) *)
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
apply FnormalizeCanonic; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto with real.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto with real.
Qed.
 
Theorem FminRep :
 forall p q : float,
 isMin p q -> exists m : Z, q = Float m (Fexp p) :>R.
intros p q H'.
replace (FtoRradix q) with (FtoRradix (Fnormalize radix b precision q)).
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision f)) (FtoRradix f) *)
2: unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
case (Zle_or_lt (Fexp (Fnormalize radix b precision q)) (Fexp p)); intros H'1.
exists (Fnum p).
unfold FtoRradix in |- *; apply FSuccZleEq with (3 := pGivesBound); auto.
(* A min of a float is always represnetable with the same exposant *)
replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto.
replace (FtoR radix (Fnormalize radix b precision q)) with (FtoR radix q);
 [ idtac | rewrite FnormalizeCorrect ]; auto.
(* Goal: Rle (FtoRradix p) r *)
(* Goal: Rle (FtoRradix q) (FtoRradix p) *)
apply isMin_inv1 with (1 := H'); auto.
replace (FSucc b radix precision (Fnormalize radix b precision q)) with
 (FNSucc b radix precision q); [ idtac | case p ]; 
 auto.
replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto.
case (Req_dec p q); intros Eq0.
unfold FtoRradix in Eq0; rewrite Eq0.
apply FNSuccLt; auto.
case (MinMax q p); auto.
intros H'2 H'3; elim H'3; intros H'4 H'5; clear H'3.
case H'4; auto.
intros H'0; absurd (p <= q)%R; rewrite H'0; auto.
apply Rlt_not_le; auto.
(* Goal: Rlt (FtoRradix p) (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix p) *)
(* Goal: Rle r (FtoRradix (FNSucc b radix precision p)) *)
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoRradix f)), Rle (FtoRradix (FNSucc b radix precision p)) (FtoRradix f) *)
unfold FtoRradix in |- *; apply FNSuccLt; auto.
inversion H'.
elim H0; intros H'3 H'6; apply H'6; clear H0; auto.
rewrite <- H'0; auto with real.
exists
 (Fnum
    (Fshift radix (Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
       (Fnormalize radix b precision q))).
pattern (Fexp p) at 2 in |- *;
 replace (Fexp p) with
  (Fexp
     (Fshift radix
        (Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
        (Fnormalize radix b precision q))).
unfold FtoRradix in |- *;
 rewrite <-
  FshiftCorrect
                with
                (n := 
                  Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
               (x := Fnormalize radix b precision q).
case
 (Fshift radix (Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
    (Fnormalize radix b precision q)); auto.
auto with arith.
(* Goal: @eq Z (Z.sub (Fexp q) (Z.of_nat (Z.abs_nat (Z.sub (Fexp q) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))))))) (Z.of_nat (digit radix (Z.of_nat (Z.abs_nat (up (Rabs r)))))) *)
(* Goal: @eq Z (Fnum (boundR r)) (Z.of_nat (S O)) *)
(* Goal: forall (p : Z) (_ : Z.lt (Z.opp (Z.of_nat (S O))) p) (_ : Z.lt p (Z.of_nat (S O))), @eq Z p Z0 *)
(* Goal: forall (_ : not (is_Fzero q)) (_ : Rlt (FtoRradix (Fopp (boundR r))) (FtoRradix q)) (_ : Rlt (FtoRradix q) (FtoRradix (boundR r))) (_ : Fbounded b q), @In float q (mBFloat r) *)
simpl in |- *; rewrite inj_abs; auto with zarith.
Qed.
 
Theorem MaxBinade :
 forall (r : R) (p : float),
 Fbounded b p ->
 (r <= p)%R -> (FNPred b radix precision p < r)%R -> isMax r p.
(* Goal: forall (r : R) (p : float) (_ : Fbounded b p) (_ : Rle r (FtoRradix p)) (_ : Rlt (FtoRradix (FNPred b radix precision p)) r), isMax r p *)
intros r p H' H'0 H'1.
(* Goal: isMin r (Fopp (Fopp (FNPred b radix precision p))) *)
rewrite <- (Ropp_involutive r).
(* Goal: isMax (Ropp (Ropp r)) p *)
rewrite <- (Fopp_Fopp p).
(* Goal: isMax (Ropp (Ropp r)) (Fopp (Fopp p)) *)
apply MinOppMax.
(* Goal: isMin (Ropp r) (Fopp p) *)
apply MinBinade; auto with real float.
(* Goal: Rle (FtoRradix (Fopp p)) (Ropp r) *)
(* Goal: Rlt (Ropp r) (FtoRradix (FNSucc b radix precision (Fopp p))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
(* Same for max *)
(* Goal: Rlt (Ropp r) (FtoRradix (FNSucc b radix precision (Fopp p))) *)
rewrite <- (Fopp_Fopp (FNSucc b radix precision (Fopp p))).
(* Goal: Rlt (Ropp r) (FtoRradix (Fopp (Fopp (FNSucc b radix precision (Fopp p))))) *)
rewrite <- FNPredFopFNSucc; auto.
(* Goal: Rlt (Ropp r) (FtoRradix (Fopp (FNPred b radix precision p))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real arith.
Qed.
 
Theorem MaxMin :
 forall (p : float) (r : R),
 isMax r p -> r <> p :>R -> isMin r (FNPred b radix precision p).
(* Goal: forall (p : float) (r : R) (_ : isMax r p) (_ : not (@eq R r (FtoRradix p))), isMin r (FNPred b radix precision p) *)
intros p r H' H'0.
(* Goal: isMin r (FNPred b radix precision p) *)
rewrite <- (Fopp_Fopp (FNPred b radix precision p)).
(* Goal: isMin r (Fopp (Fopp (FNPred b radix precision p))) *)
rewrite <- (Ropp_involutive r).
(* Goal: isMin (Ropp (Ropp r)) (Fopp (Fopp (FNPred b radix precision p))) *)
apply MaxOppMin.
(* Goal: isMax (Ropp r) (Fopp (FNPred b radix precision p)) *)
rewrite FNPredFopFNSucc; auto.
(* Goal: isMax (Ropp r) (Fopp (Fopp (FNSucc b radix precision (Fopp p)))) *)
rewrite Fopp_Fopp; auto.
(* Taking the pred of a max we get a min *)
(* Goal: isMax (Ropp r) (FNSucc b radix precision (Fopp p)) *)
apply MinMax; auto.
(* Goal: isMin (Ropp (FtoR radix p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
apply MaxOppMin; auto.
(* Goal: not (@eq R (Ropp r) (FtoRradix (Fopp p))) *)
Contradict H'0.
rewrite <- (Ropp_involutive r); rewrite H'0; auto; unfold FtoRradix in |- *;
 rewrite Fopp_correct; auto; apply Ropp_involutive.
Qed.
 
Theorem FmaxRep :
 forall p q : float,
 isMax p q -> exists m : Z, q = Float m (Fexp p) :>R.
(* Goal: forall (p q : float) (_ : isMax (FtoRradix p) q), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
intros p q H'; case (FminRep (Fopp p) (Fopp q)).
(* Goal: isMin (FtoRradix (Fopp p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: isMin (Ropp (FtoR radix p)) (Fopp q) *)
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
apply MaxOppMin; auto.
(* Goal: forall (x : Z) (_ : @eq R (FtoRradix (Fopp q)) (FtoRradix (Float x (Fexp (Fopp p))))), @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
intros x H'0.
(* Goal: @ex Z (fun m : Z => @eq R (FtoRradix q) (FtoRradix (Float m (Fexp p)))) *)
exists (- x)%Z.
(* Goal: @eq R (FtoRradix q) (FtoRradix (Float (Z.opp x) (Fexp p))) *)
rewrite <- (Ropp_involutive (FtoRradix q)).
(* The max of a float can be represented with the same exposant *)
(* Goal: @eq R (Ropp (Ropp (FtoRradix q))) (FtoRradix (Float (Z.opp x) (Fexp p))) *)
unfold FtoRradix in |- *; rewrite <- Fopp_correct.
(* Goal: @eq R (Ropp (FtoR radix (Fopp q))) (FtoR radix (Float (Z.opp x) (Fexp p))) *)
unfold FtoRradix in H'0; rewrite H'0.
(* Goal: @eq R (Ropp (FtoR radix (Float x (Fexp (Fopp p))))) (FtoR radix (Float (Z.opp x) (Fexp p))) *)
unfold FtoR in |- *; simpl in |- *; auto with real.
(* Goal: @eq R (Ropp (Rmult (IZR x) (powerRZ (IZR radix) (Fexp p)))) (Rmult (IZR (Z.opp x)) (powerRZ (IZR radix) (Fexp p))) *)
rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_l_reverse; auto.
Qed.
 
End FMinMax.
Hint Resolve ProjectMax MonotoneMax MinOppMax MaxOppMin MinMax MinBinade
  MaxBinade MaxMin: float.
