(****************************************************************************
                                                                             
          IEEE754  :  Fnorm                                                     
                                                                             
          Laurent Thery  &  Sylvie Boldo                                                    
                                                                             
  ******************************************************************************)
Require Export Fbound.
 
Section Fnormalized_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.
Coercion FtoRradix : float >-> R.
Variable b : Fbound.
 
Definition Fnormal (p : float) :=
  Fbounded b p /\ (Zpos (vNum b) <= Zabs (radix * Fnum p))%Z.
 
Theorem FnormalBounded : forall p : float, Fnormal p -> Fbounded b p.
(* Goal: forall (p : float) (_ : Fsubnormal p), Z.lt (Z.abs (Z.mul radix (Fnum p))) (Zpos (vNum b)) *)
intros p H; case H; auto.
Qed.
 
Theorem FnormalBound :
 forall p : float,
 Fnormal p -> (Zpos (vNum b) <= Zabs (radix * Fnum p))%Z.
(* Goal: forall (p : float) (_ : Fsubnormal p), Z.lt (Z.abs (Z.mul radix (Fnum p))) (Zpos (vNum b)) *)
intros p H; case H; auto.
Qed.
Hint Resolve FnormalBounded FnormalBound: float.
 
Theorem FnormalNotZero : forall p : float, Fnormal p -> ~ is_Fzero p.
(* Goal: forall (p : float) (_ : Fnormal p), not (is_Fzero p) *)
unfold is_Fzero in |- *; intros p H; red in |- *; intros H1.
(* Goal: False *)
case H; rewrite H1.
(* Goal: forall (_ : Fbounded b p) (_ : Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix Z0))), False *)
replace (Zabs (radix * 0)) with 0%Z; auto with zarith.
(* Goal: @eq Z Z0 (Z.abs (Z.mul radix Z0)) *)
rewrite Zmult_comm; simpl in |- *; auto.
Qed.
 
Theorem FnormalFop : forall p : float, Fnormal p -> Fnormal (Fopp p).
(* Goal: forall (p : float) (_ : Fnormal p), Fnormal (Fopp p) *)
intros p H; split; auto with float.
replace (Zabs (radix * Fnum (Fopp p))) with (Zabs (radix * Fnum p));
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
 auto with float.
(* Goal: @eq Z (Z.abs (Z.mul radix (Fnum p))) (Z.abs (Z.mul radix (Fnum (Fopp p)))) *)
case p; simpl in |- *; auto with zarith.
intros Fnum1 Fexp1; rewrite <- Zopp_mult_distr_r; apply sym_equal;
 apply Zabs_Zopp.
Qed.
 
Theorem FnormalFabs : forall p : float, Fnormal p -> Fnormal (Fabs p).
(* Goal: forall (p : float) (_ : Fsubnormal p), Fsubnormal (Fabs p) *)
intros p; case p; intros a e H; split; auto with float.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Fnum (Fabs (Float a e))))) *)
simpl in |- *; case H; intros H1 H2; simpl in |- *; auto.
(* Goal: Z.le (Zpos (vNum b)) (Z.mul (Z.abs (Fnum p)) radix) *)
rewrite <- (Zabs_eq radix); auto with zarith.
(* Goal: Z.lt (Z.abs (Z.mul (Z.abs radix) (Z.abs a))) (Zpos (vNum b)) *)
rewrite <- Zabs_Zmult.
(* Goal: Z.lt (Z.abs (Z.abs (Z.mul radix a))) (Zpos (vNum b)) *)
rewrite (fun x => Zabs_eq (Zabs x)); auto with float zarith.
Qed.
 
Definition pPred x := Zpred (Zpos x).
 
Theorem maxMax1 :
 forall (p : float) (z : Z),
 Fbounded b p -> (Fexp p <= z)%Z -> (Fabs p <= Float (pPred (vNum b)) z)%R.
(* Goal: forall (p : float) (z : Z) (_ : Fbounded b p) (_ : Z.le (Fexp p) z), Rle (FtoRradix (Fabs p)) (FtoRradix (Float (pPred (vNum b)) z)) *)
intros p z H H0; unfold FtoRradix in |- *.
rewrite <-
 (FshiftCorrect _ radixMoreThanOne (Zabs_nat (z - Fexp p))
    (Float (pPred (vNum b)) z)).
(* Goal: Rle (FtoR radix (Fabs p)) (FtoR radix (Fshift radix (Z.abs_nat (Z.sub z (Fexp p))) (Float (pPred (vNum b)) z))) *)
unfold FtoR, Fabs in |- *; simpl in |- *; auto with zarith.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Z.mul (pPred (vNum b)) (Zpower_nat radix (Z.abs_nat (Z.sub z (Fexp p)))))) (powerRZ (IZR radix) (Z.sub z (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p))))))) *)
rewrite Rmult_IZR; rewrite Zpower_nat_Z_powerRZ; auto with zarith.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p)))))) (powerRZ (IZR radix) (Z.sub z (Z.of_nat (Z.abs_nat (Z.sub z (Fexp p))))))) *)
repeat rewrite inj_abs; auto with zarith.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.sub z (Fexp p)))) (powerRZ (IZR radix) (Z.sub z (Z.sub z (Fexp p))))) *)
replace (z - (z - Fexp p))%Z with (Fexp p); [ idtac | ring ].
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.sub z (Fexp p)))) (powerRZ (IZR radix) (Fexp p))) *)
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.add (Z.sub z (Fexp p)) (Fexp p)))) *)
replace (z - Fexp p + Fexp p)%Z with z; [ idtac | ring ].
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) z)) *)
apply Rle_trans with (pPred (vNum b) * powerRZ radix (Fexp p))%R.
apply Rle_monotone_exp; auto with zarith; repeat rewrite Rmult_IZR;
 apply Rle_IZR; unfold pPred in |- *; apply Zle_Zpred;
 auto with float real zarith.
(* Goal: Rle (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) z)) *)
apply Rmult_le_compat_l; auto with real zarith.
replace 0%R with (IZR 0); auto with real; apply Rle_IZR; unfold pPred in |- *;
 apply Zle_Zpred; auto with float zarith.
(* Goal: Rle (powerRZ (IZR radix) (Fexp p)) (powerRZ (IZR radix) z) *)
apply Rle_powerRZ; auto with float real zarith.
Qed.
 
Theorem FnormalBoundAbs :
 forall p : float,
 Fnormal p -> (Float (pPred (vNum b)) (Zpred (Fexp p)) < Fabs p)%R.
(* Goal: forall (p : float) (_ : Fnormal p), Rle (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp p))))) (FtoRradix (Fabs p)) *)
intros p H'; unfold FtoRradix, FtoR in |- *; simpl in |- *.
pattern (Fexp p) at 2 in |- *; replace (Fexp p) with (Zsucc (Zpred (Fexp p)));
 [ rewrite powerRZ_Zs; auto with real zarith
 | unfold Zsucc, Zpred in |- *; ring ].
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (IZR (Z.abs (Fnum p))) (Rmult (IZR radix) (powerRZ (IZR radix) (Z.pred (Fexp p))))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: Rlt (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp p)))) *)
apply Rmult_lt_compat_r; auto with real arith.
(* Goal: Rlt (IZR (pPred (vNum b))) (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) *)
rewrite <- Rmult_IZR; apply Rlt_IZR.
unfold pPred in |- *; cut (Zpos (vNum b) <= Zabs (Fnum p) * radix)%Z;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
rewrite <- (Zabs_eq radix); auto with float zarith; rewrite <- Zabs_Zmult;
 rewrite Zmult_comm; auto with float real zarith.
Qed.
 
Definition Fsubnormal (p : float) :=
  Fbounded b p /\
  Fexp p = (- dExp b)%Z /\ (Zabs (radix * Fnum p) < Zpos (vNum b))%Z.
 
Theorem FsubnormalFbounded : forall p : float, Fsubnormal p -> Fbounded b p.
(* Goal: forall (p : float) (_ : Fsubnormal p), Z.lt (Z.abs (Z.mul radix (Fnum p))) (Zpos (vNum b)) *)
intros p H; case H; auto.
Qed.
 
Theorem FsubnormalFexp :
 forall p : float, Fsubnormal p -> Fexp p = (- dExp b)%Z.
(* Goal: forall (p : float) (_ : Fsubnormal p), Z.lt (Z.abs (Z.mul radix (Fnum p))) (Zpos (vNum b)) *)
intros p H; case H; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
Qed.
 
Theorem FsubnormalBound :
 forall p : float,
 Fsubnormal p -> (Zabs (radix * Fnum p) < Zpos (vNum b))%Z.
(* Goal: forall (p : float) (_ : Fsubnormal p), Z.lt (Z.abs (Z.mul radix (Fnum p))) (Zpos (vNum b)) *)
intros p H; case H; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
Qed.
Hint Resolve FsubnormalFbounded FsubnormalBound FsubnormalFexp: float.
 
Theorem FsubnormFopp : forall p : float, Fsubnormal p -> Fsubnormal (Fopp p).
(* Goal: forall (p : float) (_ : Fsubnormal p), Fsubnormal (Fopp p) *)
intros p H'; repeat split; simpl in |- *; auto with zarith float.
(* Goal: Z.lt (Z.abs (Z.opp (Fnum p))) (Zpos (vNum b)) *)
(* Goal: Z.lt (Z.abs (Z.mul radix (Z.opp (Fnum p)))) (Zpos (vNum b)) *)
rewrite Zabs_Zopp; auto with float.
(* Goal: Z.lt (Z.abs (Z.opp (Fnum p))) (Zpos (vNum b)) *)
(* Goal: Z.lt (Z.abs (Z.mul radix (Z.opp (Fnum p)))) (Zpos (vNum b)) *)
rewrite <- Zopp_mult_distr_r; rewrite Zabs_Zopp; auto with float.
Qed.
 
Theorem FsubnormFabs : forall p : float, Fsubnormal p -> Fsubnormal (Fabs p).
(* Goal: forall (p : float) (_ : Fsubnormal p), Fsubnormal (Fabs p) *)
intros p; case p; intros a e H; split; auto with float.
(* Goal: and (@eq Z (Fexp (Fabs (Float a e))) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum (Fabs (Float a e))))) (Zpos (vNum b))) *)
simpl in |- *; split; auto with float.
(* Goal: Z.lt (Z.abs (Z.mul radix a)) (Zpos (vNum b)) *)
case H; intros H1 (H2, H3); auto.
(* Goal: Z.le (Zpos (vNum b)) (Z.mul (Z.abs (Fnum p)) radix) *)
rewrite <- (Zabs_eq radix); auto with zarith.
(* Goal: Z.lt (Z.abs (Z.mul (Z.abs radix) (Z.abs a))) (Zpos (vNum b)) *)
rewrite <- Zabs_Zmult.
(* Goal: Z.lt (Z.abs (Z.abs (Z.mul radix a))) (Zpos (vNum b)) *)
rewrite (fun x => Zabs_eq (Zabs x)); auto with float zarith.
(* Goal: Z.lt (Z.abs (Z.mul radix a)) (Zpos (vNum b)) *)
case H; intros H1 (H2, H3); auto.
Qed.
 
