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) :=
(Zabs (Fnum d) < Zpos (vNum b))%Z ∧ (- dExp b ≤ Fexp d)%Z.
Theorem FboundedNum :
∀ (b : Fbound) (p : float),
Fbounded b p → (Zabs (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)) (Zabs (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 Zle_trans with (Fexp p); auto with float.
pattern (Fexp p) at 1 in |- *;
(replace (Fexp p) with (Fexp p + 0%nat)%Z; [ idtac | simpl in |- *; ring ]).
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 (Zabs (- Fnum x)) with (Zabs (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 : float ⇒ r = (- p)%R :>R ∧ Fbounded b r ∧ Fexp r = z) →
ex (fun r : float ⇒ r = p :>R ∧ Fbounded b r ∧ Fexp r = z).
intros b z p H'; elim H'; intros r E; elim E; intros H'0 H'1; elim H'1;
intros H'2 H'3; clear H'1 E H'.
∃ (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 (Zabs (Zabs (Fnum f))) with (Zabs (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 Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
repeat rewrite Zabs_eq; auto.
apply Zle_trans with (Fnum (Fshift radix (Zabs_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 Zle_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 Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
apply
Zle_trans with (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)));
auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite Zabs_Zmult.
pattern (Zabs (Fnum q)) at 1 in |- *;
replace (Zabs (Fnum q)) with (Zabs (Fnum q) × 1%nat)%Z;
[ apply Zle_Zmult_comp_l | auto with zarith ]; auto with zarith.
rewrite Zabs_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 (Zabs_nat (Fexp q - Fexp p)) q));
auto.
rewrite <- (fun x ⇒ Rabs_pos_eq (powerRZ radix x)); auto with real zarith.
rewrite <- Faux.Rabsolu_Zabs.
rewrite <- Rabs_mult.
change
(Rabs (FtoRradix (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)) ≤
Zabs (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 Zle_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 Zle_lt_trans with (Zabs (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 Zabs_eq; auto with zarith.
case H'0; auto.
apply Zle_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 - Zabs_nat (Fexp p - Fexp q))%Z = Fexp q);
[ intros Eq1 | idtac ].
∃ (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p); split; split; auto.
apply Zle_lt_trans with (Fnum q); auto with float.
replace (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p))) with
(Fnum (Fabs (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p)));
auto.
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 <- (Zabs_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 → (Zabs x ≤ Zabs 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 (Zabs_nat (Fexp p - Fexp q)))%Z.
cut
(Float (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p - Fexp q))) (Fexp q) = p
:>R); [ intros Eq1 | idtac ].
split; auto.
repeat split; simpl in |- *; auto with float.
apply Zle_lt_trans with (Zabs (Fnum q)); auto with float.
apply Zle_monotony_contra_abs_pow with (z := radix) (n := Fexp q);
auto with real arith.
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 - Zabs_nat (Fexp p - Fexp q))%Z.
change (Fshift radix (Zabs_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 (Zpred (Zpos (vNum b))) z).
intros b z H; split; auto.
change (Zabs (Zpred (Zpos (vNum b))) < Zpos (vNum b))%Z in |- ×.
rewrite Zabs_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 (Zabs_nat (z - Fexp p))
(Float (Zpos (vNum b)) z)); unfold Fshift in |- ×.
change
(FtoR radix (Fabs p) <
FtoR radix
(Float (Zpos (vNum b) × Zpower_nat radix (Zabs_nat (z - Fexp p)))
(z - Zabs_nat (z - Fexp p))))%R in |- ×.
replace (z - Zabs_nat (z - Fexp p))%Z with (Fexp p).
unfold Fabs, FtoR in |- ×.
change
(Zabs (Fnum p) × powerRZ radix (Fexp p) <
(Zpos (vNum b) × Zpower_nat radix (Zabs_nat (z - Fexp p)))%Z ×
powerRZ radix (Fexp p))%R in |- ×.
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.
Section Fbounded_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
Coercion Z_of_N: N >-> Z.
Record Fbound : Set := Bound {vNum : positive; dExp : N}.
Definition Fbounded (b : Fbound) (d : float) :=
(Zabs (Fnum d) < Zpos (vNum b))%Z ∧ (- dExp b ≤ Fexp d)%Z.
Theorem FboundedNum :
∀ (b : Fbound) (p : float),
Fbounded b p → (Zabs (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)) (Zabs (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 Zle_trans with (Fexp p); auto with float.
pattern (Fexp p) at 1 in |- *;
(replace (Fexp p) with (Fexp p + 0%nat)%Z; [ idtac | simpl in |- *; ring ]).
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 (Zabs (- Fnum x)) with (Zabs (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 : float ⇒ r = (- p)%R :>R ∧ Fbounded b r ∧ Fexp r = z) →
ex (fun r : float ⇒ r = p :>R ∧ Fbounded b r ∧ Fexp r = z).
intros b z p H'; elim H'; intros r E; elim E; intros H'0 H'1; elim H'1;
intros H'2 H'3; clear H'1 E H'.
∃ (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 (Zabs (Zabs (Fnum f))) with (Zabs (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 Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
repeat rewrite Zabs_eq; auto.
apply Zle_trans with (Fnum (Fshift radix (Zabs_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 Zle_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 Zle_lt_trans with (Zabs (Fnum p)); [ idtac | auto with float ].
apply
Zle_trans with (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)));
auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite Zabs_Zmult.
pattern (Zabs (Fnum q)) at 1 in |- *;
replace (Zabs (Fnum q)) with (Zabs (Fnum q) × 1%nat)%Z;
[ apply Zle_Zmult_comp_l | auto with zarith ]; auto with zarith.
rewrite Zabs_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 (Zabs_nat (Fexp q - Fexp p)) q));
auto.
rewrite <- (fun x ⇒ Rabs_pos_eq (powerRZ radix x)); auto with real zarith.
rewrite <- Faux.Rabsolu_Zabs.
rewrite <- Rabs_mult.
change
(Rabs (FtoRradix (Fshift radix (Zabs_nat (Fexp q - Fexp p)) q)) ≤
Zabs (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 Zle_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 Zle_lt_trans with (Zabs (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 Zabs_eq; auto with zarith.
case H'0; auto.
apply Zle_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 - Zabs_nat (Fexp p - Fexp q))%Z = Fexp q);
[ intros Eq1 | idtac ].
∃ (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p); split; split; auto.
apply Zle_lt_trans with (Fnum q); auto with float.
replace (Zabs (Fnum (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p))) with
(Fnum (Fabs (Fshift radix (Zabs_nat (Fexp p - Fexp q)) p)));
auto.
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 <- (Zabs_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 → (Zabs x ≤ Zabs 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 (Zabs_nat (Fexp p - Fexp q)))%Z.
cut
(Float (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p - Fexp q))) (Fexp q) = p
:>R); [ intros Eq1 | idtac ].
split; auto.
repeat split; simpl in |- *; auto with float.
apply Zle_lt_trans with (Zabs (Fnum q)); auto with float.
apply Zle_monotony_contra_abs_pow with (z := radix) (n := Fexp q);
auto with real arith.
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 - Zabs_nat (Fexp p - Fexp q))%Z.
change (Fshift radix (Zabs_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 (Zpred (Zpos (vNum b))) z).
intros b z H; split; auto.
change (Zabs (Zpred (Zpos (vNum b))) < Zpos (vNum b))%Z in |- ×.
rewrite Zabs_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 (Zabs_nat (z - Fexp p))
(Float (Zpos (vNum b)) z)); unfold Fshift in |- ×.
change
(FtoR radix (Fabs p) <
FtoR radix
(Float (Zpos (vNum b) × Zpower_nat radix (Zabs_nat (z - Fexp p)))
(z - Zabs_nat (z - Fexp p))))%R in |- ×.
replace (z - Zabs_nat (z - Fexp p))%Z with (Fexp p).
unfold Fabs, FtoR in |- ×.
change
(Zabs (Fnum p) × powerRZ radix (Fexp p) <
(Zpos (vNum b) × Zpower_nat radix (Zabs_nat (z - Fexp p)))%Z ×
powerRZ radix (Fexp p))%R in |- ×.
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.