Library Float.Ct2.FboundI

Require Export AllFloat.

Section FboundedI_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

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

Record FboundI : Set := BoundI {vNumInf : nat; vNumSup : nat; dExpI : nat}.

Definition FboundedI (b : FboundI) (d : float) :=
  ((- vNumInf b <= Fnum d)%Z /\ (Fnum d <= vNumSup b)%Z) /\
  (- dExpI b <= Fexp d)%Z.

Theorem isBoundedI :
 forall (b : FboundI) (p : float), {FboundedI b p} + {~ FboundedI b p}.
intros b p; case (Z_le_gt_dec (Fnum p) (vNumSup b)); intros H'.
case (Z_le_gt_dec (- vNumInf b) (Fnum p)); intros H'0.
case (Z_le_gt_dec (- dExpI b) (Fexp p)); intros H'1.
left; repeat split; auto.
right; red in |- *; intros H'3; absurd (- dExpI b > Fexp p)%Z; elim H'3;
 auto with zarith.
right; red in |- *; intros H'1; absurd (- vNumInf b > Fnum p)%Z; elim H'1;
 auto with zarith.
right; red in |- *; intros H'0; absurd (Fnum p > vNumSup b)%Z; elim H'0;
 auto with zarith.
Qed.

Theorem FboundedIFzero : forall b : FboundI, FboundedI b (Fzero (- dExpI b)).
intros b; repeat (split; simpl in |- *).
replace 0%Z with (- 0%nat)%Z; [ idtac | simpl in |- *; auto ].
apply Zle_Zopp; apply inj_le; auto with arith.
replace 0%Z with (Z_of_nat 0); [ idtac | simpl in |- *; auto ].
apply inj_le; auto with arith.
auto with zarith.
Qed.

Definition FnormalI (b : FboundI) (p : float) :=
  FboundedI b p /\
  ((vNumSup b < radix * Fnum p)%R \/ (radix * Fnum p < (- vNumInf b)%Z)%R).

Theorem FnormalINotZero :
 forall (b : FboundI) (p : float), FnormalI b p -> ~ is_Fzero p.
intros b p H; elim H; intros H1 H2; unfold is_Fzero in |- *.
case (Z_zerop (Fnum p)); auto; intros H3.
generalize H2; rewrite H3.
replace (radix * 0%Z)%R with 0%R; [ idtac | simpl; ring ].
clear H2; intros H2.
case H2; intros H4; clear H2.
absurd (vNumSup b < 0)%R; auto with arith real.
apply Rle_not_lt; auto with zarith real.
absurd (0 < (- vNumInf b)%Z)%R; auto.
apply Rle_not_lt; replace 0%R with (IZR (- (0))); auto with arith.
apply Rle_IZR; apply Zle_Zopp; auto with zarith.
Qed.

Theorem FnormalIUnique_aux :
 forall (b : FboundI) (p q : float),
 FnormalI b p ->
 FnormalI b q -> p = q :>R -> (Fexp p < Fexp q)%Z -> p = q :>float.
intros b p q Hp Hq H H'.
absurd (p = q :>R); auto.
elim Hq; intros H3 H4; case H4; clear H4; intros H4.
apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
apply Rle_lt_trans with (vNumSup b * powerRZ radix (Fexp p))%R.
apply Rmult_le_compat_r.
apply powerRZ_le; auto with real zarith.
rewrite INR_IZR_INZ; apply Rle_IZR; elim Hp; intros V1 V2; elim V1;
 intros V3 V4; elim V3; auto with zarith.
apply Rle_lt_trans with (vNumSup b * powerRZ radix (Fexp q - 1%nat))%R.
apply Rmult_le_compat_l.
replace 0%R with (INR 0); auto with real arith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
unfold Zminus in |- *; rewrite powerRZ_add; auto with real zarith.
replace (radix * (Fnum q * powerRZ radix (Fexp q)))%R with
 (radix * Fnum q * powerRZ radix (Fexp q))%R; [ idtac | ring ].
replace
 (radix * (vNumSup b * (powerRZ radix (Fexp q) * powerRZ radix (- 1%nat))))%R
 with (vNumSup b * powerRZ radix (Fexp q))%R.