Theorem FsubnormalUnique :
 forall p q : float, Fsubnormal p -> Fsubnormal q -> p = q :>R -> p = q.
(* Goal: forall (p q : float) (_ : Fnormal p) (_ : Fnormal q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float p q *)
intros p q H' H'0 H'1.
(* Goal: @eq float p q *)
apply FtoREqInv2 with (radix := radix); auto.
(* Goal: @eq Z (Fexp p) (Fexp q) *)
generalize H' H'0; unfold Fsubnormal in |- *; auto with zarith.
Qed.
 
Theorem FsubnormalLt :
 forall p q : float,
 Fsubnormal p -> Fsubnormal q -> (p < q)%R -> (Fnum p < Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fnormal p) (_ : Fnormal q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float p q *)
intros p q H' H'0 H'1.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith.
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply trans_equal with (- dExp b)%Z.
(* Goal: @eq Z (Fexp p) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: @eq Z (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case H'; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
(* Goal: @eq Z (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
apply sym_equal; case H'0; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
Qed.
 
Theorem LtFsubnormal :
 forall p q : float,
 Fsubnormal p -> Fsubnormal q -> (Fnum p < Fnum q)%Z -> (p < q)%R.
(* Goal: forall (p q : float) (_ : Fnormal p) (_ : Fnormal q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float p q *)
intros p q H' H'0 H'1.
case (Rtotal_order p q); auto; intros Test; case Test; clear Test;
 intros Test; Contradict H'1.
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
unfold FtoRradix in Test; rewrite sameExpEq with (2 := Test); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
auto with zarith.
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply trans_equal with (- dExp b)%Z.
(* Goal: @eq Z (Fexp p) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: @eq Z (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case H'; auto.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
(* Goal: @eq Z (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply sym_equal; case H'0.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H1 H2; case H2; auto.
(* Goal: not (Z.lt (Fnum p) nNormMin) *)
apply Zle_not_lt.
(* Goal: Z.le (Fnum q) (Fnum p) *)
apply Zlt_le_weak.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
apply FsubnormalLt; auto.
Qed.
 
Definition Fcanonic (a : float) := Fnormal a \/ Fsubnormal a.
 
Theorem FcanonicBound : forall p : float, Fcanonic p -> Fbounded b p.
(* Goal: forall (p : float) (_ : Fcanonic p), Fbounded b p *)
intros p H; case H; auto with float.
Qed.
Hint Resolve FcanonicBound: float.
 
Theorem pUCanonic_absolu :
 forall p : float, Fcanonic p -> (Zabs (Fnum p) < Zpos (vNum b))%Z.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
auto with float.
Qed.
 
Theorem FcanonicFopp : forall p : float, Fcanonic p -> Fcanonic (Fopp p).
(* Goal: forall (p : float) (_ : Fcanonic p), Fcanonic (Fopp p) *)
intros p H'; case H'; intros H'1.
(* Goal: Fcanonic (Fopp p) *)
(* Goal: Fcanonic (Fopp p) *)
left; apply FnormalFop; auto.
(* Goal: Fcanonic (Fopp p) *)
right; apply FsubnormFopp; auto.
Qed.
 
Theorem FcanonicFabs : forall p : float, Fcanonic p -> Fcanonic (Fabs p).
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros p H'; case H'; clear H'; auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros H; left; auto with float.
(* Goal: Fnormal (Fabs p) *)
(* Goal: forall _ : Fsubnormal p, Fcanonic (Fabs p) *)
apply FnormalFabs; auto.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros H; right; auto with float.
(* Goal: Fsubnormal (Fabs p) *)
apply FsubnormFabs; auto.
Qed.
 
Theorem NormalNotSubNormal : forall p : float, ~ (Fnormal p /\ Fsubnormal p).
(* Goal: forall p : float, not (and (Fnormal p) (Fsubnormal p)) *)
intros p; red in |- *; intros H; elim H; intros H0 H1; clear H.
absurd (Zabs (radix * Fnum p) < Zpos (vNum b))%Z;
 auto with float zarith.
Qed.
 
Theorem MaxFloat :
 forall x : float,
 Fbounded b x -> (Rabs x < Float (Zpos (vNum b)) (Fexp x))%R.
(* Goal: forall (x : float) (_ : Fbounded b x), Rlt (Rabs (FtoRradix x)) (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) *)
intros.
(* Goal: Rlt (Rabs (FtoRradix x)) (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) *)
replace (Rabs x) with (FtoR radix (Fabs x)).
(* Goal: @eq R (FtoR radix (Fabs x)) (Rabs (FtoRradix x)) *)
unfold FtoRradix in |- *.
(* Goal: Rlt (FtoR radix (Fabs x)) (FtoR radix (Float (Zpos (vNum b)) (Fexp x))) *)
(* Goal: @eq R (FtoR radix (Fabs x)) (Rabs (FtoRradix x)) *)
apply maxMax with (b := b); auto with *.
(* Goal: @eq R (FtoR radix (Fabs x)) (Rabs (FtoRradix x)) *)
unfold FtoRradix in |- *.
(* Goal: @eq R (FtoR radix (Fabs x)) (Rabs (FtoR radix x)) *)
apply Fabs_correct; auto with *.
Qed.
(* What depends of the precision *)
Variable precision : nat.
Hypothesis precisionNotZero : precision <> 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Theorem FboundNext :
 forall p : float,
 Fbounded b p ->
 exists q : float, Fbounded b q /\ q = Float (Zsucc (Fnum p)) (Fexp p) :>R.
(* Goal: forall (p : float) (_ : Fcanonic p), @eq float (Fnormalize p) p *)
intros p H'.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
case (Zle_lt_or_eq (Zsucc (Fnum p)) (Zpos (vNum b))); auto with float.
(* Goal: Z.le (Z.succ (Fnum p)) (Zpos (vNum b)) *)
(* Goal: forall _ : Z.lt (Z.succ (Fnum p)) (Zpos (vNum b)), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix q) (FtoRradix (Float (Z.succ (Fnum p)) (Fexp p))))) *)
(* Goal: forall _ : @eq Z (Z.succ (Fnum p)) (Zpos (vNum b)), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix q) (FtoRradix (Float (Z.succ (Fnum p)) (Fexp p))))) *)
case (Zle_or_lt 0 (Fnum p)); intros H1.
(* Goal: Z.le nNormMin (Fnum p) *)
rewrite <- (Zabs_eq (Fnum p)); auto with float zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zle_trans with 0%Z; auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros H'0; exists (Float (Zsucc (Fnum p)) (Fexp p)); split; auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
repeat split; simpl in |- *; auto with float.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case (Zle_or_lt 0 (Fnum p)); intros H1; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.succ (Fnum p))) (Zpos (vNum b)) *)
(* Goal: forall _ : @eq Z (Z.succ (Fnum p)) (Zpos (vNum b)), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix q) (FtoRradix (Float (Z.succ (Fnum p)) (Fexp p))))) *)
apply Zlt_trans with (Zabs (Fnum p)); auto with float zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat rewrite Zabs_eq_opp; auto with zarith.
intros H'0;
 exists (Float (Zpower_nat radix (pred precision)) (Zsucc (Fexp p))); 
 split; auto.
