(****************************************************************************
                                                                             
          IEEE754  :  Fbound                                                   
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fop.
Section Fbounded_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Coercion Z_of_N: N >-> Z.
 
Record Fbound : Set := Bound {vNum : positive; dExp : N}.
 
Definition Fbounded (b : Fbound) (d : float) :=
  (Zabs (Fnum d) < Zpos (vNum b))%Z /\ (- dExp b <= Fexp d)%Z.
 
Theorem FboundedNum :
 forall (b : Fbound) (p : float),
 Fbounded b p -> (Zabs (Fnum p) < Zpos (vNum b))%Z.
(* Goal: forall (b : Fbound) (p : float) (_ : Fbounded b p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros b p H; case H; intros H1 H2; case H1; auto.
Qed.
 
Theorem FboundedExp :
 forall (b : Fbound) (p : float), Fbounded b p -> (- dExp b <= Fexp p)%Z.
(* Goal: forall (b : Fbound) (p : float) (_ : Fbounded b p), Z.le (Z.opp (Z.of_N (dExp b))) (Fexp p) *)
intros b p H; case H; auto.
Qed.
Hint Resolve FboundedNum FboundedExp: float.
 
Theorem isBounded :
 forall (b : Fbound) (p : float), {Fbounded b p} + {~ Fbounded b p}.
intros b p; case (Z_le_gt_dec (Zpos (vNum b)) (Zabs (Fnum p)));
 intros H'.
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
right; red in |- *; intros H'3; Contradict H'; auto with float zarith.
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
case (Z_le_gt_dec (- dExp b) (Fexp p)); intros H'1.
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
left; repeat split; auto with zarith.
(* Goal: sumbool (Fbounded b p) (not (Fbounded b p)) *)
right; red in |- *; intros H'3; Contradict H'1; auto with float zarith.
Qed.
 
Theorem FzeroisZero : forall b : Fbound, Fzero (- dExp b) = 0%R :>R.
(* Goal: forall b : Fbound, @eq R (FtoRradix (Fzero (Z.opp (Z.of_N (dExp b))))) (IZR Z0) *)
intros b; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
Qed.
 
Theorem FboundedFzero : forall b : Fbound, Fbounded b (Fzero (- dExp b)).
(* Goal: forall b : Fbound, Fbounded b (Fzero (Z.opp (Z.of_N (dExp b)))) *)
intros b; repeat (split; simpl in |- *).
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) *)
replace 0%Z with (- 0%nat)%Z; [ idtac | simpl in |- *; auto ].
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.opp (Z.of_N (dExp b))) *)
apply Zeq_le; auto with arith.
Qed.
Hint Unfold Fbounded.
 
Theorem FboundedZeroSameExp :
 forall (b : Fbound) (p : float), Fbounded b p -> Fbounded b (Fzero (Fexp p)).
(* Goal: forall (b : Fbound) (p : float) (_ : Fbounded b p), Fbounded b (Fzero (Fexp p)) *)
intros b p H'; (repeat split; simpl in |- *; auto with float zarith).
Qed.
 
Theorem FBoundedScale :
 forall (b : Fbound) (p : float) (n : nat),
 Fbounded b p -> Fbounded b (Float (Fnum p) (Fexp p + n)).
(* Goal: forall (b : Fbound) (p : float) (n : nat) (_ : Fbounded b p), Fbounded b (Float (Fnum p) (Z.add (Fexp p) (Z.of_nat n))) *)
intros b p n H'; repeat split; simpl in |- *; auto with float.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.add (Fexp p) (Z.of_nat n)) *)
apply Zle_trans with (Fexp p); auto with float.
pattern (Fexp p) at 1 in |- *;
 (replace (Fexp p) with (Fexp p + 0%nat)%Z; [ idtac | simpl in |- *; ring ]).
(* Goal: Z.le (Z.add (Fexp p) (Z.of_nat O)) (Z.add (Fexp p) (Z.of_nat n)) *)
apply Zplus_le_compat_l.
(* Goal: Z.le (Z.of_nat O) (Z.of_nat n) *)
apply inj_le; auto with arith.
Qed.
 
