Library Float.Fbound

Require Export Fop.
Section Fbounded_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

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

Coercion Z_of_N: N >-> Z.

Record Fbound : Set := Bound {vNum : positive; dExp : N}.

Definition Fbounded (b : Fbound) (d : float) :=
  (Z.abs (Fnum d) < Zpos (vNum b))%Z (- dExp b Fexp d)%Z.

Theorem FboundedNum :
  (b : Fbound) (p : float),
 Fbounded b p (Z.abs (Fnum p) < Zpos (vNum b))%Z.
intros b p H; case H; intros H1 H2; case H1; auto.
Qed.

Theorem FboundedExp :
  (b : Fbound) (p : float), Fbounded b p (- dExp b Fexp p)%Z.
intros b p H; case H; auto.
Qed.
Hint Resolve FboundedNum FboundedExp: float.

Theorem isBounded :
  (b : Fbound) (p : float), {Fbounded b p} + {¬ Fbounded b p}.
intros b p; case (Z_le_gt_dec (Zpos (vNum b)) (Z.abs (Fnum p)));
 intros H'.
right; red in |- *; intros H'3; Contradict H'; auto with float zarith.
case (Z_le_gt_dec (- dExp b) (Fexp p)); intros H'1.
left; repeat split; auto with zarith.
right; red in |- *; intros H'3; Contradict H'1; auto with float zarith.
Qed.

Theorem FzeroisZero : b : Fbound, Fzero (- dExp b) = 0%R :>R.
intros b; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
Qed.

Theorem FboundedFzero : b : Fbound, Fbounded b (Fzero (- dExp b)).
intros b; repeat (split; simpl in |- *).
replace 0%Z with (- 0%nat)%Z; [ idtac | simpl in |- *; auto ].
apply Zeq_le; auto with arith.
Qed.
Hint Unfold Fbounded.

Theorem FboundedZeroSameExp :
  (b : Fbound) (p : float), Fbounded b p Fbounded b (Fzero (Fexp p)).
intros b p H'; (repeat split; simpl in |- *; auto with float zarith).
Qed.

Theorem FBoundedScale :
  (b : Fbound) (p : float) (n : nat),
 Fbounded b p Fbounded b (Float (Fnum p) (Fexp p + n)).
intros b p n H'; repeat split; simpl in |- *; auto with float.
apply Z.le_trans with (Fexp p); auto with float.
pattern (Fexp p) at 1 in |- *;
 (replace (Fexp p) with (Fexp p + 0%nat)%Z; [ idtac | simpl in |- *; ring ]).
apply Zplus_le_compat_l.
apply inj_le; auto with arith.
Qed.

Theorem FvalScale :
  (b : Fbound) (p : float) (n : nat),
 Float (Fnum p) (Fexp p + n) = (powerRZ radix n × p)%R :>R.
intros b p n; unfold FtoRradix, FtoR in |- *; simpl in |- ×.
rewrite powerRZ_add; auto with real zarith.
ring.
Qed.

Theorem oppBounded :
  (b : Fbound) (x : float), Fbounded b x Fbounded b (Fopp x).
intros b x H'; repeat split; simpl in |- *; auto with float zarith.
replace (Z.abs (- Fnum x)) with (Z.abs (Fnum x)); auto with float.
case (Fnum x); simpl in |- *; auto.
Qed.

Theorem oppBoundedInv :
  (b : Fbound) (x : float), Fbounded b (Fopp x) Fbounded b x.
intros b x H'; rewrite <- (Fopp_Fopp x).
apply oppBounded; auto.
Qed.

Theorem FopRepAux :
  (b : Fbound) (z : Z) (p : R),
 ex (fun r : floatr = (- p)%R :>R Fbounded b r Fexp r = z)
 ex (fun r : floatr = p :>R Fbounded b r Fexp r = z).
intros b z p H'; elim H'; intros r E; elim E; intros H'0 H'1; elim H'1;
 intros H'2 H'3; clear H'1 E H'.
(Fopp r); split; auto.
rewrite <- (Ropp_involutive p).
rewrite <- H'0; auto.
unfold FtoRradix in |- *; apply Fopp_correct; auto.
split.
apply oppBounded; auto.
simpl in |- *; auto.
Qed.

Theorem absFBounded :
  (b : Fbound) (f : float), Fbounded b f Fbounded b (Fabs f).
intros b f H'; repeat split; simpl in |- *; auto with float.
replace (Z.abs (Z.abs (Fnum f))) with (Z.abs (Fnum f)); auto with float.
case (Fnum f); auto.
Qed.

Theorem FboundedEqExpPos :
  (b : Fbound) (p q : float),
 Fbounded b p
 p = q :>R (Fexp p Fexp q)%R (0 q)%R Fbounded b q.