(* Goal: Fbounded b (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p))) *)
(* Goal: @eq R (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p)))) (FtoRradix (Float (Z.succ (Fnum p)) (Fexp p))) *)
repeat split; simpl in |- *; auto with zarith arith float.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite H'0; rewrite pGivesBound.
(* Goal: @eq R (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p)))) (FtoRradix (Float (Zpower_nat radix precision) (Fexp p))) *)
pattern precision at 2 in |- *; replace precision with (1 + pred precision).
(* Goal: @eq R (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p)))) (FtoRradix (Float (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision))) (Fexp p))) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
rewrite Zpower_nat_is_exp.
(* Goal: @eq R (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p)))) (FtoRradix (Float (Z.mul (Zpower_nat radix (S O)) (Zpower_nat radix (Init.Nat.pred precision))) (Fexp p))) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
rewrite Zpower_nat_1.
(* Goal: @eq R (FtoRradix (Float (Zpower_nat radix (Init.Nat.pred precision)) (Z.succ (Fexp p)))) (FtoRradix (Float (Z.mul radix (Zpower_nat radix (Init.Nat.pred precision))) (Fexp p))) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (powerRZ (IZR radix) (Z.succ (Fexp p)))) (Rmult (IZR (Z.mul radix (Zpower_nat radix (Init.Nat.pred precision)))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
rewrite powerRZ_Zs; auto with real zarith.
(* Goal: @eq R (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (Rmult (IZR radix) (powerRZ (IZR radix) (Fexp p)))) (Rmult (IZR (Z.mul radix (Zpower_nat radix (Init.Nat.pred precision)))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
rewrite Rmult_IZR; ring.
(* Goal: @eq nat precision (Init.Nat.add (Init.Nat.pred precision) (S O)) *)
generalize precisionNotZero; case precision; simpl in |- *; auto with arith.
(* Goal: forall _ : not (@eq nat O O), @eq nat (S O) O *)
intros H'1; case H'1; auto.
Qed.
 
Theorem digitPredVNumiSPrecision :
 digit radix (Zpred (Zpos (vNum b))) = precision.
(* Goal: @eq nat (digit radix (Zpos (vNum b))) (S precision) *)
apply digitInv; auto.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
Qed.
 
Theorem digitVNumiSPrecision :
 digit radix (Zpos (vNum b)) = S precision.
(* Goal: @eq nat (digit radix (Zpos (vNum b))) (S precision) *)
apply digitInv; auto.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite pGivesBound; auto with zarith.
Qed.
 
Theorem vNumPrecision :
 forall n : Z,
 digit radix n <= precision -> (Zabs n < Zpos (vNum b))%Z.
(* Goal: forall (n : Z) (_ : le (digit radix n) precision), Z.lt (Z.abs n) (Zpos (vNum b)) *)
intros n H'.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite <- (Zabs_eq (Zpos (vNum b))); auto with zarith.
(* Goal: Z.lt (Z.abs n) (Z.abs (Zpos (vNum b))) *)
apply digit_anti_monotone_lt with (n := radix); auto.
(* Goal: lt (digit radix n) (digit radix (Zpos (vNum b))) *)
rewrite digitVNumiSPrecision; auto with arith.
Qed.
 
Theorem pGivesDigit :
 forall p : float, Fbounded b p -> Fdigit radix p <= precision.
(* Goal: forall (p : float) (_ : Fsubnormal p), lt (Fdigit radix p) precision *)
intros p H; unfold Fdigit in |- *.
(* Goal: le (S (digit radix (Fnum p))) precision *)
rewrite <- digitPredVNumiSPrecision.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply digit_monotone; auto with zarith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum p) (Zpower_nat radix (S O)))) (Z.abs (Z.pred (Zpos (vNum b)))) *)
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite (fun x => Zabs_eq (Zpred x)); auto with float zarith.
Qed.
 
Theorem digitGivesBoundedNum :
 forall p : float,
 Fdigit radix p <= precision -> (Zabs (Fnum p) < Zpos (vNum b))%Z.
(* Goal: forall (p : float) (_ : le (Fdigit radix p) precision), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros p H; apply vNumPrecision; auto.
Qed.
 
Theorem FboundedOne :
 forall z : Z, (- dExp b <= z)%Z -> Fbounded b (Float 1%nat z).
(* Goal: forall (z : Z) (_ : Z.le (Z.opp (Z.of_N (dExp b))) z), Fbounded b (Float (Z.of_nat (S O)) z) *)
intros z H'; repeat (split; simpl in |- *; auto with zarith).
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
rewrite pGivesBound; auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zlt_le_trans with (Zpower_nat radix 1); auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zpower_nat_1; auto with zarith.
Qed.
 
Theorem FboundedMboundPos :
 forall z m : Z,
 (0 <= m)%Z ->
 (m <= Zpower_nat radix precision)%Z ->
 (- dExp b <= z)%Z ->
 exists c : float, Fbounded b c /\ c = (m * powerRZ radix z)%R :>R.
(* Goal: forall (z m : Z) (_ : Z.le Z0 m) (_ : Z.le m (Zpower_nat radix precision)) (_ : Z.le (Z.opp (Z.of_N (dExp b))) z), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
intros z m H' H'0 H'1; case (Zle_lt_or_eq _ _ H'0); intros H'2.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
exists (Float m z); split; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat split; simpl in |- *; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
rewrite Zabs_eq; auto; rewrite pGivesBound; auto.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
case (FboundNext (Float (Zpred (Zpos (vNum b))) z)); auto with float.
(* Goal: forall (x : float) (_ : and (Fbounded b x) (@eq R (FtoRradix x) (FtoRradix (Float (Z.succ (Fnum (Float (Z.pred (Zpos (vNum b))) z))) (Fexp (Float (Z.pred (Zpos (vNum b))) z)))))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
intros f' (H1, H2); exists f'; split; auto.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite H2; rewrite pGivesBound.
(* Goal: @eq R (FtoRradix (Float (Z.succ (Fnum (Float (Z.pred (Zpower_nat radix precision)) z))) (Fexp (Float (Z.pred (Zpower_nat radix precision)) z)))) (Rmult (IZR m) (powerRZ (IZR radix) z)) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Z.succ (Z.pred (Zpower_nat radix precision)))) (powerRZ (IZR radix) z)) (Rmult (IZR m) (powerRZ (IZR radix) z)) *)
rewrite <- Zsucc_pred; rewrite <- H'2; auto; ring.
Qed.
 
Theorem FboundedMbound :
 forall z m : Z,
 (Zabs m <= Zpower_nat radix precision)%Z ->
 (- dExp b <= z)%Z ->
 exists c : float, Fbounded b c /\ c = (m * powerRZ radix z)%R :>R.
(* Goal: forall (z m : Z) (_ : Z.le (Z.abs m) (Zpower_nat radix precision)) (_ : Z.le (Z.opp (Z.of_N (dExp b))) z), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
intros z m H H0.
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
case (Zle_or_lt 0 m); intros H1.
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
case (FboundedMboundPos z (Zabs m)); auto; try rewrite Zabs_eq; auto.
(* Goal: forall (x : float) (_ : and (Fbounded b x) (@eq R (FtoRradix x) (Rmult (IZR m) (powerRZ (IZR radix) z)))), @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
(* Goal: @ex float (fun c : float => and (Fbounded b c) (@eq R (FtoRradix c) (Rmult (IZR m) (powerRZ (IZR radix) z)))) *)
intros f (H2, H3); exists f; split; auto.
case (FboundedMboundPos z (Zabs m)); auto; try rewrite Zabs_eq_opp;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros f (H2, H3); exists (Fopp f); split; auto with float.
rewrite (Fopp_correct radix); auto with arith; fold FtoRradix in |- *;
 rewrite H3.
(* Goal: @eq R (Ropp (Rmult (IZR (Z.opp m)) (powerRZ (IZR radix) z))) (Rmult (IZR m) (powerRZ (IZR radix) z)) *)
rewrite Ropp_Ropp_IZR; ring.
Qed.
 
Theorem FnormalPrecision :
 forall p : float, Fnormal p -> Fdigit radix p = precision.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
intros p H; apply le_antisym; auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply pGivesDigit; auto with float.
apply le_S_n.
rewrite <- digitVNumiSPrecision.
(* Goal: forall _ : le (Fdigit radix p) precision, @eq nat precision (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.pred (Fdigit radix p)) (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
unfold Fdigit in |- *.
(* Goal: le (S (digit radix (Fnum p))) (digit radix (Z.pred (Zpos (vNum b)))) *)
replace (S (digit radix (Fnum p))) with (digit radix (Fnum p) + 1).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite <- digitAdd; auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply digit_monotone; auto with float.
rewrite (fun x => Zabs_eq (Zpos x)); auto with float zarith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum p) (Zpower_nat radix (S O)))) (Z.pred (Zpos (vNum b))) *)
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite Zmult_comm; rewrite Zpower_nat_1; auto with float zarith.
red in |- *; intros H1; case H.
intros H0 H2; Contradict H2; rewrite H1.
(* Goal: forall (_ : Fbounded b p) (_ : Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix Z0))), False *)
replace (Zabs (radix * 0)) with 0%Z; auto with zarith.
(* Goal: @eq Z Z0 (Z.abs (Z.mul radix Z0)) *)
rewrite Zmult_comm; simpl in |- *; auto.
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite plus_comm; simpl in |- *; auto.
Qed.
Hint Resolve FnormalPrecision: float.
 
Theorem FnormalUnique :
 forall p q : float, Fnormal p -> Fnormal q -> p = q :>R -> p = q.