Theorem FvalScale :
 forall (b : Fbound) (p : float) (n : nat),
 Float (Fnum p) (Fexp p + n) = (powerRZ radix n * p)%R :>R.
(* Goal: forall (_ : Fbound) (p : float) (n : nat), @eq R (FtoRradix (Float (Fnum p) (Z.add (Fexp p) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (FtoRradix p)) *)
intros b p n; unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Z.add (Fexp p) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite powerRZ_add; auto with real zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
ring.
Qed.
 
Theorem oppBounded :
 forall (b : Fbound) (x : float), Fbounded b x -> Fbounded b (Fopp x).
(* Goal: forall (b : Fbound) (x : float) (_ : Fbounded b x), Fbounded b (Fopp x) *)
intros b x H'; repeat split; simpl in |- *; auto with float zarith.
(* Goal: Z.lt (Z.abs (Z.opp (Fnum x))) (Zpos (vNum b)) *)
replace (Zabs (- Fnum x)) with (Zabs (Fnum x)); auto with float.
(* Goal: @eq Z (Z.abs (Fnum x)) (Z.abs (Z.opp (Fnum x))) *)
case (Fnum x); simpl in |- *; auto.
Qed.
 
Theorem oppBoundedInv :
 forall (b : Fbound) (x : float), Fbounded b (Fopp x) -> Fbounded b x.
(* Goal: forall (b : Fbound) (x : float) (_ : Fbounded b (Fopp x)), Fbounded b x *)
intros b x H'; rewrite <- (Fopp_Fopp x).
(* Goal: Fbounded b (Fopp r) *)
(* Goal: @eq Z (Fexp (Fopp r)) z *)
apply oppBounded; auto.
Qed.
 
Theorem FopRepAux :
 forall (b : Fbound) (z : Z) (p : R),
 ex (fun r : float => r = (- p)%R :>R /\ Fbounded b r /\ Fexp r = z) ->
 ex (fun r : float => r = p :>R /\ Fbounded b r /\ Fexp r = z).
intros b z p H'; elim H'; intros r E; elim E; intros H'0 H'1; elim H'1;
 intros H'2 H'3; clear H'1 E H'.
(* Goal: @ex float (fun r : float => and (@eq R (FtoRradix r) p) (and (Fbounded b r) (@eq Z (Fexp r) z))) *)
exists (Fopp r); split; auto.
(* Goal: @eq R (FtoRradix (Fopp r)) p *)
(* Goal: and (Fbounded b (Fopp r)) (@eq Z (Fexp (Fopp r)) z) *)
rewrite <- (Ropp_involutive p).
(* Goal: @eq R (FtoRradix (Fopp r)) (Ropp (Ropp p)) *)
(* Goal: and (Fbounded b (Fopp r)) (@eq Z (Fexp (Fopp r)) z) *)
rewrite <- H'0; auto.
(* Goal: @eq R (FtoRradix (Fopp r)) (Ropp (FtoRradix r)) *)
(* Goal: and (Fbounded b (Fopp r)) (@eq Z (Fexp (Fopp r)) z) *)
unfold FtoRradix in |- *; apply Fopp_correct; auto.
(* Goal: Fbounded b q *)
split.
(* Goal: Fbounded b (Fopp r) *)
(* Goal: @eq Z (Fexp (Fopp r)) z *)
apply oppBounded; auto.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix m f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
simpl in |- *; auto.
Qed.
 
Theorem absFBounded :
 forall (b : Fbound) (f : float), Fbounded b f -> Fbounded b (Fabs f).
(* Goal: forall (b : Fbound) (f : float) (_ : Fbounded b f), Fbounded b (Fabs f) *)
intros b f H'; repeat split; simpl in |- *; auto with float.
(* Goal: Z.lt (Z.abs (Z.abs (Fnum f))) (Zpos (vNum b)) *)
replace (Zabs (Zabs (Fnum f))) with (Zabs (Fnum f)); auto with float.
(* Goal: @eq Z (Z.abs (Fnum f)) (Z.abs (Z.abs (Fnum f))) *)
case (Fnum f); auto.
Qed.
 
Theorem FboundedEqExpPos :
 forall (b : Fbound) (p q : float),
 Fbounded b p ->
 p = q :>R -> (Fexp p <= Fexp q)%R -> (0 <= q)%R -> Fbounded b q.
(* Goal: forall (b : Fbound) (p q : float) (_ : Fbounded b p) (_ : @eq R (FtoRradix p) (FtoRradix q)) (_ : Rle (IZR (Fexp p)) (IZR (Fexp q))) (_ : Rle (IZR Z0) (FtoRradix q)), Fbounded b q *)
intros b p q H' H'0 H'1 H'2.
cut (0 <= Fnum p)%Z;
 [ intros Z1
 | apply (LeR0Fnum radix); auto with real arith; fold FtoRradix in |- *;
    rewrite H'0; auto ].
cut (0 <= Fnum q)%Z;
 [ intros Z2 | apply (LeR0Fnum radix); auto with real arith ].
(* Goal: Fbounded b q *)
split.
(* Goal: Z.lt (Z.abs (Fnum q)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
(* Goal: Z.le (Z.abs (Fnum q)) (Z.abs (Fnum p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
repeat rewrite Zabs_eq; auto.
apply Zle_trans with (Fnum (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q));
 auto.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix m f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
unfold Fshift in |- *; simpl in |- *; auto.
pattern (Fnum q) at 1 in |- *; replace (Fnum q) with (Fnum q * 1)%Z;
 auto with zarith.
(* Goal: Z.le (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fnum p) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply (Rle_Fexp_eq_Zle radix); auto with real zarith.
(* Goal: Rle (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (FtoR radix p) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite FshiftCorrect; auto with real zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
unfold Fshift in |- *; simpl in |- *; rewrite inj_abs; try ring.
(* Goal: Z.le Z0 (Z.sub (Fexp q) (Fexp p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply Zle_Zminus_ZERO; apply le_IZR; auto with real arith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply Zle_trans with (Fexp p).
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
case H'; auto.
(* Goal: Z.le (Fexp p) (Fexp q) *)
apply le_IZR; auto with real arith.
Qed.
 
Theorem FboundedEqExp :
 forall (b : Fbound) (p q : float),
 Fbounded b p -> p = q :>R -> (Fexp p <= Fexp q)%R -> Fbounded b q.
(* Goal: Fbounded b q *)
intros b p q H' H'0 H'1; split.
(* Goal: Z.lt (Z.abs (Fnum q)) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
apply
 Zle_trans with (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)));
 auto.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix m f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
unfold Fshift in |- *; simpl in |- *; auto.
(* Goal: Z.le (Z.abs (Fnum q)) (Z.abs (Z.mul (Fnum q) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p)))))) *)
(* Goal: Z.le (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))) (Z.abs (Fnum p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite Zabs_Zmult.
pattern (Zabs (Fnum q)) at 1 in |- *;
 replace (Zabs (Fnum q)) with (Zabs (Fnum q) * 1%nat)%Z;
 [ apply Zle_Zmult_comp_l | auto with zarith ]; auto with zarith.
(* Goal: Z.le (Z.of_nat (S O)) (Z.abs (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))))) *)
(* Goal: @eq Z (Z.mul (Z.abs (Fnum q)) (Z.of_nat (S O))) (Z.abs (Fnum q)) *)
(* Goal: Z.le (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))) (Z.abs (Fnum p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite Zabs_eq; simpl in |- *; auto with zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
simpl in |- *; ring.
(* Goal: Z.le (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))) (Z.abs (Fnum p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
cut (Fexp p <= Fexp q)%Z; [ intros E2 | idtac ].
(* Goal: Z.le (Z.abs x) (Z.abs y) *)
apply le_IZR; auto.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
pattern (Fexp p) at 2 in |- *;
 replace (Fexp p) with (Fexp (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q));
 auto.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)))) (powerRZ (IZR radix) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite <- (fun x => Rabs_pos_eq (powerRZ radix x)); auto with real zarith.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)))) (Rabs (powerRZ (IZR radix) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite <- Faux.Rabsolu_Zabs.
(* Goal: Rle (Rmult (Rabs (IZR (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)))) (Rabs (powerRZ (IZR radix) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite <- Rabs_mult.
change
  (Rabs (FtoRradix (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)) <=
   Zabs (Fnum p) * powerRZ radix (Fexp p))%R in |- *.
(* Goal: Rle (Rabs (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
(* Goal: Rle (Rabs (FtoR radix q)) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
fold FtoRradix in |- *; rewrite <- H'0.
(* Goal: Rle (Rabs (FtoRradix p)) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite <- (Fabs_correct radix); auto with real zarith.
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.sub (Fexp q) (Z.of_nat (Z.abs_nat (Z.sub (Fexp q) (Fexp p))))) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
rewrite inj_abs; [ ring | auto with zarith ].
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
cut (Fexp p <= Fexp q)%Z; [ intros E2 | apply le_IZR ]; auto.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply Zle_trans with (Fexp p); [ idtac | apply le_IZR ]; auto with float.
Qed.
 
Theorem eqExpLess :
 forall (b : Fbound) (p q : float),
 Fbounded b p ->
 p = q :>R ->
 exists r : float, Fbounded b r /\ r = q :>R /\ (Fexp q <= Fexp r)%R.
(* Goal: forall (b : Fbound) (p q : float) (_ : Fbounded b p) (_ : @eq R (FtoRradix p) (FtoRradix q)), @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix q)) (Rle (IZR (Fexp q)) (IZR (Fexp r))))) *)
intros b p q H' H'0.
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix q)) (Rle (IZR (Fexp q)) (IZR (Fexp r))))) *)
case (Rle_or_lt (Fexp q) (Fexp p)); intros H'1.
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix q)) (Rle (IZR (Fexp q)) (IZR (Fexp r))))) *)
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix q)) (Rle (IZR (Fexp q)) (IZR (Fexp r))))) *)
exists p; repeat (split; auto).
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix q)) (Rle (IZR (Fexp q)) (IZR (Fexp r))))) *)
exists q; split; [ idtac | split ]; auto with real.
(* Goal: Fbounded b q *)
apply FboundedEqExp with (p := p); auto.
(* Goal: Rle (IZR (Fexp p)) (IZR (Fexp q)) *)
apply Rlt_le; auto.
Qed.
 
