Library Float.Ct2.FboundI
Require Export AllFloat.
Section FboundedI_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Record FboundI : Set := BoundI {vNumInf : nat; vNumSup : nat; dExpI : nat}.
Definition FboundedI (b : FboundI) (d : float) :=
((- vNumInf b ≤ Fnum d)%Z ∧ (Fnum d ≤ vNumSup b)%Z) ∧
(- dExpI b ≤ Fexp d)%Z.
Theorem isBoundedI :
∀ (b : FboundI) (p : float), {FboundedI b p} + {¬ FboundedI b p}.
intros b p; case (Z_le_gt_dec (Fnum p) (vNumSup b)); intros H'.
case (Z_le_gt_dec (- vNumInf b) (Fnum p)); intros H'0.
case (Z_le_gt_dec (- dExpI b) (Fexp p)); intros H'1.
left; repeat split; auto.
right; red in |- *; intros H'3; absurd (- dExpI b > Fexp p)%Z; elim H'3;
auto with zarith.
right; red in |- *; intros H'1; absurd (- vNumInf b > Fnum p)%Z; elim H'1;
auto with zarith.
right; red in |- *; intros H'0; absurd (Fnum p > vNumSup b)%Z; elim H'0;
auto with zarith.
Qed.
Theorem FboundedIFzero : ∀ b : FboundI, FboundedI b (Fzero (- dExpI b)).
intros b; repeat (split; simpl in |- *).
replace 0%Z with (- 0%nat)%Z; [ idtac | simpl in |- *; auto ].
apply Zle_Zopp; apply inj_le; auto with arith.
replace 0%Z with (Z_of_nat 0); [ idtac | simpl in |- *; auto ].
apply inj_le; auto with arith.
auto with zarith.
Qed.
Definition FnormalI (b : FboundI) (p : float) :=
FboundedI b p ∧
((vNumSup b < radix × Fnum p)%R ∨ (radix × Fnum p < (- vNumInf b)%Z)%R).
Theorem FnormalINotZero :
∀ (b : FboundI) (p : float), FnormalI b p → ¬ is_Fzero p.
intros b p H; elim H; intros H1 H2; unfold is_Fzero in |- ×.
case (Z_zerop (Fnum p)); auto; intros H3.
generalize H2; rewrite H3.
replace (radix × 0%Z)%R with 0%R; [ idtac | simpl; ring ].
clear H2; intros H2.
case H2; intros H4; clear H2.
absurd (vNumSup b < 0)%R; auto with arith real.
apply Rle_not_lt; auto with zarith real.
absurd (0 < (- vNumInf b)%Z)%R; auto.
apply Rle_not_lt; replace 0%R with (IZR (- (0))); auto with arith.
apply Rle_IZR; apply Zle_Zopp; auto with zarith.
Qed.
Theorem FnormalIUnique_aux :
∀ (b : FboundI) (p q : float),
FnormalI b p →
FnormalI b q → p = q :>R → (Fexp p < Fexp q)%Z → p = q :>float.
intros b p q Hp Hq H H'.
absurd (p = q :>R); auto.
elim Hq; intros H3 H4; case H4; clear H4; intros H4.
apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rle_lt_trans with (vNumSup b × powerRZ radix (Fexp p))%R.
apply Rmult_le_compat_r.
apply powerRZ_le; auto with real zarith.
rewrite INR_IZR_INZ; apply Rle_IZR; elim Hp; intros V1 V2; elim V1;
intros V3 V4; elim V3; auto with zarith.
apply Rle_lt_trans with (vNumSup b × powerRZ radix (Fexp q - 1%nat))%R.
apply Rmult_le_compat_l.
replace 0%R with (INR 0); auto with real arith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
unfold Zminus in |- *; rewrite powerRZ_add; auto with real zarith.
replace (radix × (Fnum q × powerRZ radix (Fexp q)))%R with
(radix × Fnum q × powerRZ radix (Fexp q))%R; [ idtac | ring ].
replace
(radix × (vNumSup b × (powerRZ radix (Fexp q) × powerRZ radix (- 1%nat))))%R
with (vNumSup b × powerRZ radix (Fexp q))%R.
apply Rmult_lt_compat_r; auto with real zarith.
simpl in |- *;
apply
trans_eq with (radix × / radix × (vNumSup b × powerRZ radix (Fexp q)))%R.
rewrite Rinv_r; auto with real zarith.
replace (radix × 1)%R with (IZR radix); ring; ring.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
replace (Fnum q × powerRZ radix (Fexp q))%R with
(radix × Fnum q × powerRZ radix (Fexp q + - 1%nat))%R.
apply
Rlt_le_trans with ((- vNumInf b)%Z × powerRZ radix (Fexp q + - 1%nat))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_trans with ((- vNumInf b)%Z × powerRZ radix (Fexp p))%R.
rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_l_reverse;
rewrite Ropp_mult_distr_l_reverse; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real arith zarith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q + - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_IZR; unfold FnormalI in Hp; unfold FboundedI in Hp; intuition.
rewrite powerRZ_add; auto with real zarith arith.
simpl in |- *; replace (radix × 1)%R with (IZR radix); simpl; try ring.
field; auto with zarith real.
Qed.
Theorem FnormalIUnique :
∀ (b : FboundI) (p q : float),
FnormalI b p → FnormalI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H.
case (Zle_or_lt (Fexp p) (Fexp q)); intros H1.
cut (∀ a b : Z, (a ≤ b)%Z → a = b ∨ (a < b)%Z);
[ intros F | idtac ].
2: intros x y V; omega.
lapply (F (Fexp p) (Fexp q)); [ intros H'1 | auto ].
case H'1; intros H2; clear F H'1.
apply sameExpEq with radix; auto.
apply FnormalIUnique_aux with b; auto.
apply sym_eq; apply FnormalIUnique_aux with b; auto.
Qed.
Definition FsubnormalI (b : FboundI) (p : float) :=
FboundedI b p ∧
Fexp p = (- dExpI b)%Z ∧
((- vNumInf b)%Z ≤ radix × Fnum p)%R ∧ (radix × Fnum p ≤ vNumSup b)%R.
Theorem FsubnormalIUnique :
∀ (b : FboundI) (p q : float),
FsubnormalI b p → FsubnormalI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H.
apply sameExpEq with radix; auto with zarith.
elim Hp; intros H0 H1; elim H1; clear H1; intros H1 H2.
elim Hq; intros H4 H5; elim H5; clear H5; intros H5 H6.
auto with zarith.
Qed.
Theorem NormalIandSubnormalINotEq :
∀ (b : FboundI) (p q : float),
FnormalI b p → FsubnormalI b q → p ≠ q :>R.
intros b p q Hp Hq.
elim Hp; intros H1 H2; elim Hq; intros H4 H3.
elim H3; intros H5 H6; clear H3.
elim H6; intros H3 H7; clear H6.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite H5.
case H2; intros H8.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
apply Rlt_le_trans with (Fnum p × powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rle_lt_trans with (INR (vNumSup b)); auto.
apply Rmult_le_compat_l.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix × 0)%R with (INR 0); auto with real arith.
apply Rle_trans with (INR (vNumSup b)); auto with real arith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
apply Rlt_dichotomy_converse; left.
apply Ropp_lt_cancel.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rlt_le_trans with (- Fnum p × powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Ropp_lt_gt_contravar.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rlt_le_trans with (IZR (- vNumInf b)); auto with real arith.
apply Rmult_le_compat_l.
replace 0%R with (-0)%R; auto with real; apply Ropp_le_contravar.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix × 0)%R with 0%R; auto with real.
apply Rle_trans with (IZR (- vNumInf b)); auto with real arith.
replace 0%R with (IZR 0); auto with real arith zarith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
Qed.
Definition FcanonicI (b : FboundI) (a : float) :=
FnormalI b a ∨ FsubnormalI b a.
Theorem FcanonicIUnique :
∀ (b : FboundI) (p q : float),
FcanonicI b p → FcanonicI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H; case Hp; case Hq; intros H1 H2.
apply FnormalIUnique with b; auto.
Contradict H; apply NormalIandSubnormalINotEq with b; auto.
Contradict H; apply not_eq_sym; apply NormalIandSubnormalINotEq with b; auto.
apply FsubnormalIUnique with b; auto.
Qed.
Theorem Zpower_nat_S :
∀ n : nat, Zpower_nat radix (S n) = (radix × Zpower_nat radix n)%Z.
intros n; replace (S n) with (1 + n); auto with arith.
Qed.
Fixpoint FNIAux (v N q : nat) {struct q} : nat :=
match q with
| O ⇒ 0
| S q' ⇒
match (Zpower_nat radix q' × v ?= radix × N)%Z with
| Datatypes.Lt ⇒ q'
| Datatypes.Eq ⇒ q'
| _ ⇒ FNIAux v N q'
end
end.
Definition FNI (q N : nat) := pred (FNIAux q N (S (S N))).
Theorem FNIAuxLess :
∀ v N q : nat,
0 < v → v ≤ N → (Zpower_nat radix (FNIAux v N q) × v ≤ radix × N)%Z.
intros v N q; elim q.
intros H1 H2; apply Zle_trans with (Z_of_nat v); simpl in |- ×.
apply Zeq_le; case v; auto with arith zarith.
apply Zle_trans with (Z_of_nat N); auto with arith zarith.
pattern (Z_of_nat N) at 1 in |- *; replace (Z_of_nat N) with (1 × N)%Z;
auto with arith zarith.
intros q1 H H1 H2.
simpl in |- *;
generalize (Zcompare_correct (Zpower_nat radix q1 × v) (radix × N));
case (Zpower_nat radix q1 × v ?= radix × N)%Z; auto with arith zarith.
Qed.
Theorem FNILess :
∀ q N : nat, 0 < q → q ≤ N → (Zpower_nat radix (FNI q N) × q ≤ N)%Z.
intros q N H1 H2; unfold FNI in |- ×.
apply Zmult_le_reg_r with radix; auto with zarith.
generalize (refl_equal (FNIAux q N (S (S N))));
pattern (FNIAux q N (S (S N))) at -1 in |- *; case (FNIAux q N (S (S N))).
intros H3; replace (Zpower_nat radix (pred 0) × q)%Z with (Z_of_nat q);
auto with arith zarith.
intros n H3; simpl in |- ×.
rewrite (Zmult_comm (Z_of_nat N) radix).
replace (Zpower_nat radix n × q × radix)%Z with
(Zpower_nat radix (FNIAux q N (S (S N))) × q)%Z;
[ apply FNIAuxLess; auto | idtac ].
rewrite H3; rewrite Zpower_nat_S; ring.
Qed.
Theorem FNIAuxMore :
∀ v N q : nat,
FNIAux v N q < pred q → (N < Zpower_nat radix (FNIAux v N q) × v)%Z.
intros v N q; elim q; simpl in |- ×.
intros H; inversion H.
intros q1 H'.
generalize (Zcompare_correct (Zpower_nat radix q1 × v) (radix × N));
case (Zpower_nat radix q1 × v ?= radix × N)%Z; auto with arith zarith.
intros H1 H2.
case (le_lt_or_eq (FNIAux v N q1) (pred q1)); auto with zarith arith.
intros H3; rewrite H3.
apply Zgt_lt; apply Zmult_gt_reg_r with radix; auto with zarith; apply Zlt_gt.
apply Zlt_le_trans with (Zpower_nat radix q1 × v)%Z; auto with zarith.
rewrite Zmult_comm; auto.
replace (Zpower_nat radix (pred q1) × v × radix)%Z with
(radix × Zpower_nat radix (pred q1) × v)%Z;
[ rewrite <- Zpower_nat_S | ring ].
apply Zmult_le_compat_r; auto with zarith.
Qed.
Theorem Zlt_Zpower_nat : ∀ n : nat, (n < Zpower_nat radix n)%Z.
intros n; induction n as [| n Hrecn].
simpl in |- *; auto with zarith.
rewrite Zpower_nat_S.
apply Zlt_le_trans with (1 + Zpower_nat radix n)%Z.
replace (Z_of_nat (S n)) with (1 + n)%Z; auto with arith zarith.
replace 1%Z with (Z_of_nat 1); auto with arith zarith.
rewrite <- inj_plus; auto with arith zarith.
apply Zle_trans with (Zpower_nat radix n + Zpower_nat radix n)%Z;
auto with zarith.
apply Zle_trans with (2 × Zpower_nat radix n)%Z; auto with zarith.
Qed.
Theorem FNIMore :
∀ N q : nat,
0 < q → q ≤ N → (N < radix × (Zpower_nat radix (FNI q N) × q))%Z.
intros N q; case q.
intros H; inversion H.
intros q' H H'; unfold FNI in |- ×.
apply
Zlt_le_trans with (Zpower_nat radix (FNIAux (S q') N (S (S N))) × S q')%Z.
apply FNIAuxMore; auto with arith zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
case (FNIAux (S q') N (S (S N))).
simpl in |- *; auto with arith.
intros n0 H2; replace (pred (S (S N))) with (S N); auto with arith.
rewrite <- H2.
apply Zpower_nat_anti_monotone_lt with radix; auto with arith zarith.
apply Zgt_lt; apply Zmult_gt_reg_r with (Z_of_nat (S q'));
auto with zarith arith; apply Zlt_gt.
apply Zlt_le_trans with (Z_of_nat 1); auto with zarith arith.
apply Zle_lt_trans with (radix × N)%Z.
apply FNIAuxLess; auto with zarith arith.
apply Zle_lt_trans with (radix × N × S q')%Z; auto with zarith arith.
pattern (radix × N)%Z at 1 in |- *;
replace (radix × N)%Z with (radix × N × 1%nat)%Z;
auto with arith zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Zmult_gt_0_lt_compat_r; auto with zarith arith.
apply Zlt_gt; auto with arith zarith.
rewrite Zpower_nat_S; apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply Zlt_Zpower_nat.
rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
case (FNIAux (S q') N (S (S N))).
intros H1; simpl in |- *; auto with zarith arith.
intros H1; rewrite <- Zpower_nat_S; auto with zarith arith.
Qed.
Definition FnormalizeI (b : FboundI) (p : float) :=
match (0 ?= Fnum p)%Z with
| Datatypes.Eq ⇒ Float 0 (- dExpI b)
| Datatypes.Lt ⇒
Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
(Zabs_nat (Fexp p + dExpI b))) p
| Datatypes.Gt ⇒
Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
(Zabs_nat (Fexp p + dExpI b))) p
end.
Theorem FnormalizeICorrect :
∀ (b : FboundI) (p : float), FnormalizeI b p = p :>R.
intros b p; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite <- H; simpl; ring.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
Qed.
Theorem FnormalizeIBounded :
∀ (b : FboundI) (p : float),
FboundedI b p → FboundedI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
replace (Float 0 (- dExpI b)) with (Fzero (- dExpI b));
[ apply FboundedIFzero | unfold Fzero in |- *; auto ].
unfold Fshift in |- ×.
repeat split; simpl in |- ×.
apply Zle_trans with 0%Z; auto with zarith arith.
apply
Zle_trans
with (Fnum p × Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b)))%Z;
auto with zarith arith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (Zabs (Fnum p));
[ rewrite Zabs_absolu; rewrite Zmult_comm
| apply Zabs_eq; auto with zarith ].
apply FNILess; auto with arith zarith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith; elim H; intuition.
apply
Zplus_le_reg_l
with
(dExpI b +
min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
Zle_trans
with
(Z_of_nat
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
(Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
[ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
unfold Fshift in |- ×.
repeat split; simpl in |- ×.
2: apply Zle_trans with 0%Z; auto with zarith arith.
2: cut (∀ x y : Z, (x ≤ 0)%Z → (0 ≤ y)%Z → (x × y ≤ 0)%Z);
[ intros F; apply F | intros x y H3 H2 ]; auto with zarith.
2: rewrite <- (Zopp_involutive (x × y));
rewrite <- (Zopp_involutive 0).
2: apply Zle_Zopp; simpl in |- *; rewrite <- Zopp_mult_distr_l_reverse;
auto with zarith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (- Zabs_nat (Fnum p))%Z;
auto with zarith.
rewrite Zopp_mult_distr_l_reverse; apply Zle_Zopp.
apply
Zle_trans
with
(Zabs_nat (Fnum p) ×
Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b)))%Z.
apply Zle_Zmult_comp_l; auto with zarith arith.
rewrite Zmult_comm; apply FNILess.
rewrite <- absolu_Zopp; auto with zarith arith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe.
rewrite <- (Zopp_involutive (Z_of_nat (vNumInf b))).
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zle_Zopp; elim H; intuition.
rewrite <- absolu_Zopp; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith.
apply
Zplus_le_reg_l
with
(dExpI b +
min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
Zle_trans
with
(Z_of_nat
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
(Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
[ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
Qed.
Theorem FcanonicIBoundedI :
∀ (b : FboundI) (p : float), FcanonicI b p → FboundedI b p.
intros b p H.
case H; intros H1; elim H1; auto.
Qed.
Theorem FnormalizeIFcanonicI :
∀ (b : FboundI) (p : float),
FboundedI b p → FcanonicI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
unfold FcanonicI in |- *; right.
repeat split; simpl in |- *; auto with zarith.
replace (radix × 0)%R with (IZR 0); auto with zarith real.
replace (radix × 0)%R with (INR 0); auto with zarith real arith.
case
(min_or (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)));
intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
(Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))
p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; auto.
left; unfold Fshift in |- *; simpl in |- ×.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zabs_eq (Fnum p));
auto with zarith; rewrite Zabs_absolu.
rewrite <- Rmult_IZR; rewrite INR_IZR_INZ; apply Rlt_IZR.
rewrite
(Zmult_comm (Zabs_nat (Fnum p))
(Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b))))
.
apply FNIMore.
apply lt_Zlt_inv; simpl in |- *; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith;
elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
[ intros H4 | auto with zarith ].
case
(Rle_or_lt
(radix × (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z)
(vNumSup b)); intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- ×.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
replace 0%R with (IZR 0); auto with real zarith.
rewrite Rmult_IZR; auto with real arith zarith.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
cut (0 < - Fnum p)%Z; [ intros Y | auto with zarith ].
case
(min_or (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)));
intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
(Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))
p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H2; auto with zarith.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H4; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H4; absurd (0 < Fnum p)%Z; auto with zarith.
right; unfold Fshift in |- *; simpl in |- ×.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zopp_involutive (Fnum p));
rewrite <- (Zabs_eq (- Fnum p)); auto with zarith.
rewrite Zopp_mult_distr_l_reverse; rewrite <- Rmult_IZR;
rewrite Zmult_comm; rewrite Zopp_mult_distr_l_reverse.
apply Rlt_IZR; apply Zlt_Zopp.
rewrite Zabs_absolu; rewrite absolu_Zopp.
rewrite Zmult_comm;
rewrite
(Zmult_comm (Zabs_nat (Fnum p))
(Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b))))
.
apply FNIMore; auto with zarith.
rewrite <- absolu_Zopp; apply lt_Zlt_inv; simpl in |- *;
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith; elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
[ intros H4 | auto with zarith ].
case
(Rle_or_lt (- vNumInf b)%Z
(radix × (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z));
intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- ×.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- ×.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
apply Ropp_le_cancel.
rewrite Rmult_comm; rewrite <- Ropp_mult_distr_l_reverse; rewrite Rmult_comm.
replace (-0)%R with 0%R; auto with real.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
rewrite <- Ropp_Ropp_IZR; rewrite Zmult_comm.
rewrite Zopp_mult_distr_r; rewrite Zmult_comm; auto with zarith real.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- ×.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
Qed.
End FboundedI_Def.
Section FboundedI_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Record FboundI : Set := BoundI {vNumInf : nat; vNumSup : nat; dExpI : nat}.
Definition FboundedI (b : FboundI) (d : float) :=
((- vNumInf b ≤ Fnum d)%Z ∧ (Fnum d ≤ vNumSup b)%Z) ∧
(- dExpI b ≤ Fexp d)%Z.
Theorem isBoundedI :
∀ (b : FboundI) (p : float), {FboundedI b p} + {¬ FboundedI b p}.
intros b p; case (Z_le_gt_dec (Fnum p) (vNumSup b)); intros H'.
case (Z_le_gt_dec (- vNumInf b) (Fnum p)); intros H'0.
case (Z_le_gt_dec (- dExpI b) (Fexp p)); intros H'1.
left; repeat split; auto.
right; red in |- *; intros H'3; absurd (- dExpI b > Fexp p)%Z; elim H'3;
auto with zarith.
right; red in |- *; intros H'1; absurd (- vNumInf b > Fnum p)%Z; elim H'1;
auto with zarith.
right; red in |- *; intros H'0; absurd (Fnum p > vNumSup b)%Z; elim H'0;
auto with zarith.
Qed.
Theorem FboundedIFzero : ∀ b : FboundI, FboundedI b (Fzero (- dExpI b)).
intros b; repeat (split; simpl in |- *).
replace 0%Z with (- 0%nat)%Z; [ idtac | simpl in |- *; auto ].
apply Zle_Zopp; apply inj_le; auto with arith.
replace 0%Z with (Z_of_nat 0); [ idtac | simpl in |- *; auto ].
apply inj_le; auto with arith.
auto with zarith.
Qed.
Definition FnormalI (b : FboundI) (p : float) :=
FboundedI b p ∧
((vNumSup b < radix × Fnum p)%R ∨ (radix × Fnum p < (- vNumInf b)%Z)%R).
Theorem FnormalINotZero :
∀ (b : FboundI) (p : float), FnormalI b p → ¬ is_Fzero p.
intros b p H; elim H; intros H1 H2; unfold is_Fzero in |- ×.
case (Z_zerop (Fnum p)); auto; intros H3.
generalize H2; rewrite H3.
replace (radix × 0%Z)%R with 0%R; [ idtac | simpl; ring ].
clear H2; intros H2.
case H2; intros H4; clear H2.
absurd (vNumSup b < 0)%R; auto with arith real.
apply Rle_not_lt; auto with zarith real.
absurd (0 < (- vNumInf b)%Z)%R; auto.
apply Rle_not_lt; replace 0%R with (IZR (- (0))); auto with arith.
apply Rle_IZR; apply Zle_Zopp; auto with zarith.
Qed.
Theorem FnormalIUnique_aux :
∀ (b : FboundI) (p q : float),
FnormalI b p →
FnormalI b q → p = q :>R → (Fexp p < Fexp q)%Z → p = q :>float.
intros b p q Hp Hq H H'.
absurd (p = q :>R); auto.
elim Hq; intros H3 H4; case H4; clear H4; intros H4.
apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rle_lt_trans with (vNumSup b × powerRZ radix (Fexp p))%R.
apply Rmult_le_compat_r.
apply powerRZ_le; auto with real zarith.
rewrite INR_IZR_INZ; apply Rle_IZR; elim Hp; intros V1 V2; elim V1;
intros V3 V4; elim V3; auto with zarith.
apply Rle_lt_trans with (vNumSup b × powerRZ radix (Fexp q - 1%nat))%R.
apply Rmult_le_compat_l.
replace 0%R with (INR 0); auto with real arith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
unfold Zminus in |- *; rewrite powerRZ_add; auto with real zarith.
replace (radix × (Fnum q × powerRZ radix (Fexp q)))%R with
(radix × Fnum q × powerRZ radix (Fexp q))%R; [ idtac | ring ].
replace
(radix × (vNumSup b × (powerRZ radix (Fexp q) × powerRZ radix (- 1%nat))))%R
with (vNumSup b × powerRZ radix (Fexp q))%R.
apply Rmult_lt_compat_r; auto with real zarith.
simpl in |- *;
apply
trans_eq with (radix × / radix × (vNumSup b × powerRZ radix (Fexp q)))%R.
rewrite Rinv_r; auto with real zarith.
replace (radix × 1)%R with (IZR radix); ring; ring.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
replace (Fnum q × powerRZ radix (Fexp q))%R with
(radix × Fnum q × powerRZ radix (Fexp q + - 1%nat))%R.
apply
Rlt_le_trans with ((- vNumInf b)%Z × powerRZ radix (Fexp q + - 1%nat))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_trans with ((- vNumInf b)%Z × powerRZ radix (Fexp p))%R.
rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_l_reverse;
rewrite Ropp_mult_distr_l_reverse; apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real arith zarith.
apply Rle_powerRZ; auto with real arith zarith.
apply Zlt_succ_le.
replace (Zsucc (Fexp q + - 1%nat)) with (Fexp q); auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_IZR; unfold FnormalI in Hp; unfold FboundedI in Hp; intuition.
rewrite powerRZ_add; auto with real zarith arith.
simpl in |- *; replace (radix × 1)%R with (IZR radix); simpl; try ring.
field; auto with zarith real.
Qed.
Theorem FnormalIUnique :
∀ (b : FboundI) (p q : float),
FnormalI b p → FnormalI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H.
case (Zle_or_lt (Fexp p) (Fexp q)); intros H1.
cut (∀ a b : Z, (a ≤ b)%Z → a = b ∨ (a < b)%Z);
[ intros F | idtac ].
2: intros x y V; omega.
lapply (F (Fexp p) (Fexp q)); [ intros H'1 | auto ].
case H'1; intros H2; clear F H'1.
apply sameExpEq with radix; auto.
apply FnormalIUnique_aux with b; auto.
apply sym_eq; apply FnormalIUnique_aux with b; auto.
Qed.
Definition FsubnormalI (b : FboundI) (p : float) :=
FboundedI b p ∧
Fexp p = (- dExpI b)%Z ∧
((- vNumInf b)%Z ≤ radix × Fnum p)%R ∧ (radix × Fnum p ≤ vNumSup b)%R.
Theorem FsubnormalIUnique :
∀ (b : FboundI) (p q : float),
FsubnormalI b p → FsubnormalI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H.
apply sameExpEq with radix; auto with zarith.
elim Hp; intros H0 H1; elim H1; clear H1; intros H1 H2.
elim Hq; intros H4 H5; elim H5; clear H5; intros H5 H6.
auto with zarith.
Qed.
Theorem NormalIandSubnormalINotEq :
∀ (b : FboundI) (p q : float),
FnormalI b p → FsubnormalI b q → p ≠ q :>R.
intros b p q Hp Hq.
elim Hp; intros H1 H2; elim Hq; intros H4 H3.
elim H3; intros H5 H6; clear H3.
elim H6; intros H3 H7; clear H6.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite H5.
case H2; intros H8.
apply not_eq_sym; apply Rlt_dichotomy_converse; left.
apply Rlt_le_trans with (Fnum p × powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rle_lt_trans with (INR (vNumSup b)); auto.
apply Rmult_le_compat_l.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix × 0)%R with (INR 0); auto with real arith.
apply Rle_trans with (INR (vNumSup b)); auto with real arith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
apply Rlt_dichotomy_converse; left.
apply Ropp_lt_cancel.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rlt_le_trans with (- Fnum p × powerRZ radix (- dExpI b))%R.
apply Rmult_lt_compat_r.
apply powerRZ_lt; auto with real zarith.
apply Ropp_lt_gt_contravar.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rlt_le_trans with (IZR (- vNumInf b)); auto with real arith.
apply Rmult_le_compat_l.
replace 0%R with (-0)%R; auto with real; apply Ropp_le_contravar.
apply Rmult_le_reg_l with (IZR radix); auto with real zarith.
replace (radix × 0)%R with 0%R; auto with real.
apply Rle_trans with (IZR (- vNumInf b)); auto with real arith.
replace 0%R with (IZR 0); auto with real arith zarith.
apply Rle_powerRZ; auto with real arith.
elim H1; auto.
Qed.
Definition FcanonicI (b : FboundI) (a : float) :=
FnormalI b a ∨ FsubnormalI b a.
Theorem FcanonicIUnique :
∀ (b : FboundI) (p q : float),
FcanonicI b p → FcanonicI b q → p = q :>R → p = q :>float.
intros b p q Hp Hq H; case Hp; case Hq; intros H1 H2.
apply FnormalIUnique with b; auto.
Contradict H; apply NormalIandSubnormalINotEq with b; auto.
Contradict H; apply not_eq_sym; apply NormalIandSubnormalINotEq with b; auto.
apply FsubnormalIUnique with b; auto.
Qed.
Theorem Zpower_nat_S :
∀ n : nat, Zpower_nat radix (S n) = (radix × Zpower_nat radix n)%Z.
intros n; replace (S n) with (1 + n); auto with arith.
Qed.
Fixpoint FNIAux (v N q : nat) {struct q} : nat :=
match q with
| O ⇒ 0
| S q' ⇒
match (Zpower_nat radix q' × v ?= radix × N)%Z with
| Datatypes.Lt ⇒ q'
| Datatypes.Eq ⇒ q'
| _ ⇒ FNIAux v N q'
end
end.
Definition FNI (q N : nat) := pred (FNIAux q N (S (S N))).
Theorem FNIAuxLess :
∀ v N q : nat,
0 < v → v ≤ N → (Zpower_nat radix (FNIAux v N q) × v ≤ radix × N)%Z.
intros v N q; elim q.
intros H1 H2; apply Zle_trans with (Z_of_nat v); simpl in |- ×.
apply Zeq_le; case v; auto with arith zarith.
apply Zle_trans with (Z_of_nat N); auto with arith zarith.
pattern (Z_of_nat N) at 1 in |- *; replace (Z_of_nat N) with (1 × N)%Z;
auto with arith zarith.
intros q1 H H1 H2.
simpl in |- *;
generalize (Zcompare_correct (Zpower_nat radix q1 × v) (radix × N));
case (Zpower_nat radix q1 × v ?= radix × N)%Z; auto with arith zarith.
Qed.
Theorem FNILess :
∀ q N : nat, 0 < q → q ≤ N → (Zpower_nat radix (FNI q N) × q ≤ N)%Z.
intros q N H1 H2; unfold FNI in |- ×.
apply Zmult_le_reg_r with radix; auto with zarith.
generalize (refl_equal (FNIAux q N (S (S N))));
pattern (FNIAux q N (S (S N))) at -1 in |- *; case (FNIAux q N (S (S N))).
intros H3; replace (Zpower_nat radix (pred 0) × q)%Z with (Z_of_nat q);
auto with arith zarith.
intros n H3; simpl in |- ×.
rewrite (Zmult_comm (Z_of_nat N) radix).
replace (Zpower_nat radix n × q × radix)%Z with
(Zpower_nat radix (FNIAux q N (S (S N))) × q)%Z;
[ apply FNIAuxLess; auto | idtac ].
rewrite H3; rewrite Zpower_nat_S; ring.
Qed.
Theorem FNIAuxMore :
∀ v N q : nat,
FNIAux v N q < pred q → (N < Zpower_nat radix (FNIAux v N q) × v)%Z.
intros v N q; elim q; simpl in |- ×.
intros H; inversion H.
intros q1 H'.
generalize (Zcompare_correct (Zpower_nat radix q1 × v) (radix × N));
case (Zpower_nat radix q1 × v ?= radix × N)%Z; auto with arith zarith.
intros H1 H2.
case (le_lt_or_eq (FNIAux v N q1) (pred q1)); auto with zarith arith.
intros H3; rewrite H3.
apply Zgt_lt; apply Zmult_gt_reg_r with radix; auto with zarith; apply Zlt_gt.
apply Zlt_le_trans with (Zpower_nat radix q1 × v)%Z; auto with zarith.
rewrite Zmult_comm; auto.
replace (Zpower_nat radix (pred q1) × v × radix)%Z with
(radix × Zpower_nat radix (pred q1) × v)%Z;
[ rewrite <- Zpower_nat_S | ring ].
apply Zmult_le_compat_r; auto with zarith.
Qed.
Theorem Zlt_Zpower_nat : ∀ n : nat, (n < Zpower_nat radix n)%Z.
intros n; induction n as [| n Hrecn].
simpl in |- *; auto with zarith.
rewrite Zpower_nat_S.
apply Zlt_le_trans with (1 + Zpower_nat radix n)%Z.
replace (Z_of_nat (S n)) with (1 + n)%Z; auto with arith zarith.
replace 1%Z with (Z_of_nat 1); auto with arith zarith.
rewrite <- inj_plus; auto with arith zarith.
apply Zle_trans with (Zpower_nat radix n + Zpower_nat radix n)%Z;
auto with zarith.
apply Zle_trans with (2 × Zpower_nat radix n)%Z; auto with zarith.
Qed.
Theorem FNIMore :
∀ N q : nat,
0 < q → q ≤ N → (N < radix × (Zpower_nat radix (FNI q N) × q))%Z.
intros N q; case q.
intros H; inversion H.
intros q' H H'; unfold FNI in |- ×.
apply
Zlt_le_trans with (Zpower_nat radix (FNIAux (S q') N (S (S N))) × S q')%Z.
apply FNIAuxMore; auto with arith zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
case (FNIAux (S q') N (S (S N))).
simpl in |- *; auto with arith.
intros n0 H2; replace (pred (S (S N))) with (S N); auto with arith.
rewrite <- H2.
apply Zpower_nat_anti_monotone_lt with radix; auto with arith zarith.
apply Zgt_lt; apply Zmult_gt_reg_r with (Z_of_nat (S q'));
auto with zarith arith; apply Zlt_gt.
apply Zlt_le_trans with (Z_of_nat 1); auto with zarith arith.
apply Zle_lt_trans with (radix × N)%Z.
apply FNIAuxLess; auto with zarith arith.
apply Zle_lt_trans with (radix × N × S q')%Z; auto with zarith arith.
pattern (radix × N)%Z at 1 in |- *;
replace (radix × N)%Z with (radix × N × 1%nat)%Z;
auto with arith zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
apply Zmult_gt_0_lt_compat_r; auto with zarith arith.
apply Zlt_gt; auto with arith zarith.
rewrite Zpower_nat_S; apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply Zlt_Zpower_nat.
rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith.
generalize (refl_equal (FNIAux (S q') N (S (S N))));
pattern (FNIAux (S q') N (S (S N))) at -1 in |- *;
case (FNIAux (S q') N (S (S N))).
intros H1; simpl in |- *; auto with zarith arith.
intros H1; rewrite <- Zpower_nat_S; auto with zarith arith.
Qed.
Definition FnormalizeI (b : FboundI) (p : float) :=
match (0 ?= Fnum p)%Z with
| Datatypes.Eq ⇒ Float 0 (- dExpI b)
| Datatypes.Lt ⇒
Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
(Zabs_nat (Fexp p + dExpI b))) p
| Datatypes.Gt ⇒
Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
(Zabs_nat (Fexp p + dExpI b))) p
end.
Theorem FnormalizeICorrect :
∀ (b : FboundI) (p : float), FnormalizeI b p = p :>R.
intros b p; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite <- H; simpl; ring.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
unfold FtoRradix in |- *; apply FshiftCorrect; auto.
Qed.
Theorem FnormalizeIBounded :
∀ (b : FboundI) (p : float),
FboundedI b p → FboundedI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
replace (Float 0 (- dExpI b)) with (Fzero (- dExpI b));
[ apply FboundedIFzero | unfold Fzero in |- *; auto ].
unfold Fshift in |- ×.
repeat split; simpl in |- ×.
apply Zle_trans with 0%Z; auto with zarith arith.
apply
Zle_trans
with (Fnum p × Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b)))%Z;
auto with zarith arith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (Zabs (Fnum p));
[ rewrite Zabs_absolu; rewrite Zmult_comm
| apply Zabs_eq; auto with zarith ].
apply FNILess; auto with arith zarith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith; elim H; intuition.
apply
Zplus_le_reg_l
with
(dExpI b +
min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
Zle_trans
with
(Z_of_nat
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b))
(Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
[ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
unfold Fshift in |- ×.
repeat split; simpl in |- ×.
2: apply Zle_trans with 0%Z; auto with zarith arith.
2: cut (∀ x y : Z, (x ≤ 0)%Z → (0 ≤ y)%Z → (x × y ≤ 0)%Z);
[ intros F; apply F | intros x y H3 H2 ]; auto with zarith.
2: rewrite <- (Zopp_involutive (x × y));
rewrite <- (Zopp_involutive 0).
2: apply Zle_Zopp; simpl in |- *; rewrite <- Zopp_mult_distr_l_reverse;
auto with zarith.
pattern (Fnum p) at 1 in |- *; replace (Fnum p) with (- Zabs_nat (Fnum p))%Z;
auto with zarith.
rewrite Zopp_mult_distr_l_reverse; apply Zle_Zopp.
apply
Zle_trans
with
(Zabs_nat (Fnum p) ×
Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b)))%Z.
apply Zle_Zmult_comp_l; auto with zarith arith.
rewrite Zmult_comm; apply FNILess.
rewrite <- absolu_Zopp; auto with zarith arith.
apply lt_Zlt_inv; rewrite <- Zabs_absolu; simpl in |- *; rewrite Zabs_eq;
auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe.
rewrite <- (Zopp_involutive (Z_of_nat (vNumInf b))).
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zle_Zopp; elim H; intuition.
rewrite <- absolu_Zopp; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith.
apply
Zplus_le_reg_l
with
(dExpI b +
min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))%Z.
apply
Zle_trans
with
(Z_of_nat
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b))
(Zabs_nat (Fexp p + dExpI b)))); [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (dExpI b + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
apply Zle_trans with (Z_of_nat (Zabs_nat (Fexp p + dExpI b)));
auto with zarith arith.
case (Zle_or_lt 0 (Fexp p + dExpI b)); intros H2.
rewrite inj_abs; auto with zarith arith.
rewrite <- absolu_Zopp; rewrite inj_abs; auto with zarith arith.
apply Zplus_le_reg_l with (- dExpI b + Fexp p)%Z.
apply Zle_trans with (- dExpI b + - dExpI b)%Z;
[ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p + Fexp p)%Z; [ idtac | apply Zeq_le; ring ].
repeat rewrite Zred_factor1.
apply Zle_Zmult_comp_r; auto with zarith arith; elim H; intuition.
Qed.
Theorem FcanonicIBoundedI :
∀ (b : FboundI) (p : float), FcanonicI b p → FboundedI b p.
intros b p H.
case H; intros H1; elim H1; auto.
Qed.
Theorem FnormalizeIFcanonicI :
∀ (b : FboundI) (p : float),
FboundedI b p → FcanonicI b (FnormalizeI b p).
intros b p H; unfold FnormalizeI in |- ×.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z; intros H1.
unfold FcanonicI in |- *; right.
repeat split; simpl in |- *; auto with zarith.
replace (radix × 0)%R with (IZR 0); auto with zarith real.
replace (radix × 0)%R with (INR 0); auto with zarith real arith.
case
(min_or (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)));
intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
(Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumSup b)) (Zabs_nat (Fexp p + dExpI b)))
p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; auto.
left; unfold Fshift in |- *; simpl in |- ×.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zabs_eq (Fnum p));
auto with zarith; rewrite Zabs_absolu.
rewrite <- Rmult_IZR; rewrite INR_IZR_INZ; apply Rlt_IZR.
rewrite
(Zmult_comm (Zabs_nat (Fnum p))
(Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumSup b))))
.
apply FNIMore.
apply lt_Zlt_inv; simpl in |- *; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith;
elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
[ intros H4 | auto with zarith ].
case
(Rle_or_lt
(radix × (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z)
(vNumSup b)); intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- ×.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
replace 0%R with (IZR 0); auto with real zarith.
rewrite Rmult_IZR; auto with real arith zarith.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real arith zarith.
apply Rmult_lt_0_compat; auto with real arith zarith.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H1; simpl in |- *; rewrite H2; auto.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
cut (0 < - Fnum p)%Z; [ intros Y | auto with zarith ].
case
(min_or (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)));
intros H2; elim H2; clear H2; intros H2 H3; rewrite H2.
unfold FcanonicI in |- *; left; split.
rewrite <- H2.
replace
(Fshift radix
(min (FNI (Zabs_nat (Fnum p)) (vNumInf b)) (Zabs_nat (Fexp p + dExpI b)))
p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- *; rewrite H2; auto with zarith.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H4; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H4; absurd (0 < Fnum p)%Z; auto with zarith.
right; unfold Fshift in |- *; simpl in |- ×.
pattern (Fnum p) at 1 in |- *; rewrite <- (Zopp_involutive (Fnum p));
rewrite <- (Zabs_eq (- Fnum p)); auto with zarith.
rewrite Zopp_mult_distr_l_reverse; rewrite <- Rmult_IZR;
rewrite Zmult_comm; rewrite Zopp_mult_distr_l_reverse.
apply Rlt_IZR; apply Zlt_Zopp.
rewrite Zabs_absolu; rewrite absolu_Zopp.
rewrite Zmult_comm;
rewrite
(Zmult_comm (Zabs_nat (Fnum p))
(Zpower_nat radix (FNI (Zabs_nat (Fnum p)) (vNumInf b))))
.
apply FNIMore; auto with zarith.
rewrite <- absolu_Zopp; apply lt_Zlt_inv; simpl in |- *;
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite <- absolu_Zopp; apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq;
auto with zarith; elim H; intuition.
cut (Zabs_nat (Fexp p + dExpI b) = (Fexp p + dExpI b)%Z :>Z);
[ intros H4 | auto with zarith ].
case
(Rle_or_lt (- vNumInf b)%Z
(radix × (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p + dExpI b)))%Z));
intros H5.
unfold FcanonicI in |- *; right; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- ×.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
split.
unfold Fshift in |- *; simpl in |- *; rewrite H4; ring.
unfold Fshift in |- *; simpl in |- ×.
split; auto.
apply Rle_trans with 0%R; auto with real arith zarith.
apply Ropp_le_cancel.
rewrite Rmult_comm; rewrite <- Ropp_mult_distr_l_reverse; rewrite Rmult_comm.
replace (-0)%R with 0%R; auto with real.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
rewrite <- Ropp_Ropp_IZR; rewrite Zmult_comm.
rewrite Zopp_mult_distr_r; rewrite Zmult_comm; auto with zarith real.
unfold FcanonicI in |- *; left; split.
replace (Fshift radix (Zabs_nat (Fexp p + dExpI b)) p) with (FnormalizeI b p).
apply FnormalizeIBounded; auto.
unfold FnormalizeI in |- ×.
replace (0 ?= Fnum p)%Z with Datatypes.Gt; auto with zarith.
rewrite H2; auto.
generalize (Zcompare_correct 0 (Fnum p)); case (0 ?= Fnum p)%Z;
auto with zarith.
intros H6; absurd (0%Z = Fnum p :>Z); auto with zarith.
intros H6; absurd (0 < Fnum p)%Z; auto with zarith.
unfold Fshift in |- *; simpl in |- *; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (- dExpI b)%Z.
apply Zle_trans with (- dExpI b)%Z; [ apply Zeq_le; ring | idtac ].
apply Zle_trans with (Fexp p); [ idtac | apply Zeq_le; ring ].
elim H; intuition.
Qed.
End FboundedI_Def.