(* Goal: forall (p q : float) (_ : Fnormal p) (_ : Fnormal q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float p q *)
intros p q H' H'0 H'1.
(* Goal: @eq float p q *)
apply (FdigitEq radix); auto.
(* Goal: not (is_Fzero p) *)
(* Goal: @eq nat (Fdigit radix p) (Fdigit radix q) *)
apply FnormalNotZero; auto.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply trans_equal with (y := precision); auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply sym_equal; auto with float.
Qed.
 
Theorem FnormalLtPos :
 forall p q : float,
 Fnormal p ->
 Fnormal q ->
 (0 <= p)%R ->
 (p < q)%R -> (Fexp p < Fexp q)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
case (Zle_or_lt (Fexp q) (Fexp p)); auto.
intros H'3; right.
case (Zle_lt_or_eq _ _ H'3); intros H'4.
2: split; auto.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
2: apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith.
absurd (Fnum (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p) < Fnum q)%Z; auto.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
2: apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith.
2: unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
2: unfold Fshift in |- *; simpl in |- *; auto with zarith.
2: replace (Z_of_nat (Zabs_nat (Fexp p - Fexp q))) with (Fexp p - Fexp q)%Z;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
    auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
2: cut (0 < Fexp p - Fexp q)%Z; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
2: case (Fexp p - Fexp q)%Z; simpl in |- *; auto with zarith.
2: intros p0; rewrite (inject_nat_convert (Zpos p0)); auto with arith.
2: intros p0 H'5; discriminate.
red in |- *; intros H'5.
absurd
 (Fdigit radix (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p) <=
  Fdigit radix q); auto with arith.
rewrite FshiftFdigit; auto with arith.
replace (Fdigit radix p) with precision.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
replace (Fdigit radix q) with precision; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
cut (0 < Fexp p - Fexp q)%Z; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case (Fexp p - Fexp q)%Z; simpl in |- *; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros p0 H'6; generalize (convert_not_O p0); auto with zarith.
intros p0 H'6; discriminate.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply sym_equal; auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply sym_equal; auto with float.
apply FnormalNotZero; auto with arith.
unfold Fdigit in |- *; apply digit_monotone; auto with arith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoRradix q) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply Rle_trans with (r2 := FtoRradix p); auto with real.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply LeR0Fnum with (radix := radix); auto with zarith.
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
Qed.
 
Theorem FnormalLtNeg :
 forall p q : float,
 Fnormal p ->
 Fnormal q ->
 (q <= 0)%R ->
 (p < q)%R -> (Fexp q < Fexp p)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
cut
 ((Fexp (Fopp q) < Fexp (Fopp p))%Z \/
  Fexp (Fopp q) = Fexp (Fopp p) /\ (Fnum (Fopp q) < Fnum (Fopp p))%Z).
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
simpl in |- *.
intros H'3; elim H'3; clear H'3; intros H'3;
 [ idtac | elim H'3; clear H'3; intros H'3 H'4 ]; auto; 
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 right; split; auto with zarith.
apply FnormalLtPos; try apply FnormalFop; auto; unfold FtoRradix in |- *;
 repeat rewrite Fopp_correct; replace 0%R with (-0)%R; 
 auto with real.
Qed.
 
Definition nNormMin := Zpower_nat radix (pred precision).
 
Theorem nNormPos : (0 < nNormMin)%Z.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
unfold nNormMin in |- *; auto with zarith.
Qed.
 
Theorem digitnNormMin : digit radix nNormMin = precision.
unfold nNormMin, Fdigit in |- *; simpl in |- *; apply digitInv;
 auto with zarith arith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
Qed.
 
Theorem nNrMMimLevNum : (nNormMin <= Zpos (vNum b))%Z.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: Z.lt nNormMin (Zpower_nat radix precision) *)
(* Goal: Z.le Z0 nNormMin *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
unfold nNormMin in |- *; simpl in |- *; auto with zarith arith.
Qed.
Hint Resolve nNrMMimLevNum: arith.
 
Definition firstNormalPos := Float nNormMin (- dExp b).
 
Theorem firstNormalPosNormal : Fnormal firstNormalPos.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat split; unfold firstNormalPos in |- *; simpl in |- *; auto with zarith.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt nNormMin (Zpower_nat radix precision) *)
(* Goal: Z.le Z0 nNormMin *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
unfold nNormMin in |- *; simpl in |- *; auto with zarith arith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zlt_le_weak; auto with zarith.
(* Goal: Z.lt Z0 nNormMin *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
apply nNormPos.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: Z.le (Zpower_nat radix precision) (Z.abs (Z.mul radix nNormMin)) *)
replace precision with (pred precision + 1).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zpower_nat_is_exp; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zpower_nat_1; auto with zarith.
rewrite (fun x => Zmult_comm x radix); unfold nNormMin in |- *;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
unfold nNormMin in |- *; auto with zarith.
Qed.
 
Theorem pNormal_absolu_min :
 forall p : float, Fnormal p -> (nNormMin <= Zabs (Fnum p))%Z.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros p H; apply Zmult_le_reg_r with (p := radix); auto with zarith.
(* Goal: Z.le (Z.mul nNormMin radix) (Z.mul (Z.abs (Fnum p)) radix) *)
unfold nNormMin in |- *.
(* Goal: Rle (IZR (Zpos (vNum b))) (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (IZR radix)) *)
pattern radix at 2 in |- *; rewrite <- (Zpower_nat_1 radix).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite <- Zpower_nat_is_exp; auto with zarith.
(* Goal: Rle (IZR (Zpos (vNum b))) (IZR (Zpower_nat radix (Init.Nat.add (Init.Nat.pred precision) (S O)))) *)
replace (pred precision + 1) with precision.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
rewrite <- pGivesBound; auto with float.
(* Goal: Z.le (Zpos (vNum b)) (Z.mul (Z.abs (Fnum p)) radix) *)
rewrite <- (Zabs_eq radix); auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
rewrite <- Zabs_Zmult; rewrite Zmult_comm; auto with float.
generalize precisionNotZero; case precision; simpl in |- *;
 try (intros tmp; Contradict tmp; auto; fail); intros; 
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
 rewrite plus_comm; simpl in |- *; auto.
Qed.
 
Theorem maxMaxBis :
 forall (p : float) (z : Z),
 Fbounded b p -> (Fexp p < z)%Z -> (Fabs p < Float nNormMin z)%R.
intros p z H' H'0;
 apply
  Rlt_le_trans with (FtoR radix (Float (Zpos (vNum b)) (Zpred z))).
unfold FtoRradix in |- *; apply maxMax; auto with zarith;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 unfold Zpred in |- *; auto with zarith.
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
unfold FtoRradix, FtoR, nNormMin in |- *; simpl in |- *.
pattern z at 2 in |- *; replace z with (Zsucc (Zpred z));
 [ rewrite powerRZ_Zs; auto with real zarith
 | unfold Zsucc, Zpred in |- *; ring ].
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.pred z))) (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (Rmult (IZR radix) (powerRZ (IZR radix) (Z.pred z)))) *)
rewrite <- Rmult_assoc.
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp p)))) *)
apply Rmult_le_compat_r; auto with real arith.
(* Goal: Rle (IZR (Zpos (vNum b))) (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (IZR radix)) *)
pattern radix at 2 in |- *; rewrite <- (Zpower_nat_1 radix).
(* Goal: Rle (IZR (Zpos (vNum b))) (Rmult (IZR (Zpower_nat radix (Init.Nat.pred precision))) (IZR (Zpower_nat radix (S O)))) *)
rewrite <- Rmult_IZR.
(* Goal: Rle (IZR (Zpos (vNum b))) (IZR (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) (Zpower_nat radix (S O)))) *)
rewrite <- Zpower_nat_is_exp.
(* Goal: Rle (IZR (Zpos (vNum b))) (IZR (Zpower_nat radix (Init.Nat.add (Init.Nat.pred precision) (S O)))) *)
replace (pred precision + 1) with precision.
(* Goal: Rle (IZR (Zpos (vNum b))) (IZR (Zpower_nat radix precision)) *)
(* Goal: @eq nat precision (Init.Nat.add (Init.Nat.pred precision) (S O)) *)
replace (INR (nat_of_P (vNum b))) with (IZR (Zpos (vNum b))).
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Zpower_nat radix precision)) *)
(* Goal: @eq nat precision (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.pred (Fdigit radix p)) (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
rewrite pGivesBound; auto with real.
(* Goal: @eq R (IZR (Zpos (vNum b))) (INR (Pos.to_nat (vNum b))) *)
(* Goal: @eq nat precision (Init.Nat.add (Init.Nat.pred precision) (S O)) *)
simpl; unfold IZR; rewrite <- INR_IPR; auto.
(* Goal: @eq nat precision (Init.Nat.add (Init.Nat.pred precision) (S O)) *)
generalize precisionNotZero; case precision; simpl in |- *; auto with arith.
(* Goal: forall _ : not (@eq nat O O), @eq nat O (S O) *)
(* Goal: forall (n : nat) (_ : not (@eq nat (S n) O)), @eq nat (S n) (Init.Nat.add n (S O)) *)
intros H'1; Contradict H'1; auto.
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
intros; rewrite plus_comm; simpl in |- *; auto.
Qed.
 
Theorem FnormalLtFirstNormalPos :
 forall p : float, Fnormal p -> (0 <= p)%R -> (firstNormalPos <= p)%R.
(* Goal: forall (p : float) (_ : Fnormal p) (_ : Rle (FtoRradix p) (IZR Z0)), Rle (FtoRradix p) (FtoRradix (Fopp firstNormalPos)) *)
intros p H' H'0.
(* Goal: Rle (FtoRradix firstNormalPos) (FtoRradix p) *)
case (Rle_or_lt firstNormalPos p); intros Lt0; auto with real.
(* Goal: Rle (FtoRradix firstNormalPos) (FtoRradix p) *)
case (FnormalLtPos p firstNormalPos); auto.
(* Goal: Fnormal firstNormalPos *)
(* Goal: forall _ : Z.lt (Fexp p) (Fexp firstNormalPos), Rle (FtoRradix firstNormalPos) (FtoRradix p) *)
(* Goal: forall _ : and (@eq Z (Fexp p) (Fexp firstNormalPos)) (Z.lt (Fnum p) (Fnum firstNormalPos)), Rle (FtoRradix firstNormalPos) (FtoRradix p) *)
apply firstNormalPosNormal.
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
intros H'1; Contradict H'1; unfold firstNormalPos in |- *; simpl in |- *.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply Zle_not_lt; auto with float.
(* Goal: forall _ : and (@eq Z (Fexp p) (Fexp firstNormalPos)) (Z.lt (Fnum p) (Fnum firstNormalPos)), Rle (FtoRradix firstNormalPos) (FtoRradix p) *)
intros H'1; elim H'1; intros H'2 H'3; Contradict H'3.
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
unfold firstNormalPos in |- *; simpl in |- *.
(* Goal: not (Z.lt (Fnum p) nNormMin) *)
apply Zle_not_lt.
(* Goal: Z.le nNormMin (Fnum p) *)
rewrite <- (Zabs_eq (Fnum p)); auto with float zarith.
(* Goal: Z.le nNormMin (Z.abs (Fnum p)) *)
(* Goal: Z.le Z0 (Fnum p) *)
apply pNormal_absolu_min; auto.
(* Goal: Z.le Z0 (Fnum p) *)
apply LeR0Fnum with (radix := radix); auto with arith.
Qed.
 
Theorem FnormalLtFirstNormalNeg :
 forall p : float, Fnormal p -> (p <= 0)%R -> (p <= Fopp firstNormalPos)%R.
(* Goal: forall (p : float) (_ : Fnormal p) (_ : Rle (FtoRradix p) (IZR Z0)), Rle (FtoRradix p) (FtoRradix (Fopp firstNormalPos)) *)
intros p H' H'0.
rewrite <- (Ropp_involutive p); unfold FtoRradix in |- *;
 repeat rewrite Fopp_correct.
(* Goal: Rle (Ropp (Ropp (FtoR radix p))) (Ropp (FtoR radix firstNormalPos)) *)
apply Ropp_le_contravar; rewrite <- Fopp_correct.
(* Goal: Rle (FtoR radix firstNormalPos) (FtoR radix (Fopp p)) *)
apply FnormalLtFirstNormalPos.
(* Goal: Fnormal (Fopp q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp p)) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp q)) *)
apply FnormalFop; auto.
replace 0%R with (-0)%R; unfold FtoRradix in |- *; try rewrite Fopp_correct;
 auto with real.
Qed.
 
Theorem FsubnormalDigit :
 forall p : float, Fsubnormal p -> Fdigit radix p < precision.
(* Goal: forall (p : float) (_ : Fsubnormal p), lt (Fdigit radix p) precision *)
intros p H; unfold Fdigit in |- *.
(* Goal: lt (digit radix (Fnum p)) precision *)
case (Z_eq_dec (Fnum p) 0); intros Z1.
(* Goal: lt (digit radix (Fnum p)) precision *)
(* Goal: lt (digit radix (Fnum p)) precision *)
rewrite Z1; simpl in |- *; auto with arith.
(* Goal: lt (digit radix (Fnum p)) precision *)
apply lt_S_n; apply le_lt_n_Sm.
(* Goal: le (S (digit radix (Fnum p))) precision *)
rewrite <- digitPredVNumiSPrecision.
(* Goal: le (S (digit radix (Fnum p))) (digit radix (Z.pred (Zpos (vNum b)))) *)
replace (S (digit radix (Fnum p))) with (digit radix (Fnum p) + 1).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite <- digitAdd; auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply digit_monotone; auto with float.
(* Goal: Z.le (Z.abs (Z.mul (Fnum p) (Zpower_nat radix (S O)))) (Z.abs (Z.pred (Zpos (vNum b)))) *)
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite (fun x => Zabs_eq (Zpred x)); auto with float zarith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum p) (Zpower_nat radix (S O)))) (Z.pred (Zpos (vNum b))) *)
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite Zmult_comm; rewrite Zpower_nat_1; auto with float zarith.
(* Goal: @eq nat (Init.Nat.add (digit radix (Fnum p)) (S O)) (S (digit radix (Fnum p))) *)
rewrite plus_comm; simpl in |- *; auto.
Qed.
Hint Resolve FsubnormalDigit: float.
 
Theorem pSubnormal_absolu_min :
 forall p : float, Fsubnormal p -> (Zabs (Fnum p) < nNormMin)%Z.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros p H'; apply Zlt_mult_simpl_l with (c := radix); auto with zarith.