Theorem FboundedShiftLess :
 forall (b : Fbound) (f : float) (n m : nat),
 m <= n -> Fbounded b (Fshift radix n f) -> Fbounded b (Fshift radix m f).
(* Goal: forall (b : Fbound) (f : float) (n m : nat) (_ : le m n) (_ : Fbounded b (Fshift radix n f)), Fbounded b (Fshift radix m f) *)
intros b f n m H' H'0; split; auto.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix m f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
simpl in |- *; auto.
(* Goal: Z.lt (Z.abs (Z.mul (Fnum f) (Zpower_nat radix m))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
apply Zle_lt_trans with (Zabs (Fnum (Fshift radix n f))).
(* Goal: Z.le (Z.abs (Z.mul (Fnum f) (Zpower_nat radix m))) (Z.abs (Fnum (Fshift radix n f))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
simpl in |- *; replace m with (m + 0); auto with arith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum f) (Zpower_nat radix (Init.Nat.add m O)))) (Z.abs (Z.mul (Fnum f) (Zpower_nat radix n))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
replace n with (m + (n - m)); auto with arith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum f) (Zpower_nat radix (Init.Nat.add m O)))) (Z.abs (Z.mul (Fnum f) (Zpower_nat radix (Init.Nat.add m (Init.Nat.sub n m))))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
repeat rewrite Zpower_nat_is_exp.
(* Goal: Z.le (Z.abs (Z.mul (Fnum f) (Z.mul (Zpower_nat radix m) (Zpower_nat radix O)))) (Z.abs (Z.mul (Fnum f) (Z.mul (Zpower_nat radix m) (Zpower_nat radix (Init.Nat.sub n m))))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
repeat rewrite Zabs_Zmult; auto.
(* Goal: Z.le (Z.mul (Z.abs (Zpower_nat radix m)) (Z.abs (Zpower_nat radix O))) (Z.mul (Z.abs (Zpower_nat radix m)) (Z.abs (Zpower_nat radix (Init.Nat.sub n m)))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
apply Zle_Zmult_comp_l; auto with zarith.
(* Goal: Z.le (Z.mul (Z.abs (Zpower_nat radix m)) (Z.abs (Zpower_nat radix O))) (Z.mul (Z.abs (Zpower_nat radix m)) (Z.abs (Zpower_nat radix (Init.Nat.sub n m)))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
apply Zle_Zmult_comp_l; auto with zarith.
(* Goal: Z.le (Z.abs (Zpower_nat radix O)) (Z.abs (Zpower_nat radix (Init.Nat.sub n m))) *)
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
repeat rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix n f))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
case H'0; auto.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix m f)) *)
apply Zle_trans with (Fexp (Fshift radix n f)); auto with float.
(* Goal: Z.le (Fexp (Fshift radix n f)) (Fexp (Fshift radix m f)) *)
simpl in |- *; unfold Zminus in |- *; auto with zarith.
Qed.
 
Theorem eqExpMax :
 forall (b : Fbound) (p q : float),
 Fbounded b p ->
 Fbounded b q ->
 (Fabs p <= q)%R ->
 exists r : float, Fbounded b r /\ r = p :>R /\ (Fexp r <= Fexp q)%Z.
(* Goal: forall (b : Fbound) (p q : float) (_ : Fbounded b p) (_ : Fbounded b q) (_ : Rle (FtoRradix (Fabs p)) (FtoRradix q)), @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix p)) (Z.le (Fexp r) (Fexp q)))) *)
intros b p q H' H'0 H'1; case (Zle_or_lt (Fexp p) (Fexp q)); intros Rl0.
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix p)) (Z.le (Fexp r) (Fexp q)))) *)
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix p)) (Z.le (Fexp r) (Fexp q)))) *)
exists p; auto.
cut ((Fexp p - Zabs_nat (Fexp p - Fexp q))%Z = Fexp q);
 [ intros Eq1 | idtac ].