apply Rmult_lt_compat_r; auto with real zarith.
simpl in |- *;
 apply
  trans_eq with (radix * / radix * (vNumSup b * powerRZ radix (Fexp q)))%R.
rewrite Rinv_r; auto with real zarith.
replace (radix * 1)%R with (IZR radix); ring; ring.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
replace (Fnum q * powerRZ radix (Fexp q))%R with
 (radix * Fnum q * powerRZ radix (Fexp q + - 1%nat))%R.
apply
 Rlt_le_trans with ((- vNumInf b)%Z * powerRZ radix (Fexp q + - 1%nat))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_trans with ((- vNumInf b)%Z * powerRZ radix (Fexp p))%R.
rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_l_reverse;
 rewrite Ropp_mult_distr_l_reverse; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real arith zarith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q + - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_IZR; unfold FnormalI in Hp; unfold FboundedI in Hp; intuition.
rewrite powerRZ_add; auto with real zarith arith.
simpl in |- *; replace (radix * 1)%R with (IZR radix); simpl; try ring.
field; auto with zarith real.
Qed.

Theorem FnormalIUnique :
 forall (b : FboundI) (p q : float),
 FnormalI b p -> FnormalI b q -> p = q :>R -> p = q :>float.
intros b p q Hp Hq H.
case (Zle_or_lt (Fexp p) (Fexp q)); intros H1.
cut (forall a b : Z, (a <= b)%Z -> a = b \/ (a < b)%Z);
 [ intros F | idtac ].