(* Goal: Z.lt (Z.mul radix (Z.abs (Fnum p))) (Z.mul radix nNormMin) *)
replace (radix * Zabs (Fnum p))%Z with (Zabs (radix * Fnum p)).
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
replace (radix * nNormMin)%Z with (Zpos (vNum b)); auto with float.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: @eq Z (Zpower_nat radix precision) (Z.mul radix nNormMin) *)
(* Goal: @eq Z (Z.abs (Z.mul radix (Fnum p))) (Z.mul radix (Z.abs (Fnum p))) *)
replace precision with (1 + pred precision).
(* Goal: @eq Z (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.pred precision))) (Z.mul radix nNormMin) *)
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
(* Goal: @eq Z (Z.abs (Z.mul radix (Fnum p))) (Z.mul radix (Z.abs (Fnum p))) *)
rewrite Zpower_nat_is_exp; auto with zarith; rewrite Zpower_nat_1; auto.
(* Goal: @eq nat (Init.Nat.add (S O) (Init.Nat.pred precision)) precision *)
(* Goal: @eq Z (Z.abs (Z.mul radix (Fnum p))) (Z.mul radix (Z.abs (Fnum p))) *)
generalize precisionNotZero; case precision; simpl in |- *; auto.
(* Goal: forall _ : not (@eq nat O O), @eq nat (S O) O *)
(* Goal: @eq Z (Z.abs (Z.mul radix (Fnum p))) (Z.mul radix (Z.abs (Fnum p))) *)
intros H; Contradict H; auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_Zmult; rewrite (Zabs_eq radix); auto with zarith.
Qed.
 
Theorem FsubnormalLtFirstNormalPos :
 forall p : float, Fsubnormal p -> (0 <= p)%R -> (p < firstNormalPos)%R.
intros p H' H'0; unfold FtoRradix, FtoR, firstNormalPos in |- *;
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
 simpl in |- *.
replace (Fexp p) with (- dExp b)%Z.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
2: apply sym_equal; case H'; intros H1 H2; case H2; auto.
(* Goal: Rlt (Rmult (IZR (pPred (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp p)))) *)
apply Rmult_lt_compat_r; auto with real arith.
apply Rlt_IZR.
rewrite <- (Zabs_eq (Fnum p)).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
2: apply LeR0Fnum with (radix := radix); auto with zarith.
apply pSubnormal_absolu_min; auto.
Qed.
 
Theorem FsubnormalnormalLtPos :
 forall p q : float,
 Fsubnormal p -> Fnormal q -> (0 <= p)%R -> (0 <= q)%R -> (p < q)%R.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
(* Goal: Rlt (FtoRradix p) (FtoRradix q) *)
apply Rlt_le_trans with (r2 := FtoRradix firstNormalPos).
(* Goal: Rlt (FtoRradix p) (FtoRradix firstNormalPos) *)
(* Goal: Rle (FtoRradix firstNormalPos) (FtoRradix q) *)
apply FsubnormalLtFirstNormalPos; auto.
(* Goal: Rle (FtoRradix firstNormalPos) (FtoRradix q) *)
apply FnormalLtFirstNormalPos; auto.
Qed.
 
Theorem FsubnormalnormalLtNeg :
 forall p q : float,
 Fsubnormal p -> Fnormal q -> (p <= 0)%R -> (q <= 0)%R -> (q < p)%R.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
(* Goal: Rlt (FtoRradix q) (FtoRradix p) *)
rewrite <- (Ropp_involutive p); rewrite <- (Ropp_involutive q).
(* Goal: Rlt (Ropp (Ropp (FtoRradix q))) (Ropp (Ropp (FtoRradix p))) *)
apply Ropp_gt_lt_contravar; red in |- *.
(* Goal: Rlt (Ropp (FtoRradix p)) (Ropp (FtoRradix q)) *)
unfold FtoRradix in |- *; repeat rewrite <- Fopp_correct.
(* Goal: Rlt (FtoRradix q) (FtoRradix p) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply FsubnormalnormalLtPos; auto.
(* Goal: Fsubnormal (Fopp p) *)
(* Goal: Fnormal (Fopp q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp p)) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp q)) *)
apply FsubnormFopp; auto.
(* Goal: Fnormal (Fopp q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp p)) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp q)) *)
apply FnormalFop; auto.
unfold FtoRradix in |- *; rewrite Fopp_correct; replace 0%R with (-0)%R;
 auto with real.
unfold FtoRradix in |- *; rewrite Fopp_correct; replace 0%R with (-0)%R;
 auto with real.
Qed.
 
Definition Fnormalize (p : float) :=
  match Z_zerop (Fnum p) with
  | left _ => Float 0 (- dExp b)
  | right _ =>
      Fshift radix
        (min (precision - Fdigit radix p) (Zabs_nat (dExp b + Fexp p))) p
  end.
 
Theorem FnormalizeCorrect : forall p : float, Fnormalize p = p :>R.
(* Goal: forall p : float, @eq R (FtoRradix (Fnormalize p)) (FtoRradix p) *)
intros p; unfold Fnormalize in |- *.
(* Goal: @eq R (FtoRradix (if Z_zerop (Fnum p) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)) (FtoRradix p) *)
case (Z_zerop (Fnum p)).
case p; intros Fnum1 Fexp1 H'; unfold FtoRradix, FtoR in |- *; rewrite H';
 simpl in |- *; auto with real.
(* Goal: @eq R (Rmult (IZR Z0) (powerRZ (IZR radix) (Z.opp (Z.of_N (dExp b))))) (Rmult (IZR Z0) (powerRZ (IZR radix) Fexp1)) *)
(* Goal: forall _ : not (@eq Z (Fnum p) Z0), @eq R (FtoRradix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)) (FtoRradix p) *)
apply trans_eq with 0%R; auto with real.
(* Goal: forall _ : not (@eq Z (Fnum p) Z0), @eq R (FtoRradix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)) (FtoRradix p) *)
intros H'; unfold FtoRradix in |- *; apply FshiftCorrect; auto.
Qed.
 
Theorem Fnormalize_Fopp :
 forall p : float, Fnormalize (Fopp p) = Fopp (Fnormalize p).
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
intros p; case p; unfold Fnormalize in |- *; simpl in |- *.
(* Goal: forall Fnum Fexp : Z, @eq float (if Z_zerop (Z.opp Fnum) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Fopp (Float Fnum Fexp)))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp))) (Fopp (Float Fnum Fexp))) (Fopp (if Z_zerop Fnum then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Float Fnum Fexp))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp))) (Float Fnum Fexp))) *)
intros Fnum1 Fexp1; case (Z_zerop Fnum1); intros H'.
(* Goal: @eq float (if Z_zerop (Z.opp Fnum1) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Fopp (Float Fnum1 Fexp1)))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) (Fopp (Float Fnum1 Fexp1))) (Fopp (Float Z0 (Z.opp (Z.of_N (dExp b))))) *)
(* Goal: @eq float (if Z_zerop (Z.opp Fnum1) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Fopp (Float Fnum1 Fexp1)))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) (Fopp (Float Fnum1 Fexp1))) (Fopp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Float Fnum1 Fexp1))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) (Float Fnum1 Fexp1))) *)
rewrite H'; simpl in |- *; auto.
(* Goal: @eq float (if Z_zerop (Z.opp Fnum1) then Float Z0 (Z.opp (Z.of_N (dExp b))) else Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Fopp (Float Fnum1 Fexp1)))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) (Fopp (Float Fnum1 Fexp1))) (Fopp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix (Float Fnum1 Fexp1))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) (Float Fnum1 Fexp1))) *)
case (Z_zerop (- Fnum1)); intros H'0; simpl in |- *; auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case H'; replace Fnum1 with (- - Fnum1)%Z; auto with zarith.
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
unfold Fopp, Fshift, Fdigit in |- *; simpl in |- *.
(* Goal: @eq float (Float (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix (Z.opp Fnum1))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) (Z.sub Fexp1 (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix (Z.opp Fnum1))) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) (Float (Z.opp (Z.mul Fnum1 (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) (Z.sub Fexp1 (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) *)
replace (digit radix (- Fnum1)) with (digit radix Fnum1).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply floatEq; simpl in |- *; auto with zarith.
(* Goal: @eq Z (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) (Z.opp (Z.mul Fnum1 (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) *)
(* Goal: @eq nat (digit radix Fnum1) (digit radix (Z.opp Fnum1)) *)
ring.
(* Goal: @eq nat (digit radix Fnum1) (digit radix (Z.opp Fnum1)) *)
case Fnum1; simpl in |- *; auto.
Qed.
 
Theorem FnormalizeBounded :
 forall p : float, Fbounded b p -> Fbounded b (Fnormalize p).
(* Goal: forall (p : float) (_ : Fbounded b p), Fbounded b (Fnormalize p) *)
intros p H'; red in |- *; split.
(* Goal: forall _ : Fbounded b (Fnormalize p), Fcanonic (Fnormalize p) *)
unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H'0; simpl in |- *; auto with zarith.
(* Goal: forall _ : not (@eq Z (Fnum p) Z0), Z.lt (Z.abs (Fnum (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fnormalize p)) *)
intros H'0.
(* Goal: Z.lt (Z.abs (Fnum (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fnormalize p)) *)
apply digitGivesBoundedNum; auto.
(* Goal: le (Fdigit radix (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)) precision *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fnormalize p)) *)
rewrite FshiftFdigit; auto.
apply le_trans with (m := Fdigit radix p + (precision - Fdigit radix p));
 auto with arith.
(* Goal: le (Init.Nat.add (Fdigit radix p) (Init.Nat.sub precision (Fdigit radix p))) precision *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fnormalize p)) *)
rewrite <- le_plus_minus; auto.
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply pGivesDigit; auto.
(* Goal: forall _ : Fbounded b (Fnormalize p), Fcanonic (Fnormalize p) *)
unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
simpl in |- *; auto with zarith.
generalize H'; case p; unfold Fbounded, Fnormal, Fdigit in |- *;
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
 simpl in |- *.
(* Goal: forall (Fnum Fexp : Z) (_ : and (Z.lt (Z.abs Fnum) (Zpos (vNum b))) (Z.le (Z.opp (Z.of_N (dExp b))) Fexp)) (_ : not (@eq Z Fnum Z0)), Z.le (Z.opp (Z.of_N (dExp b))) (Z.sub Fexp (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp))))) *)
intros Fnum1 Fexp1 H'0 H'1.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Z.sub Fexp1 (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) *)
apply Zle_trans with (m := (Fexp1 - Zabs_nat (dExp b + Fexp1))%Z).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite inj_abs; auto with zarith.
(* Goal: Z.le (Z.sub Fexp1 (Z.of_nat (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))) (Z.sub Fexp1 (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) *)
unfold Zminus in |- *; apply Zplus_le_compat_l; auto.
(* Goal: Z.le (Z.opp (Z.of_nat (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))) (Z.opp (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) *)
apply Zle_Zopp; auto.
(* Goal: Z.le (Z.of_nat (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))) (Z.of_nat (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))) *)
apply inj_le; auto with arith.
Qed.
 
Theorem FnormalizeCanonic :
 forall p : float, Fbounded b p -> Fcanonic (Fnormalize p).