(* Goal: @ex float (fun r : float => and (Fbounded b r) (and (@eq R (FtoRradix r) (FtoRradix p)) (Z.le (Fexp r) (Fexp q)))) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
exists (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p); split; split; auto.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
apply Zle_lt_trans with (Fnum q); auto with float.
replace (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p))) with
 (Fnum (Fabs (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p))); 
 auto.
(* Goal: Z.le (Fnum (Fabs (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p))) (Fnum q) *)
(* Goal: Z.lt (Fnum q) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
apply (Rle_Fexp_eq_Zle radix); auto with arith.
rewrite Fabs_correct; auto with arith; rewrite FshiftCorrect; auto with arith;
 rewrite <- (Fabs_correct radix); auto with float arith.
(* Goal: Z.lt (Fnum q) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
rewrite <- (Zabs_eq (Fnum q)); auto with float zarith.
(* Goal: Z.le Z0 (Fnum q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
apply (LeR0Fnum radix); auto.
(* Goal: Rle (IZR Z0) (FtoR radix q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
apply Rle_trans with (2 := H'1); auto with real.
(* Goal: Rle (IZR Z0) (FtoRradix (Fabs p)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
rewrite (Fabs_correct radix); auto with real zarith.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) *)
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
unfold Fshift in |- *; simpl in |- *; rewrite Eq1; auto with float.
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
(* Goal: Z.le (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: Z.le (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
rewrite Eq1; auto with zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite inj_abs; auto with zarith; ring.
Qed.
 
Theorem Zle_monotony_contra_abs_pow :
 forall x y z n : Z,
 (0 < z)%Z ->
 (Rabs (x * powerRZ z n) <= Rabs (y * powerRZ z n))%R -> (Zabs x <= Zabs y)%Z.
(* Goal: forall (x y z n : Z) (_ : Z.lt Z0 z) (_ : Rle (Rabs (Rmult (IZR x) (powerRZ (IZR z) n))) (Rabs (Rmult (IZR y) (powerRZ (IZR z) n)))), Z.le (Z.abs x) (Z.abs y) *)
intros x y z n Hz O1.
(* Goal: Z.le (Z.abs x) (Z.abs y) *)
apply le_IZR; auto.
(* Goal: Rle (IZR (Z.abs x)) (IZR (Z.abs y)) *)
apply Rmult_le_reg_l with (r := powerRZ z n); auto with real zarith.
(* Goal: Rle (Rmult (powerRZ (IZR z) n) (IZR (Z.abs x))) (Rmult (powerRZ (IZR z) n) (IZR (Z.abs y))) *)
repeat rewrite (Rmult_comm (powerRZ z n)); auto.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)))) (Rabs (powerRZ (IZR radix) (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q))))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp q) (Fexp p))) q)) (Fexp p) *)
(* Goal: Z.le (Fexp p) (Fexp q) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
repeat rewrite <- Faux.Rabsolu_Zabs.
(* Goal: Rle (Rmult (Rabs (IZR x)) (powerRZ (IZR z) n)) (Rmult (Rabs (IZR y)) (powerRZ (IZR z) n)) *)
replace (powerRZ z n) with (Rabs (powerRZ z n)).
(* Goal: Rle (Rmult (Rabs (IZR x)) (Rabs (powerRZ (IZR z) n))) (Rmult (Rabs (IZR y)) (Rabs (powerRZ (IZR z) n))) *)
(* Goal: @eq R (Rabs (powerRZ (IZR z) n)) (powerRZ (IZR z) n) *)
repeat rewrite <- Rabs_mult; auto.
(* Goal: @eq R (Rabs (powerRZ (IZR z) n)) (powerRZ (IZR z) n) *)
apply Rabs_pos_eq; auto with real zarith.
Qed.
 
Theorem LessExpBound :
 forall (b : Fbound) (p q : float),
 Fbounded b p ->
 Fbounded b q ->
 (Fexp q <= Fexp p)%Z ->
 (0 <= p)%R ->
 (p <= q)%R ->
 exists m : Z,
   Float m (Fexp q) = p :>R /\ Fbounded b (Float m (Fexp q)).
intros b p q H' H'0 H'1 H'2 H'3;
 exists (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p - Fexp q)))%Z.