2: intros x y V; omega.
lapply (F (Fexp p) (Fexp q)); [ intros H'1 | auto ].
case H'1; intros H2; clear F H'1.
apply sameExpEq with radix; auto.
apply FnormalIUnique_aux with b; auto.
apply sym_eq; apply FnormalIUnique_aux with b; auto.
Qed.

Definition FsubnormalI (b : FboundI) (p : float) :=
  FboundedI b p /\
  Fexp p = (- dExpI b)%Z /\
  ((- vNumInf b)%Z <= radix * Fnum p)%R /\ (radix * Fnum p <= vNumSup b)%R.

Theorem FsubnormalIUnique :
 forall (b : FboundI) (p q : float),
 FsubnormalI b p -> FsubnormalI b q -> p = q :>R -> p = q :>float.
intros b p q Hp Hq H.
apply sameExpEq with radix; auto with zarith.
elim Hp; intros H0 H1; elim H1; clear H1; intros H1 H2.
elim Hq; intros H4 H5; elim H5; clear H5; intros H5 H6.
auto with zarith.
Qed.

Theorem NormalIandSubnormalINotEq :
 forall (b : FboundI) (p q : float),
 FnormalI b p -> FsubnormalI b q -> p <> q :>R.
intros b p q Hp Hq.
elim Hp; intros H1 H2; elim Hq; intros H4 H3.
elim H3; intros H5 H6; clear H3.
elim H6; intros H3 H7; clear H6.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
rewrite H5.
case H2; intros H8.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
apply Rlt_le_trans with (Fnum p * powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rle_lt_trans with (INR (vNumSup b)); auto.
apply Rmult_le_compat_l.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix * 0)%R with (INR 0); auto with real arith.
apply Rle_trans with (INR (vNumSup b)); auto with real arith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
apply Rlt_dichotomy_converse; left.
apply Ropp_lt_cancel.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rlt_le_trans with (- Fnum p * powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Ropp_lt_gt_contravar.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rlt_le_trans with (IZR (- vNumInf b)); auto with real arith.
apply Rmult_le_compat_l.
replace 0%R with (-0)%R; auto with real; apply Ropp_le_contravar.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix * 0)%R with 0%R; auto with real.
apply Rle_trans with (IZR (- vNumInf b)); auto with real arith.
replace 0%R with (IZR 0); auto with real arith zarith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
Qed.

Definition FcanonicI (b : FboundI) (a : float) :=
  FnormalI b a \/ FsubnormalI b a.

Theorem FcanonicIUnique :
 forall (b : FboundI) (p q : float),
 FcanonicI b p -> FcanonicI b q -> p = q :>R -> p = q :>float.
intros b p q Hp Hq H; case Hp; case Hq; intros H1 H2.
apply FnormalIUnique with b; auto.
Contradict H; apply NormalIandSubnormalINotEq with b; auto.
Contradict H; apply not_eq_sym; apply NormalIandSubnormalINotEq with b; auto.
apply FsubnormalIUnique with b; auto.
Qed.

Theorem Zpower_nat_S :
 forall n : nat, Zpower_nat radix (S n) = (radix * Zpower_nat radix n)%Z.
intros n; replace (S n) with (1 + n); auto with arith.
Qed.

Fixpoint FNIAux (v N q : nat) {struct q} : nat :=
  match q with
  | O => 0
  | S q' =>
      match (Zpower_nat radix q' * v ?= radix * N)%Z with
      | Datatypes.Lt => q'
      | Datatypes.Eq => q'
      | _ => FNIAux v N q'
      end
  end.

Definition FNI (q N : nat) := pred (FNIAux q N (S (S N))).

Theorem FNIAuxLess :
 forall v N q : nat,
 0 < v -> v <= N -> (Zpower_nat radix (FNIAux v N q) * v <= radix * N)%Z.
intros v N q; elim q.
intros H1 H2; apply Zle_trans with (Z_of_nat v); simpl in |- *.
apply Zeq_le; case v; auto with arith zarith.
apply Zle_trans with (Z_of_nat N); auto with arith zarith.
pattern (Z_of_nat N) at 1 in |- *; replace (Z_of_nat N) with (1 * N)%Z;
 auto with arith zarith.
intros q1 H H1 H2.
simpl in |- *;
 generalize (Zcompare_correct (Zpower_nat radix q1 * v) (radix * N));
 case (Zpower_nat radix q1 * v ?= radix * N)%Z; auto with arith zarith.
Qed.

Theorem FNILess :
 forall q N : nat, 0 < q -> q <= N -> (Zpower_nat radix (FNI q N) * q <= N)%Z.
intros q N H1 H2; unfold FNI in |- *.
apply Zmult_le_reg_r with radix; auto with zarith.
generalize (refl_equal (FNIAux q N (S (S N))));
 pattern (FNIAux q N (S (S N))) at -1 in |- *; case (FNIAux q N (S (S N))).
intros H3; replace (Zpower_nat radix (pred 0) * q)%Z with (Z_of_nat q);
 auto with arith zarith.
intros n H3; simpl in |- *.
rewrite (Zmult_comm (Z_of_nat N) radix).
replace (Zpower_nat radix n * q * radix)%Z with
 (Zpower_nat radix (FNIAux q N (S (S N))) * q)%Z;
 [ apply FNIAuxLess; auto | idtac ].
rewrite H3; rewrite Zpower_nat_S; ring.
Qed.

Theorem FNIAuxMore :
 forall v N q : nat,
 FNIAux v N q < pred q -> (N < Zpower_nat radix (FNIAux v N q) * v)%Z.
intros v N q; elim q; simpl in |- *.
intros H; inversion H.
intros q1 H'.
generalize (Zcompare_correct (Zpower_nat radix q1 * v) (radix * N));
 case (Zpower_nat radix q1 * v ?= radix * N)%Z; auto with arith zarith.
intros H1 H2.
case (le_lt_or_eq (FNIAux v N q1) (pred q1)); auto with zarith arith.
intros H3; rewrite H3.
apply Zgt_lt; apply Zmult_gt_reg_r with radix; auto with zarith; apply Zlt_gt.
apply Zlt_le_trans with (Zpower_nat radix q1 * v)%Z; auto with zarith.
rewrite Zmult_comm; auto.
replace (Zpower_nat radix (pred q1) * v * radix)%Z with
 (radix * Zpower_nat radix (pred q1) * v)%Z;
 [ rewrite <- Zpower_nat_S | ring ].
apply Zmult_le_compat_r; auto with zarith.
Qed.

Theorem Zlt_Zpower_nat : forall n : nat, (n < Zpower_nat radix n)%Z.
intros n; induction n as [| n Hrecn].
simpl in |- *; auto with zarith.
rewrite Zpower_nat_S.
apply Zlt_le_trans with (1 + Zpower_nat radix n)%Z.
replace (Z_of_nat (S n)) with (1 + n)%Z; auto with arith zarith.
replace 1%Z with (Z_of_nat 1); auto with arith zarith.
rewrite <- inj_plus; auto with arith zarith.
apply Zle_trans with (Zpower_nat radix n + Zpower_nat radix n)%Z;
 auto with zarith.
apply Zle_trans with (2 * Zpower_nat radix n)%Z; auto with zarith.
Qed.

Theorem FNIMore :
 forall N q : nat,
 0 < q -> q <= N -> (N < radix * (Zpower_nat radix (FNI q N) * q))%Z.
intros N q; case q.
intros H; inversion H.
intros q' H H'; unfold FNI in |- *.
apply
 Zlt_le_trans with (Zpower_nat radix (FNIAux (S q') N (S (S N))) * S q')%Z.
apply FNIAuxMore; auto with arith zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
 pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
 case (FNIAux (S q') N (S (S N))).
simpl in |- *; auto with arith.
intros n0 H2; replace (pred (S (S N))) with (S N); auto with arith.
rewrite <- H2.
apply Zpower_nat_anti_monotone_lt with radix; auto with arith zarith.
apply Zgt_lt; apply Zmult_gt_reg_r with (Z_of_nat (S q'));
 auto with zarith arith; apply Zlt_gt.
apply Zlt_le_trans with (Z_of_nat 1); auto with zarith arith.
apply Zle_lt_trans with (radix * N)%Z.
apply FNIAuxLess; auto with zarith arith.
apply Zle_lt_trans with (radix * N * S q')%Z; auto with zarith arith.
pattern (radix * N)%Z at 1 in |- *;
 replace (radix * N)%Z with (radix * N * 1%nat)%Z;
 auto with arith zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Zmult_gt_0_lt_compat_r; auto with zarith arith.
apply Zlt_gt; auto with arith zarith.
rewrite Zpower_nat_S; apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply Zlt_Zpower_nat.
rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
 pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
 case (FNIAux (S q') N (S (S N))).
intros H1; simpl in |- *; auto with zarith arith.
intros H1; rewrite <- Zpower_nat_S; auto with zarith arith.
Qed.

Definition FnormalizeI (b : FboundI) (p : float) :=
  match (0 ?= Fnum p)%Z with
  | Datatypes.Eq => Float 0 (- dExpI b)
  | Datatypes.Lt =>
      Fshift radix
        (min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
           (Zabs_nat (Fexp p + dExpI b))) p
  | Datatypes.Gt =>
      Fshift radix
        (min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
           (Zabs_nat (Fexp p + dExpI b))) p
  end.

Theorem FnormalizeICorrect :
 forall (b : FboundI) (p : float), FnormalizeI b p = p :>R.
intros b p; unfold FnormalizeI in |- *.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
rewrite <- H; simpl; ring.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
Qed.

Theorem FnormalizeIBounded :
 forall (b : FboundI) (p : float),
 FboundedI b p -> FboundedI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- *.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
replace (Float 0 (- dExpI b)) with (Fzero (- dExpI b));
 [ apply FboundedIFzero | unfold Fzero in |- *; auto ].
unfold Fshift in |- *.
repeat split; simpl in |- *.
apply Zle_trans with 0%Z; auto with zarith arith.
apply
 Zle_trans
  with (Fnum p * Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b)))%Z;
 auto with zarith arith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (Zabs (Fnum p));
 [ rewrite Zabs_absolu; rewrite Zmult_comm
 | apply Zabs_eq; auto with zarith ].
apply FNILess; auto with arith zarith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
 auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
 auto with zarith; elim H; intuition.
apply
 Zplus_le_reg_l
  with
    (dExpI b +
     min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
 Zle_trans
  with
    (Z_of_nat
       (min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
          (Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
 auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
 [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
unfold Fshift in |- *.
repeat split; simpl in |- *.
2: apply Zle_trans with 0%Z; auto with zarith arith.
2: cut (forall x y : Z, (x <= 0)%Z -> (0 <= y)%Z -> (x * y <= 0)%Z);
    [ intros F; apply F | intros x y H3 H2 ]; auto with zarith.
2: rewrite <- (Zopp_involutive (x * y));
    rewrite <- (Zopp_involutive 0).
2: apply Zle_Zopp; simpl in |- *; rewrite <- Zopp_mult_distr_l_reverse;
    auto with zarith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (- Zabs_nat (Fnum p))%Z;
 auto with zarith.
rewrite Zopp_mult_distr_l_reverse; apply Zle_Zopp.
apply
 Zle_trans
  with
    (Zabs_nat (Fnum p) *
     Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b)))%Z.
apply Zle_Zmult_comp_l; auto with zarith arith.
rewrite Zmult_comm; apply FNILess.
rewrite <- absolu_Zopp; auto with zarith arith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
 auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe.
rewrite <- (Zopp_involutive (Z_of_nat (vNumInf b))).
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zle_Zopp; elim H; intuition.
rewrite <- absolu_Zopp; rewrite <- Zabs_absolu; rewrite Zabs_eq;
 auto with zarith.
apply
 Zplus_le_reg_l
  with
    (dExpI b +
     min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
 Zle_trans
  with
    (Z_of_nat
       (min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
          (Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
 auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
 [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
Qed.

Theorem FcanonicIBoundedI :
 forall (b : FboundI) (p : float), FcanonicI b p -> FboundedI b p.
intros b p H.
case H; intros H1; elim H1; auto.
Qed.

Theorem FnormalizeIFcanonicI :
 forall (b : FboundI) (p : float),
 FboundedI b p -> FcanonicI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- *.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
unfold FcanonicI in |- *; right.
repeat split; simpl in |- *; auto with zarith.
replace (radix * 0)%R with (IZR 0); auto with zarith real.
replace (radix * 0)%R with (INR 0); auto with zarith real arith.
case
 (min_or (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)));
 intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
 (Fshift radix
    (min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))
    p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; auto.
left; unfold Fshift in |- *; simpl in |- *.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zabs_eq (Fnum p));
 auto with zarith; rewrite Zabs_absolu.
rewrite <- Rmult_IZR; rewrite INR_IZR_INZ; apply Rlt_IZR.
rewrite
 (Zmult_comm (Zabs_nat (Fnum p))
    (Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b))))
 .
apply FNIMore.
apply lt_Zlt_inv; simpl in |- *; rewrite <- Zabs_absolu; rewrite Zabs_eq;
 auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith;
 elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
 [ intros H4 | auto with zarith ].
case
 (Rle_or_lt
    (radix * (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z)
    (vNumSup b)); intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- *.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
replace 0%R with (IZR 0); auto with real zarith.
rewrite Rmult_IZR; auto with real arith zarith.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
cut (0 < - Fnum p)%Z; [ intros Y | auto with zarith ].
case
 (min_or (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)));
 intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
 (Fshift radix
    (min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))
    p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H2; auto with zarith.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
 auto with zarith.
intros H4; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H4; absurd (0 < Fnum p)%Z; auto with zarith.
right; unfold Fshift in |- *; simpl in |- *.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zopp_involutive (Fnum p));
 rewrite <- (Zabs_eq (- Fnum p)); auto with zarith.
rewrite Zopp_mult_distr_l_reverse; rewrite <- Rmult_IZR;
 rewrite Zmult_comm; rewrite Zopp_mult_distr_l_reverse.
apply Rlt_IZR; apply Zlt_Zopp.
rewrite Zabs_absolu; rewrite absolu_Zopp.
rewrite Zmult_comm;
 rewrite
  (Zmult_comm (Zabs_nat (Fnum p))
     (Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b))))
  .
apply FNIMore; auto with zarith.
rewrite <- absolu_Zopp; apply lt_Zlt_inv; simpl in |- *;
 rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq;
 auto with zarith; elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
 [ intros H4 | auto with zarith ].
case
 (Rle_or_lt (- vNumInf b)%Z
    (radix * (Fnum p * Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z));
 intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
 auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- *.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
apply Ropp_le_cancel.
rewrite Rmult_comm; rewrite <- Ropp_mult_distr_l_reverse; rewrite Rmult_comm.
replace (-0)%R with 0%R; auto with real.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
rewrite <- Ropp_Ropp_IZR; rewrite Zmult_comm.
rewrite Zopp_mult_distr_r; rewrite Zmult_comm; auto with zarith real.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
 auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
Qed.

End FboundedI_Def.