(* Goal: forall (p : float) (_ : Fcanonic p), @eq float (Fnormalize p) p *)
intros p H'.
(* Goal: Fcanonic (Fnormalize p) *)
generalize (FnormalizeBounded p H').
(* Goal: forall _ : Fbounded b (Fnormalize p), Fcanonic (Fnormalize p) *)
unfold Fnormalize in |- *; case (Z_zerop (Fnum p)); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H'0; right; repeat split; simpl in |- *; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.mul radix Z0)) (Zpos (vNum b)) *)
(* Goal: forall (_ : not (@eq Z (Fnum p) Z0)) (_ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
rewrite Zmult_comm; simpl in |- *; red in |- *; simpl in |- *; auto.
(* Goal: forall (_ : not (@eq Z (Fnum p) Z0)) (_ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros H'1.
case (min_or (precision - Fdigit radix p) (Zabs_nat (dExp b + Fexp p)));
 intros Min; case Min; clear Min; intros MinR MinL.
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros H'2; left; split; auto.
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
rewrite MinR; unfold Fshift in |- *; simpl in |- *.
apply
 Zle_trans
  with
    (Zabs
       (radix *
        (Zpower_nat radix (pred (Fdigit radix p)) *
         Zpower_nat radix (precision - Fdigit radix p)))).
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat rewrite <- Zpower_nat_is_exp; auto with zarith.
replace (1 + (pred (Fdigit radix p) + (precision - Fdigit radix p))) with
 precision; auto.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Zpower_nat radix precision)) *)
(* Goal: @eq nat precision (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.pred (Fdigit radix p)) (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
rewrite pGivesBound; auto with real.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
cut (Fdigit radix p <= precision); auto with float.
(* Goal: forall _ : le (Fdigit radix p) precision, @eq nat precision (Init.Nat.add (S O) (Init.Nat.add (Init.Nat.pred (Fdigit radix p)) (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
unfold Fdigit in |- *.
generalize (digitNotZero _ radixMoreThanOne _ H'1);
 case (digit radix (Fnum p)); simpl in |- *; auto.
(* Goal: forall (_ : lt O O) (_ : le O precision), @eq nat precision (S (Init.Nat.sub precision O)) *)
(* Goal: forall (n : nat) (_ : lt O (S n)) (_ : le (S n) precision), @eq nat precision (S (Init.Nat.add n (Init.Nat.sub precision (S n)))) *)
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros tmp; Contradict tmp; auto with arith.
(* Goal: forall (n : nat) (_ : lt O (S n)) (_ : le (S n) precision), @eq nat precision (S (Init.Nat.add n (Init.Nat.sub precision (S n)))) *)
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros n H H0; change (precision = S n + (precision - S n)) in |- *.
(* Goal: @eq nat precision (Init.Nat.add (S n) (Init.Nat.sub precision (S n))) *)
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply le_plus_minus; auto.
(* Goal: le (Fdigit radix p) precision *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply pGivesDigit; auto.
(* Goal: Z.lt (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
repeat rewrite Zabs_Zmult.
(* Goal: Z.le (Z.mul (Z.abs radix) (Z.mul (Z.abs (Zpower_nat radix (Init.Nat.pred (Fdigit radix p)))) (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) (Z.mul (Z.abs radix) (Z.mul (Z.abs (Fnum p)) (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply Zle_Zmult_comp_l.
(* Goal: Z.le Z0 (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: Z.le (Z.abs (Zpower_nat radix (Init.Nat.pred (Fdigit radix p)))) (Z.abs (Fnum p)) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply Zle_ZERO_Zabs.
(* Goal: Z.le (Z.mul (Z.abs (Zpower_nat radix (Init.Nat.pred (Fdigit radix p)))) (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p))))) (Z.mul (Z.abs (Fnum p)) (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p))))) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply Zle_Zmult_comp_r.
(* Goal: Z.le Z0 (Z.abs (Zpower_nat radix (Init.Nat.sub precision (Fdigit radix p)))) *)
(* Goal: Z.le (Z.abs (Zpower_nat radix (Init.Nat.pred (Fdigit radix p)))) (Z.abs (Fnum p)) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
apply Zle_ZERO_Zabs.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith.
(* Goal: Z.le (Zpower_nat radix (Init.Nat.pred (Fdigit radix p))) (Z.abs (Fnum p)) *)
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
unfold Fdigit in |- *; apply digitLess; auto.
(* Goal: forall _ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros H'0; right; split; auto; split.
(* Goal: @eq Z (Fexp (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: Z.lt (Z.abs (Z.mul radix (Fnum (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)))) (Zpos (vNum b)) *)
rewrite MinR; clear MinR; auto.
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))) p)) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: Z.lt (Z.abs (Z.mul radix (Fnum (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)))) (Zpos (vNum b)) *)
cut (- dExp b <= Fexp p)%Z; [ idtac | auto with float ].
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
case p; simpl in |- *.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros Fnum1 Fexp1 H'2; rewrite inj_abs; auto with zarith.
(* Goal: Z.lt (Z.abs (Z.mul radix (Fnum (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)))) (Zpos (vNum b)) *)
rewrite MinR.
(* Goal: Z.lt (Z.abs (Z.mul radix (Fnum (Fshift radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))) p)))) (Zpos (vNum b)) *)
rewrite <- (fun x => Zabs_eq (Zpos x)).
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
unfold Fshift in |- *; simpl in |- *.
apply
 Zlt_le_trans
  with
    (Zabs
       (radix *
        (Zpower_nat radix (Fdigit radix p) *
         Zpower_nat radix (Zabs_nat (dExp b + Fexp p))))).
(* Goal: Z.lt (Z.abs (Z.mul radix (Z.mul (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
repeat rewrite Zabs_Zmult.
(* Goal: Z.lt (Z.mul (Z.abs radix) (Z.mul (Z.abs (Fnum p)) (Z.abs (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Z.mul (Z.abs radix) (Z.mul (Z.abs (Zpower_nat radix (Fdigit radix p))) (Z.abs (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
apply Zmult_gt_0_lt_compat_l.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zlt_gt; rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt (Z.mul (Z.abs (Fnum p)) (Z.abs (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))))) (Z.mul (Z.abs (Zpower_nat radix (Fdigit radix p))) (Z.abs (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))))) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
apply Zmult_gt_0_lt_compat_r.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zlt_gt; rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith.
(* Goal: Z.lt (Z.abs (Fnum p)) (Zpower_nat radix (Fdigit radix p)) *)
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
unfold Fdigit in |- *; apply digitMore; auto.
(* Goal: Z.le (Z.abs (Z.mul radix (Z.mul (Zpower_nat radix (Fdigit radix p)) (Zpower_nat radix (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat rewrite <- Zpower_nat_is_exp; auto with zarith.
(* Goal: Z.le (Z.abs (Zpower_nat radix (Init.Nat.add (S O) (Init.Nat.add (Fdigit radix p) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p))))))) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
apply Zle_trans with (Zabs (Zpower_nat radix precision)).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat rewrite Zabs_eq; auto with zarith.
(* Goal: Z.le (Z.abs (Zpower_nat radix precision)) (Zpos (vNum b)) *)
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
rewrite pGivesBound.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith.
(* Goal: Z.le Z0 (Zpos (vNum b)) *)
red in |- *; simpl in |- *; red in |- *; intros; discriminate.
Qed.
 
Theorem NormalAndSubNormalNotEq :
 forall p q : float, Fnormal p -> Fsubnormal q -> p <> q :>R.
(* Goal: forall (_ : not (@eq Z (Fnum p) Z0)) (_ : Fbounded b (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p)), Fcanonic (Fshift radix (Nat.min (Init.Nat.sub precision (Fdigit radix p)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp p)))) p) *)
intros p q H' H'0; red in |- *; intros H'1.
(* Goal: False *)
case (Rtotal_order 0 p); intros H'2.
(* Goal: False *)
(* Goal: False *)
absurd (q < p)%R.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
rewrite <- H'1; auto with real.
(* Goal: Rlt (FtoRradix q) (FtoRradix p) *)
(* Goal: False *)
apply FsubnormalnormalLtPos; auto with real.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
rewrite <- H'1; auto with real.
(* Goal: False *)
absurd (p < q)%R.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
rewrite <- H'1; auto with real.
(* Goal: Rlt (FtoRradix p) (FtoRradix q) *)
apply FsubnormalnormalLtNeg; auto with real.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
rewrite <- H'1; auto with real.
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
elim H'2; intros H'3; try rewrite <- H'3; auto with real.
(* Goal: Rle (FtoRradix p) (IZR Z0) *)
elim H'2; intros H'3; try rewrite <- H'3; auto with real.
Qed.
 
Theorem FcanonicUnique :
 forall p q : float, Fcanonic p -> Fcanonic q -> p = q :>R -> p = q.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq float p q *)
intros p q H' H'0 H'1; case H'; case H'0; intros H'2 H'3.
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
apply FnormalUnique; auto.
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
Contradict H'1; apply NormalAndSubNormalNotEq; auto.
(* Goal: @eq float p q *)
(* Goal: @eq float p q *)
absurd (q = p :>R); auto; apply NormalAndSubNormalNotEq; auto.
(* Goal: @eq float p q *)
apply FsubnormalUnique; auto.
Qed.
 
Theorem FcanonicLeastExp :
 forall x y : float,
 x = y :>R -> Fbounded b x -> Fcanonic y -> (Fexp y <= Fexp x)%Z.
(* Goal: forall (x y : float) (_ : Fcanonic x) (_ : Fcanonic y) (_ : Rle (Rabs (FtoRradix x)) (Rabs (FtoRradix y))), Z.le (Fexp x) (Fexp y) *)
intros x y H H0 H1.
(* Goal: Z.le (Fexp y) (Fexp x) *)
cut (Fcanonic (Fnormalize x)); [ intros | apply FnormalizeCanonic; auto ].
replace y with (Fnormalize x);
 [ simpl in |- * | apply FcanonicUnique; auto with real ].
(* Goal: Z.le (Fexp (Fnormalize x)) (Fexp x) *)
(* Goal: @eq R (FtoRradix (Fnormalize x)) (FtoRradix y) *)
unfold Fnormalize in |- *.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
case (Z_zerop (Fnum x)); simpl in |- *; intros Z1; auto with float.
(* Goal: Z.le (Z.sub (Fexp x) (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))))) (Fexp x) *)
(* Goal: @eq R (FtoRradix (Fnormalize x)) (FtoRradix y) *)
apply Zplus_le_reg_l with (- Fexp x)%Z.
(* Goal: @eq Z (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) (Z.opp (Z.mul Fnum1 (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) *)
(* Goal: @eq nat (digit radix Fnum1) (digit radix (Z.opp Fnum1)) *)
replace (- Fexp x + Fexp x)%Z with (- (0))%Z; try ring.
replace
 (- Fexp x +
  (Fexp x - min (precision - Fdigit radix x) (Zabs_nat (dExp b + Fexp x))))%Z
 with (- min (precision - Fdigit radix x) (Zabs_nat (dExp b + Fexp x)))%Z;
(* Goal: @eq Z (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1))))) (Z.opp (Z.mul Fnum1 (Zpower_nat radix (Nat.min (Init.Nat.sub precision (digit radix Fnum1)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) Fexp1)))))) *)
(* Goal: @eq nat (digit radix Fnum1) (digit radix (Z.opp Fnum1)) *)
 try ring.
(* Goal: Z.le (Z.opp (Z.of_nat (Nat.min (Init.Nat.sub precision (Fdigit radix x)) (Z.abs_nat (Z.add (Z.of_N (dExp b)) (Fexp x)))))) (Z.opp Z0) *)
(* Goal: @eq R (FtoRradix (Fnormalize x)) (FtoRradix y) *)
apply Zle_Zopp; auto with arith zarith.
(* Goal: @eq R (FtoRradix (Fnormalize x)) (FtoRradix y) *)
rewrite <- H.
(* Goal: @eq R (FtoRradix (Fnormalize x)) (FtoRradix x) *)
apply FnormalizeCorrect.
Qed.
 
Theorem FcanonicLtPos :
 forall p q : float,
 Fcanonic p ->
 Fcanonic q ->
 (0 <= p)%R ->
 (p < q)%R -> (Fexp p < Fexp q)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2; case H'; case H'0.
(* Goal: forall (_ : Fnormal q) (_ : Fnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros H'3 H'4; apply FnormalLtPos; auto.
(* Goal: forall (_ : Fsubnormal q) (_ : Fnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros H'3 H'4; absurd (p < q)%R; auto.
(* Goal: not (Rlt (FtoRradix p) (FtoRradix q)) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply Rlt_asym.
(* Goal: Rlt (FtoRradix q) (FtoRradix p) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply FsubnormalnormalLtPos; auto.
(* Goal: Rle (IZR Z0) (FtoRradix q) *)
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply Rle_trans with (r2 := FtoRradix p); auto with real.
(* Goal: forall (_ : Fnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros H'3 H'4; case (Z_eq_dec (Fexp q) (- dExp b)); intros H'5.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
right; split.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite H'5; case H'4; intros H1 H2; case H2; auto.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith.
(* Goal: forall (_ : Fbounded b q) (_ : and (@eq Z (Fexp q) (Z.opp (Z.of_N (dExp b)))) (Z.lt (Z.abs (Z.mul radix (Fnum q))) (Zpos (vNum b)))), @eq Z (Fexp q) (Z.opp (Z.of_N (dExp b))) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite H'5; case H'4; intros H1 H2; case H2; auto.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
left.
replace (Fexp p) with (- dExp b)%Z;
 [ idtac | apply sym_equal; auto with float ].
(* Goal: Z.lt (Z.opp (Z.of_N (dExp b))) (Fexp q) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
case (Zle_lt_or_eq (- dExp b) (Fexp q)); auto with float zarith.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: forall (_ : Fsubnormal q) (_ : Fsubnormal p), or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros H'3 H'4; right; split.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply trans_equal with (- dExp b)%Z; auto with float.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
apply sym_equal; auto with float.
(* Goal: Z.lt (Fnum p) (Fnum q) *)
apply FsubnormalLt; auto.
Qed.
 
Theorem FcanonicLePos :
 forall p q : float,
 Fcanonic p ->
 Fcanonic q ->
 (0 <= p)%R ->
 (p <= q)%R -> (Fexp p < Fexp q)%Z \/ Fexp p = Fexp q /\ (Fnum p <= Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.le (Fnum p) (Fnum q))) *)
case H'2; intros H'3.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.le (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.le (Fnum p) (Fnum q))) *)
case FcanonicLtPos with (p := p) (q := q); auto with zarith arith.
(* Goal: or (Z.lt (Fexp p) (Fexp q)) (and (@eq Z (Fexp p) (Fexp q)) (Z.le (Fnum p) (Fnum q))) *)
rewrite FcanonicUnique with (p := p) (q := q); auto with zarith arith.
Qed.
 
Theorem Fcanonic_Rle_Zle :
 forall x y : float,
 Fcanonic x -> Fcanonic y -> (Rabs x <= Rabs y)%R -> (Fexp x <= Fexp y)%Z.
(* Goal: forall (x y : float) (_ : Fcanonic x) (_ : Fcanonic y) (_ : Rle (Rabs (FtoRradix x)) (Rabs (FtoRradix y))), Z.le (Fexp x) (Fexp y) *)
intros x y H H0 H1.
cut (forall z : float, Fexp z = Fexp (Fabs z) :>Z);
 [ intros E | intros; unfold Fabs in |- *; simpl in |- *; auto with zarith ].
(* Goal: Z.le (Fexp x) (Fexp y) *)
rewrite (E x); rewrite (E y).
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
cut (Fcanonic (Fabs x)); [ intros D | apply FcanonicFabs; auto ].
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
cut (Fcanonic (Fabs y)); [ intros G | apply FcanonicFabs; auto ].
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
case H1; intros Z2.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
case (FcanonicLtPos (Fabs x) (Fabs y)); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoRradix (Fabs x)) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Fabs y)) *)
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
rewrite (Fabs_correct radix); auto with real zarith.
(* Goal: Rle (IZR Z0) (FtoRradix (Fabs x)) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Fabs y)) *)
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
repeat rewrite (Fabs_correct radix); auto with real zarith.
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
rewrite (FcanonicUnique (Fabs x) (Fabs y)); auto with float zarith.
(* Goal: Rle (IZR Z0) (FtoRradix (Fabs x)) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Fabs y)) *)
(* Goal: Z.le (Fexp (Fabs x)) (Fexp (Fabs y)) *)
repeat rewrite (Fabs_correct radix); auto with real zarith.
Qed.
 
Theorem FcanonicLtNeg :
 forall p q : float,
 Fcanonic p ->
 Fcanonic q ->
 (q <= 0)%R ->
 (p < q)%R -> (Fexp q < Fexp p)%Z \/ Fexp p = Fexp q /\ (Fnum p < Fnum q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic p) (_ : Fcanonic q) (_ : Rle (FtoRradix q) (IZR Z0)) (_ : Rlt (FtoRradix p) (FtoRradix q)), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
intros p q H' H'0 H'1 H'2.
cut
 ((Fexp (Fopp q) < Fexp (Fopp p))%Z \/
  Fexp (Fopp q) = Fexp (Fopp p) /\ (Fnum (Fopp q) < Fnum (Fopp p))%Z).
(* Goal: forall _ : or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))), or (Z.lt (Fexp q) (Fexp p)) (and (@eq Z (Fexp p) (Fexp q)) (Z.lt (Fnum p) (Fnum q))) *)
(* Goal: or (Z.lt (Fexp (Fopp q)) (Fexp (Fopp p))) (and (@eq Z (Fexp (Fopp q)) (Fexp (Fopp p))) (Z.lt (Fnum (Fopp q)) (Fnum (Fopp p)))) *)
simpl in |- *.
intros H'3; elim H'3; clear H'3; intros H'3;
 [ idtac | elim H'3; clear H'3; intros H'3 H'4 ]; auto; 
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 right; split; auto with zarith.
apply FcanonicLtPos; try apply FcanonicFopp; auto; unfold FtoRradix in |- *;
 repeat rewrite Fopp_correct; replace 0%R with (-0)%R; 
 auto with real.
Qed.
 
Theorem FcanonicFnormalizeEq :
 forall p : float, Fcanonic p -> Fnormalize p = p.
(* Goal: forall (p : float) (_ : Fcanonic p), @eq float (Fnormalize p) p *)
intros p H'.
(* Goal: @eq float (Fnormalize p) p *)
apply FcanonicUnique; auto.
(* Goal: Fcanonic (Fnormalize p) *)
(* Goal: Fcanonic (Float (pPred (vNum b)) x) *)
(* Goal: forall _ : Z.lt (Fexp (Fnormalize p)) x, @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: forall _ : and (@eq Z (Fexp (Fnormalize p)) x) (Z.le (Fnum (Fnormalize p)) (pPred (vNum b))), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply FnormalizeCanonic; auto.
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoRradix (Fnormalize p)) (FtoRradix p) *)
apply FcanonicBound with (1 := H'); auto.
(* Goal: @eq R (FtoRradix (Fnormalize p)) (FtoRradix p) *)
apply FnormalizeCorrect; auto.
Qed.
 
Theorem FcanonicPosFexpRlt :
 forall x y : float,
 (0 <= x)%R ->
 (0 <= y)%R -> Fcanonic x -> Fcanonic y -> (Fexp x < Fexp y)%Z -> (x < y)%R.
(* Goal: forall (x y : float) (_ : Rle (FtoRradix x) (IZR Z0)) (_ : Rle (FtoRradix y) (IZR Z0)) (_ : Fcanonic x) (_ : Fcanonic y) (_ : Z.lt (Fexp x) (Fexp y)), Rlt (FtoRradix y) (FtoRradix x) *)
intros x y H' H'0 H'1 H'2 H'3.
(* Goal: Rlt (FtoRradix x) (FtoRradix y) *)
case (Rle_or_lt y x); auto.
(* Goal: forall _ : Rle (FtoRradix x) (FtoRradix y), Rlt (FtoRradix y) (FtoRradix x) *)
intros H'4; case H'4; clear H'4; intros H'4.
(* Goal: Rlt (FtoRradix x) (FtoRradix y) *)
(* Goal: Rlt (FtoRradix x) (FtoRradix y) *)
case FcanonicLtPos with (p := y) (q := x); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H'5; Contradict H'3; auto with zarith.
intros H'5; elim H'5; intros H'6 H'7; clear H'5; Contradict H'3; rewrite H'6;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
(* Goal: Rlt (FtoRradix y) (FtoRradix x) *)
Contradict H'3.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite FcanonicUnique with (p := x) (q := y); auto with zarith.
Qed.
 
Theorem FcanonicNegFexpRlt :
 forall x y : float,
 (x <= 0)%R ->
 (y <= 0)%R -> Fcanonic x -> Fcanonic y -> (Fexp x < Fexp y)%Z -> (y < x)%R.
(* Goal: forall (x y : float) (_ : Rle (FtoRradix x) (IZR Z0)) (_ : Rle (FtoRradix y) (IZR Z0)) (_ : Fcanonic x) (_ : Fcanonic y) (_ : Z.lt (Fexp x) (Fexp y)), Rlt (FtoRradix y) (FtoRradix x) *)
intros x y H' H'0 H'1 H'2 H'3.
(* Goal: Rlt (FtoRradix y) (FtoRradix x) *)
case (Rle_or_lt x y); auto.
(* Goal: forall _ : Rle (FtoRradix x) (FtoRradix y), Rlt (FtoRradix y) (FtoRradix x) *)
intros H'4; case H'4; clear H'4; intros H'4.
(* Goal: Rlt (FtoRradix y) (FtoRradix x) *)
(* Goal: Rlt (FtoRradix y) (FtoRradix x) *)
case FcanonicLtNeg with (p := x) (q := y); auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H'5; Contradict H'3; auto with zarith.
intros H'5; elim H'5; intros H'6 H'7; clear H'5; Contradict H'3; rewrite H'6;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
(* Goal: Rlt (FtoRradix y) (FtoRradix x) *)
Contradict H'3.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite FcanonicUnique with (p := x) (q := y); auto with zarith.
Qed.
 
Theorem FnormalBoundAbs2 :
 forall p : float,
 Fnormal p ->
 (Zpos (vNum b) * Float 1%nat (Zpred (Fexp p)) <= Fabs p)%R.
(* Goal: forall (p : float) (_ : Fnormal p), Rle (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Z.pred (Fexp p))))) (FtoRradix (Fabs p)) *)
intros p H'; unfold FtoRradix, FtoR in |- *; simpl in |- *.
replace (1 * powerRZ radix (Zpred (Fexp p)))%R with
 (powerRZ radix (Zpred (Fexp p))); [ idtac | ring ].
pattern (Fexp p) at 2 in |- *; replace (Fexp p) with (Zsucc (Zpred (Fexp p)));
 [ rewrite powerRZ_Zs; auto with real zarith
 | unfold Zsucc, Zpred in |- *; ring ].
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (IZR (Z.abs (Fnum p))) (Rmult (IZR radix) (powerRZ (IZR radix) (Z.pred (Fexp p))))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.pred (Fexp p)))) (Rmult (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) (powerRZ (IZR radix) (Z.pred (Fexp p)))) *)
apply Rmult_le_compat_r; auto with real arith.
(* Goal: Rle (IZR (Zpos (vNum b))) (Rmult (IZR (Z.abs (Fnum p))) (IZR radix)) *)
rewrite <- Rmult_IZR; apply Rle_IZR.
(* Goal: Z.le (Zpos (vNum b)) (Z.mul (Z.abs (Fnum p)) radix) *)
rewrite <- (Zabs_eq radix); auto with zarith.
(* Goal: forall (p : float) (_ : Fcanonic p), Z.lt (Z.abs (Fnum p)) (Zpos (vNum b)) *)
rewrite <- Zabs_Zmult; rewrite Zmult_comm; auto with float.
Qed.
 
Theorem vNumbMoreThanOne : (1 < Zpos (vNum b))%Z.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
replace 1%Z with (Z_of_nat 1); [ idtac | simpl in |- *; auto ].
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite <- (Zpower_nat_O radix); rewrite pGivesBound; auto with zarith.
Qed.
 
Theorem PosNormMin : Zpos (vNum b) = (radix * nNormMin)%Z.
pattern radix at 1 in |- *; rewrite <- (Zpower_nat_1 radix);
(* Goal: Z.le (Z.mul nNormMin radix) (Z.mul (Z.abs (Fnum p)) radix) *)
 unfold nNormMin in |- *.
(* Goal: Rle (IZR (Zpos (vNum b))) (IZR (Z.mul (Zpower_nat radix (Init.Nat.pred precision)) (Zpower_nat radix (S O)))) *)
rewrite pGivesBound; rewrite <- Zpower_nat_is_exp.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
generalize precisionNotZero; case precision; auto with zarith.
Qed.
 
Theorem FnormalPpred :
 forall x : Z, (- dExp b <= x)%Z -> Fnormal (Float (pPred (vNum b)) x).
intros x H;
 (cut (0 <= pPred (vNum b))%Z;
   [ intros Z1 | unfold pPred in |- *; auto with zarith ]).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat split; simpl in |- *; auto with zarith.
(* Goal: Z.lt (Z.abs (pPred (vNum b))) (Zpos (vNum b)) *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (pPred (vNum b)))) *)
rewrite (Zabs_eq (pPred (vNum b))).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
unfold pPred in |- *; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
unfold pPred in |- *; rewrite pGivesBound; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zle_trans with ((1 + 1) * pPred (vNum b))%Z; auto with zarith.
replace ((1 + 1) * pPred (vNum b))%Z with (pPred (vNum b) + pPred (vNum b))%Z;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
replace (Zpos (vNum b)) with (1 + Zpred (Zpos (vNum b)))%Z;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 unfold pPred in |- *; auto with zarith.
(* Goal: Z.le (Z.add (Zpos xH) (Z.pred (Zpos (vNum b)))) (Z.add (Z.pred (Zpos (vNum b))) (Z.pred (Zpos (vNum b)))) *)
apply Zplus_le_compat_r; apply Zle_Zpred.
(* Goal: Z.lt (Zpos xH) (Zpos (vNum b)) *)
apply vNumbMoreThanOne.
Qed.
 