cut
 (Float (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p - Fexp q))) (Fexp q) = p
  :>R); [ intros Eq1 | idtac ].
(* Goal: and (@eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p)) (Fbounded b (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
split; auto.
(* Goal: Fbounded b (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q)) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
repeat split; simpl in |- *; auto with float.
(* Goal: Z.lt (Z.abs (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q)))))) (Zpos (vNum b)) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
apply Zle_lt_trans with (Zabs (Fnum q)); auto with float.
apply Zle_monotony_contra_abs_pow with (z := radix) (n := Fexp q);
 auto with real arith.
(* Goal: Rle (Rabs (Rmult (IZR (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q)))))) (powerRZ (IZR radix) (Fexp q)))) (Rabs (Rmult (IZR (Fnum q)) (powerRZ (IZR radix) (Fexp q)))) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
unfold FtoRradix, FtoR in Eq1; simpl in Eq1; rewrite Eq1; auto with real.
(* Goal: Rle (Rabs (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) (Rabs (Rmult (IZR (Fnum q)) (powerRZ (IZR radix) (Fexp q)))) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
change (Rabs p <= Rabs q)%R in |- *.
(* Goal: Rle (Rabs (FtoRradix p)) (Rabs (FtoRradix q)) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
repeat rewrite Rabs_pos_eq; auto with real.
(* Goal: Rle (IZR Z0) (FtoRradix q) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
apply Rle_trans with (1 := H'2); auto.
pattern (Fexp q) at 2 in |- *;
 replace (Fexp q) with (Fexp p - Zabs_nat (Fexp p - Fexp q))%Z.
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))))) (FtoRradix p) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
change (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p = p :>R) in |- *.
(* Goal: @eq R (FtoRradix (Fshift radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))) p)) (FtoRradix p) *)
(* Goal: @eq Z (Z.sub (Fexp p) (Z.of_nat (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q) *)
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite inj_abs; auto with zarith; ring.
Qed.
 
Theorem maxFbounded :
 forall (b : Fbound) (z : Z),
 (- dExp b <= z)%Z -> Fbounded b (Float (Zpred (Zpos (vNum b))) z).
(* Goal: and (@eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p)) (Fbounded b (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) *)
(* Goal: @eq R (FtoRradix (Float (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp p) (Fexp q))))) (Fexp q))) (FtoRradix p) *)
intros b z H; split; auto.
(* Goal: Z.lt (Z.abs (Fnum (Float (Z.pred (Zpos (vNum b))) z))) (Zpos (vNum b)) *)
change (Zabs (Zpred (Zpos (vNum b))) < Zpos (vNum b))%Z in |- *.
(* Goal: Z.lt (Z.abs (Z.pred (Zpos (vNum b)))) (Zpos (vNum b)) *)
rewrite Zabs_eq; auto with zarith.
Qed.
 