intros b p q H' H'0 H'1 H'2.
cut (0 Fnum p)%Z;
 [ intros Z1
 | apply (LeR0Fnum radix); auto with real arith; fold FtoRradix in |- *;
    rewrite H'0; auto ].
cut (0 Fnum q)%Z;
 [ intros Z2 | apply (LeR0Fnum radix); auto with real arith ].
split.
apply Z.le_lt_trans with (Z.abs (Fnum p)); [ idtac | auto with float ].
repeat rewrite Z.abs_eq; auto.
apply Z.le_trans with (Fnum (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q));
 auto.
unfold Fshift in |- *; simpl in |- *; auto.
pattern (Fnum q) at 1 in |- *; replace (Fnum q) with (Fnum q × 1)%Z;
 auto with zarith.
apply (Rle_Fexp_eq_Zle radix); auto with real zarith.
rewrite FshiftCorrect; auto with real zarith.
unfold Fshift in |- *; simpl in |- *; rewrite inj_abs; try ring.
apply Zle_Zminus_ZERO; apply le_IZR; auto with real arith.
apply Z.le_trans with (Fexp p).
case H'; auto.
apply le_IZR; auto with real arith.
Qed.

Theorem FboundedEqExp :
  (b : Fbound) (p q : float),
 Fbounded b p p = q :>R (Fexp p Fexp q)%R Fbounded b q.
intros b p q H' H'0 H'1; split.
apply Z.le_lt_trans with (Z.abs (Fnum p)); [ idtac | auto with float ].
apply
 Z.le_trans with (Z.abs (Fnum (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q)));
 auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite Zabs_Zmult.
pattern (Z.abs (Fnum q)) at 1 in |- *;
 replace (Z.abs (Fnum q)) with (Z.abs (Fnum q) × 1%nat)%Z;
 [ apply Zle_Zmult_comp_l | auto with zarith ]; auto with zarith.
rewrite Z.abs_eq; simpl in |- *; auto with zarith.
simpl in |- *; ring.
cut (Fexp p Fexp q)%Z; [ intros E2 | idtac ].
apply le_IZR; auto.
apply (Rle_monotony_contra_exp radix) with (z := Fexp p);
 auto with real arith.
pattern (Fexp p) at 2 in |- *;
 replace (Fexp p) with (Fexp (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q));
 auto.
rewrite <- (fun xRabs_pos_eq (powerRZ radix x)); auto with real zarith.
rewrite <- Faux.Rabsolu_Zabs.
rewrite <- Rabs_mult.
change
  (Rabs (FtoRradix (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q))
   Z.abs (Fnum p) × powerRZ radix (Fexp p))%R in |- ×.
unfold FtoRradix in |- *; rewrite FshiftCorrect; auto.
fold FtoRradix in |- *; rewrite <- H'0.
rewrite <- (Fabs_correct radix); auto with real zarith.
unfold Fshift in |- *; simpl in |- ×.
rewrite inj_abs; [ ring | auto with zarith ].
cut (Fexp p Fexp q)%Z; [ intros E2 | apply le_IZR ]; auto.
apply Z.le_trans with (Fexp p); [ idtac | apply le_IZR ]; auto with float.
Qed.

Theorem eqExpLess :
  (b : Fbound) (p q : float),
 Fbounded b p
 p = q :>R
  r : float, Fbounded b r r = q :>R (Fexp q Fexp r)%R.
intros b p q H' H'0.
case (Rle_or_lt (Fexp q) (Fexp p)); intros H'1.
p; repeat (split; auto).
q; split; [ idtac | split ]; auto with real.
apply FboundedEqExp with (p := p); auto.
apply Rlt_le; auto.
Qed.

Theorem FboundedShiftLess :
  (b : Fbound) (f : float) (n m : nat),
 m n Fbounded b (Fshift radix n f) Fbounded b (Fshift radix m f).
intros b f n m H' H'0; split; auto.
simpl in |- *; auto.
apply Z.le_lt_trans with (Z.abs (Fnum (Fshift radix n f))).
simpl in |- *; replace m with (m + 0); auto with arith.
replace n with (m + (n - m)); auto with arith.
repeat rewrite Zpower_nat_is_exp.
repeat rewrite Zabs_Zmult; auto.
apply Zle_Zmult_comp_l; auto with zarith.
apply Zle_Zmult_comp_l; auto with zarith.
repeat rewrite Z.abs_eq; auto with zarith.
case H'0; auto.
apply Z.le_trans with (Fexp (Fshift radix n f)); auto with float.
simpl in |- *; unfold Zminus in |- *; auto with zarith.
Qed.

Theorem eqExpMax :
  (b : Fbound) (p q : float),
 Fbounded b p
 Fbounded b q
 (Fabs p q)%R
  r : float, Fbounded b r r = p :>R (Fexp r Fexp q)%Z.
intros b p q H' H'0 H'1; case (Zle_or_lt (Fexp p) (Fexp q)); intros Rl0.
p; auto.
cut ((Fexp p - Z.abs_nat (Fexp p - Fexp q))%Z = Fexp q);
 [ intros Eq1 | idtac ].
(Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p); split; split; auto.
apply Z.le_lt_trans with (Fnum q); auto with float.
replace (Z.abs (Fnum (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p))) with
 (Fnum (Fabs (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p)));
 auto.
apply (Rle_Fexp_eq_Zle radix); auto with arith.
rewrite Fabs_correct; auto with arith; rewrite FshiftCorrect; auto with arith;
 rewrite <- (Fabs_correct radix); auto with float arith.
rewrite <- (Z.abs_eq (Fnum q)); auto with float zarith.
apply (LeR0Fnum radix); auto.
apply Rle_trans with (2 := H'1); auto with real.
rewrite (Fabs_correct radix); auto with real zarith.
unfold Fshift in |- *; simpl in |- *; rewrite Eq1; auto with float.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
unfold Fshift in |- *; simpl in |- ×.
rewrite Eq1; auto with zarith.
rewrite inj_abs; auto with zarith; ring.
Qed.

Theorem Zle_monotony_contra_abs_pow :
  x y z n : Z,
 (0 < z)%Z
 (Rabs (x × powerRZ z n) Rabs (y × powerRZ z n))%R (Z.abs x Z.abs y)%Z.
intros x y z n Hz O1.
apply le_IZR; auto.
apply Rmult_le_reg_l with (r := powerRZ z n); auto with real zarith.
repeat rewrite (Rmult_comm (powerRZ z n)); auto.
repeat rewrite <- Faux.Rabsolu_Zabs.
replace (powerRZ z n) with (Rabs (powerRZ z n)).
repeat rewrite <- Rabs_mult; auto.
apply Rabs_pos_eq; auto with real zarith.
Qed.

Theorem LessExpBound :
  (b : Fbound) (p q : float),
 Fbounded b p
 Fbounded b q
 (Fexp q Fexp p)%Z
 (0 p)%R
 (p q)%R
  m : Z,
   Float m (Fexp q) = p :>R Fbounded b (Float m (Fexp q)).
intros b p q H' H'0 H'1 H'2 H'3;
  (Fnum p × Zpower_nat radix (Z.abs_nat (Fexp p - Fexp q)))%Z.
cut
 (Float (Fnum p × Zpower_nat radix (Z.abs_nat (Fexp p - Fexp q))) (Fexp q) = p
  :>R); [ intros Eq1 | idtac ].
split; auto.
repeat split; simpl in |- *; auto with float.
apply Z.le_lt_trans with (Z.abs (Fnum q)); auto with float.
apply Zle_monotony_contra_abs_pow with (z := radix) (n := Fexp q);
 auto with real arith.
unfold FtoRradix, FtoR in Eq1; simpl in Eq1; rewrite Eq1; auto with real.
change (Rabs p Rabs q)%R in |- ×.
repeat rewrite Rabs_pos_eq; auto with real.
apply Rle_trans with (1 := H'2); auto.
pattern (Fexp q) at 2 in |- *;
 replace (Fexp q) with (Fexp p - Z.abs_nat (Fexp p - Fexp q))%Z.
change (Fshift radix (Z.abs_nat (Fexp p - Fexp q)) p = p :>R) in |- ×.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
rewrite inj_abs; auto with zarith; ring.
Qed.

Theorem maxFbounded :
  (b : Fbound) (z : Z),
 (- dExp b z)%Z Fbounded b (Float (Z.pred (Zpos (vNum b))) z).
intros b z H; split; auto.
change (Z.abs (Z.pred (Zpos (vNum b))) < Zpos (vNum b))%Z in |- ×.
rewrite Z.abs_eq; auto with zarith.
Qed.

Theorem maxMax :
  (b : Fbound) (p : float) (z : Z),
 Fbounded b p
 (Fexp p z)%Z (Fabs p < Float (Zpos (vNum b)) z)%R.
intros b p z H' H'0; unfold FtoRradix in |- *;
 rewrite <-
  (FshiftCorrect _ radixMoreThanOne (Z.abs_nat (z - Fexp p))
     (Float (Zpos (vNum b)) z)); unfold Fshift in |- ×.
change
  (FtoR radix (Fabs p) <
   FtoR radix
     (Float (Zpos (vNum b) × Zpower_nat radix (Z.abs_nat (z - Fexp p)))
        (z - Z.abs_nat (z - Fexp p))))%R in |- ×.
replace (z - Z.abs_nat (z - Fexp p))%Z with (Fexp p).
unfold Fabs, FtoR in |- ×.
change
  (Z.abs (Fnum p) × powerRZ radix (Fexp p) <
   (Zpos (vNum b) × Zpower_nat radix (Z.abs_nat (z - Fexp p)))%Z ×
   powerRZ radix (Fexp p))%R in |- ×.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum b)));
 auto with real float zarith.
pattern (Zpos (vNum b)) at 1 in |- *;
 replace (Zpos (vNum b)) with (Zpos (vNum b) × 1)%Z;
 auto with real float zarith; ring.
rewrite inj_abs; auto with zarith; ring.
Qed.
End Fbounded_Def.
Hint Resolve FboundedFzero oppBounded absFBounded maxFbounded FboundedNum
  FboundedExp: float.