Theorem FcanonicPpred :
 forall x : Z,
 (- dExp b <= x)%Z -> Fcanonic (Float (pPred (vNum b)) x).
(* Goal: forall (x : Z) (_ : Z.le (Z.opp (Z.of_N (dExp b))) x), Fcanonic (Float (pPred (vNum b)) x) *)
intros x H; left; apply FnormalPpred; auto.
Qed.
 
Theorem FnormalNnormMin :
 forall x : Z, (- dExp b <= x)%Z -> Fnormal (Float nNormMin x).
(* Goal: forall (x : Z) (_ : Z.le (Z.opp (Z.of_N (dExp b))) x), Fnormal (Float nNormMin x) *)
intros x H; (cut (0 < nNormMin)%Z; [ intros Z1 | apply nNormPos ]).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
repeat split; simpl in |- *; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite Zabs_eq; auto with zarith.
(* Goal: Z.lt nNormMin (Zpos (vNum b)) *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
rewrite PosNormMin.
pattern nNormMin at 1 in |- *; replace nNormMin with (1 * nNormMin)%Z;
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
 auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply Zmult_gt_0_lt_compat_r; auto with zarith.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
rewrite PosNormMin; auto with zarith.
Qed.
 
Theorem FcanonicNnormMin :
 forall x : Z, (- dExp b <= x)%Z -> Fcanonic (Float nNormMin x).
(* Goal: forall (x : Z) (_ : Z.le (Z.opp (Z.of_N (dExp b))) x), Fcanonic (Float nNormMin x) *)
intros x H; left; apply FnormalNnormMin; auto.
Qed.
 
Theorem boundedNorMinGivesExp :
 forall (x : Z) (p : float),
 Fbounded b p ->
 (- dExp b <= x)%Z ->
 (Float nNormMin x <= p)%R ->
 (p <= Float (pPred (vNum b)) x)%R -> Fexp (Fnormalize p) = x.
(* Goal: forall (x : Z) (p : float) (_ : Fbounded b p) (_ : Z.le (Z.opp (Z.of_N (dExp b))) x) (_ : Rle (FtoRradix (Float nNormMin x)) (FtoRradix p)) (_ : Rle (FtoRradix p) (FtoRradix (Float (pPred (vNum b)) x))), @eq Z (Fexp (Fnormalize p)) x *)
intros x p H' H'0 H'1 H'2.
(* Goal: @eq Z (Fexp (Fnormalize p)) x *)
cut (0 <= p)%R; [ intros Rle1 | idtac ].
case (FcanonicLePos (Float nNormMin x) (Fnormalize p));
 try rewrite FnormalizeCorrect; simpl in |- *; auto with float zarith.
(* Goal: Fcanonic (Float nNormMin x) *)
(* Goal: Fcanonic (Fnormalize p) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Float nNormMin x)) *)
(* Goal: forall _ : Z.lt x (Fexp (Fnormalize p)), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply FcanonicNnormMin; auto.
(* Goal: Fcanonic (Fnormalize p) *)
(* Goal: Fcanonic (Float (pPred (vNum b)) x) *)
(* Goal: forall _ : Z.lt (Fexp (Fnormalize p)) x, @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: forall _ : and (@eq Z (Fexp (Fnormalize p)) x) (Z.le (Fnum (Fnormalize p)) (pPred (vNum b))), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply FnormalizeCanonic; auto.
(* Goal: Rle (IZR Z0) (FtoRradix (Float nNormMin x)) *)
(* Goal: forall _ : Z.lt x (Fexp (Fnormalize p)), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply (LeFnumZERO radix); simpl in |- *; auto.
(* Goal: Z.lt Z0 nNormMin *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
apply Zlt_le_weak; apply nNormPos.
(* Goal: forall _ : Z.lt x (Fexp (Fnormalize p)), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
intros H'3.
case (FcanonicLePos (Fnormalize p) (Float (pPred (vNum b)) x));
 try rewrite FnormalizeCorrect; simpl in |- *; auto.
(* Goal: Fcanonic (Fnormalize p) *)
(* Goal: Fcanonic (Float (pPred (vNum b)) x) *)
(* Goal: forall _ : Z.lt (Fexp (Fnormalize p)) x, @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: forall _ : and (@eq Z (Fexp (Fnormalize p)) x) (Z.le (Fnum (Fnormalize p)) (pPred (vNum b))), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply FnormalizeCanonic; auto.
(* Goal: Fcanonic (Float (pPred (vNum b)) x) *)
(* Goal: forall _ : Z.lt (Fexp (Fnormalize p)) x, @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: forall _ : and (@eq Z (Fexp (Fnormalize p)) x) (Z.le (Fnum (Fnormalize p)) (pPred (vNum b))), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply FcanonicPpred; auto.
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
intros H'4; Contradict H'4; auto with zarith.
(* Goal: forall _ : and (@eq Z (Fexp (Fnormalize p)) x) (Z.le (Fnum (Fnormalize p)) (pPred (vNum b))), @eq Z (Fexp (Fnormalize p)) x *)
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
intros (H'4, H'5); auto.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
apply Rle_trans with (2 := H'1).
(* Goal: not (Z.lt (Fnum q) (Fnum q)) *)
(* Goal: @eq Z (Fexp p) (Fexp q) *)
(* Goal: not (Z.lt (Fnum p) (Fnum q)) *)
apply (LeFnumZERO radix); simpl in |- *; auto with zarith.
(* Goal: Z.lt Z0 nNormMin *)
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix nNormMin)) *)
apply Zlt_le_weak; apply nNormPos.
Qed.
 
End Fnormalized_Def.
Hint Resolve FnormalBounded FnormalPrecision: float.
Hint Resolve FnormalNotZero nNrMMimLevNum firstNormalPosNormal FsubnormFopp
  FsubnormalLtFirstNormalPos FnormalizeBounded FcanonicFopp FcanonicFabs
  FnormalizeCanonic: float.
Hint Resolve nNrMMimLevNum: arith.
Hint Resolve FsubnormalFbounded FsubnormalFexp FsubnormalDigit: float.
Hint Resolve FcanonicBound: float.