Theorem maxMax :
 forall (b : Fbound) (p : float) (z : Z),
 Fbounded b p ->
 (Fexp p <= z)%Z -> (Fabs p < Float (Zpos (vNum b)) z)%R.
intros b p z H' H'0; unfold FtoRradix in |- *;
 rewrite <-
  (FshiftCorrect _ radixMoreThanOne (Zabs_nat (z - Fexp p))
     (Float (Zpos (vNum b)) z)); unfold Fshift in |- *.
change
  (FtoR radix (Fabs p) <
   FtoR radix
     (Float (Zpos (vNum b) * Zpower_nat radix (Zabs_nat (z - Fexp p)))
        (z - Zabs_nat (z - Fexp p))))%R in |- *.
(* Goal: Rlt (FtoR radix (Fabs p)) (FtoR radix (Float (Z.mul (Zpos (vNum b)) (Zpower_nat radix (Z.abs_nat (Z.sub z (Fexp p))))) (Z.sub z (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p))))))) *)
replace (z - Zabs_nat (z - Fexp p))%Z with (Fexp p).
(* Goal: Rlt (FtoR radix (Fabs p)) (FtoR radix (Float (Z.mul (Zpos (vNum b)) (Zpower_nat radix (Z.abs_nat (Z.sub z (Fexp p))))) (Fexp p))) *)
(* Goal: @eq Z (Fexp p) (Z.sub z (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p))))) *)
unfold Fabs, FtoR in |- *.
change
  (Zabs (Fnum p) * powerRZ radix (Fexp p) <
   (Zpos (vNum b) * Zpower_nat radix (Zabs_nat (z - Fexp p)))%Z *
   powerRZ radix (Fexp p))%R in |- *.
(* Goal: Rlt (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Z.mul (Zpos (vNum b)) (Zpower_nat radix (Z.abs_nat (Z.sub z (Fexp p)))))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Fexp p) (Z.sub z (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p))))) *)
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum b)));
 auto with real float zarith.
pattern (Zpos (vNum b)) at 1 in |- *;
 replace (Zpos (vNum b)) with (Zpos (vNum b) * 1)%Z;
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
 auto with real float zarith; ring.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (Rmult (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) (Z.of_nat n)))) (Rmult (powerRZ (IZR radix) (Z.of_nat n)) (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite inj_abs; auto with zarith; ring.
Qed.
End Fbounded_Def.
Hint Resolve FboundedFzero oppBounded absFBounded maxFbounded FboundedNum
  FboundedExp: float.