Library Float.Others.IEEE
Require Export Bvector.
Require Export Zbinary.
Require Export AllFloat.
Section IEEEdefs.
Lemma Zpower_nat_is_pos :
forall (base : Z) (exp : nat),
(0 < base)%Z -> (0 < Zpower_nat base exp)%Z.
intros base exp; unfold Zpower_nat in |- *; induction exp as [| exp Hrecexp].
simpl in |- *; auto with zarith.
simpl in |- *; auto with zarith.
Qed.
Let radix := 2%Z.
Record IEEE_precision : Set := Precision {precision : nat; nbexp : nat}.
Variable p : IEEE_precision.
Hypothesis Prec_Greater_Than_One : 1 < precision p.
Hypothesis Exp_Pos : 1 < nbexp p.
Hint Resolve Prec_Greater_Than_One: arith.
Hint Resolve Exp_Pos: arith.
Hint Resolve Zpower_nat_is_pos: zarith.
Record IEEE_Float : Set := IEEE_construct
{Sign : bool;
IEEE_Frac : vector bool (pred (precision p));
IEEE_Exp : vector bool (nbexp p)}.
Let exp_max := Zpred (Zpower_nat radix (pred (nbexp p))).
Let biais1 := exp_max.
Let biais2 := Zpred (precision p).
Let mant_max := (Zpower_nat radix (pred (precision p)) - 1%Z)%R.
Let b :=
Bound
(P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (precision p)))))
(Npos (P_of_succ_nat (pred (Zabs_nat (Zpred (Zpred exp_max + precision p)))))).
Definition IEEE_normal (f : IEEE_Float) :=
binary_value (nbexp p) (IEEE_Exp f) <> 0%Z /\
binary_value (nbexp p) (IEEE_Exp f) <> Zpred (Zpower_nat radix (nbexp p)).
Definition IEEE_subnormal (f : IEEE_Float) :=
binary_value (nbexp p) (IEEE_Exp f) = 0%Z /\
binary_value (pred (precision p)) (IEEE_Frac f) <> 0%Z.
Definition IEEE_canonic (f : IEEE_Float) := IEEE_normal f \/ IEEE_subnormal f.
Definition IEEE_shift_mantissa (f : float) :=
Float (radix * Fnum f) (Zpred (Fexp f)).
Lemma vNum_eq_Zpower : Zpos (vNum b) = Zpower_nat radix (precision p).
unfold b in |- *; unfold vNum in |- *.
apply
trans_eq
with
(Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat (Zpower_nat radix (precision p))))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
cut (Zabs (Zpower_nat radix (precision p)) = Zpower_nat radix (precision p)).
intros H; pattern (Zpower_nat radix (precision p)) at 2 in |- *; rewrite <- H.
rewrite Zabs_absolu.
rewrite <- (S_pred (Zabs_nat (Zpower_nat radix (precision p))) 0);
auto with arith zarith.
apply lt_Zlt_inv; simpl in |- *; auto with zarith arith.
rewrite <- Zabs_absolu; rewrite H; auto with arith zarith.
apply Zabs_eq; auto with arith zarith.
Qed.
Theorem FtoR_Zpred_exp :
forall (r : Z) (f : float),
(1 < r)%Z -> FtoR r (Float (r * Fnum f) (Zpred (Fexp f))) = FtoR r f.
intros.
unfold FtoR; simpl.
unfold Zpred; rewrite powerRZ_add; auto with real zarith.
rewrite mult_IZR; simpl; field; auto with real zarith.
Qed.
Theorem FNorm_or_Subnorm :
forall f : float,
Fbounded b f ->
{Fnormal radix b (Fnormalize radix b (precision p) f)} +
{Fsubnormal radix b (Fnormalize radix b (precision p) f)}.
intros f H2.
cut (Fcanonic radix b (Fnormalize radix b (precision p) f));
[ intros H | idtac ].
generalize
(Z_le_gt_dec (Zpos (vNum b))
(Zabs (radix * Fnum (Fnormalize radix b (precision p) f)))).
intros H1.
case H1.
intros H3.
clear H1.
left.
auto.
split.
apply FnormalizeBounded; auto.
auto with zarith.
auto with arith.
apply vNum_eq_Zpower.
exact H3.
2: apply FnormalizeCanonic.
2: auto with arith zarith.
2: auto with arith zarith.
2: apply vNum_eq_Zpower.
2: exact H2.
right; auto.
split.
apply FnormalizeBounded; auto.
auto with arith zarith.
auto with arith.
apply vNum_eq_Zpower.
split.
2: cut
(Zpos (vNum b) >
Zabs (radix * Fnum (Fnormalize radix b (precision p) f)))%Z.
2: cut (forall a c : Z, (a > c)%Z -> (c < a)%Z).
2: intros H4.
2: apply H4.
2: apply Zgt_lt.
2: exact z.
clear H1.
case (Z_le_lt_eq_dec (- dExp b) (Fexp (Fnormalize radix b (precision p) f))).
cut (Fbounded b (Fnormalize radix b (precision p) f)).
unfold Fbounded in |- *.
intros ip.
elim ip.
intros.
exact H1; clear H1 H0 ip.
apply FnormalizeBounded.
auto with zarith.
auto with arith.
apply vNum_eq_Zpower.
exact H2.
2: intros.
2: apply sym_eq.
2: exact e.
intros.
absurd
(Fexp (Fnormalize radix b (precision p) f) <=
Fexp (IEEE_shift_mantissa (Fnormalize radix b (precision p) f)))%Z.
unfold IEEE_shift_mantissa in |- *.
simpl in |- *.
auto with zarith.
apply FcanonicLeastExp with radix b (precision p).
auto with zarith.
auto with arith.
apply vNum_eq_Zpower.
2: unfold Fbounded in |- *.
2: split.
2: unfold IEEE_shift_mantissa in |- *.
2: apply Zgt_lt.
2: auto with arith.
2: unfold IEEE_shift_mantissa in |- *.
2: apply Zlt_succ_le.
2: simpl in |- *.
2: auto with zarith.
2: exact H.
unfold IEEE_shift_mantissa in |- *.
apply FtoR_Zpred_exp.
auto with zarith.
Qed.
Theorem Expo_zero_or_pos :
forall f : IEEE_Float,
{binary_value (nbexp p) (IEEE_Exp f) = 0%Z} +
{(0 < binary_value (nbexp p) (IEEE_Exp f))%Z}.
intros g.
cut
({(binary_value (nbexp p) (IEEE_Exp g) <= 0)%Z}
+ {(binary_value (nbexp p) (IEEE_Exp g) > 0)%Z}); [ idtac | apply Z_le_gt_dec ].
intros H; elim H; intros H'.
left.
cut (0 <= binary_value (nbexp p) (IEEE_Exp g))%Z; auto with zarith.
apply Zge_le; apply binary_value_pos.
right; auto with zarith.
Qed.
Definition IEEE_subnormalToR (x : IEEE_Float) :=
match Sign x with
| false =>
(binary_value (pred (precision p)) (IEEE_Frac x) *
powerRZ radix (Zsucc (- (biais1 + biais2))))%R
| true =>
((- binary_value (pred (precision p)) (IEEE_Frac x))%Z *
powerRZ radix (Zsucc (- (biais1 + biais2))))%R
end.
Definition IEEE_normalToR (x : IEEE_Float) :=
match Sign x with
| false =>
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))%Z *
powerRZ radix
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)))%R
| true =>
(-
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))%Z *
powerRZ radix
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))))%R
end.
Definition IEEE_To_R (x : IEEE_Float) :=
match Expo_zero_or_pos x with
| left _ => IEEE_subnormalToR x
| right _ => IEEE_normalToR x
end.
Definition InDomain (f : float) :=
(Fexp (Fnormalize radix b (precision p) f) + biais2 <= exp_max)%Z /\
Fbounded b f.
Definition FNormTo_IEEE (f : float) :=
match Z_lt_ge_dec (Fnum f) 0 with
| left _ =>
IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))
| right _ =>
IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))
end.
Definition FSubnormTo_IEEE (f : float) :=
match Z_lt_ge_dec (Fnum f) 0 with
| left _ =>
IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0)
| right _ =>
IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0)
end.
Definition Float_To_IEEE (f : float) H :=
match FNorm_or_Subnorm f H with
| left _ => FNormTo_IEEE f
| right _ => FSubnormTo_IEEE f
end.
Theorem float_equals_IEEE :
forall (f : float) (H : Fbounded b f),
InDomain f -> FtoR radix f = IEEE_To_R (Float_To_IEEE f H).
assert (Y:(0 < (Zpred (Zpred exp_max + precision p)))%Z).
assert (2 < exp_max+precision p)%Z; unfold Zpred; auto with zarith.
assert (1 < precision p)%Z; auto with zarith.
assert (1 <= exp_max)%Z; auto with zarith.
unfold exp_max; apply Zle_trans with (Zpred (Zpower_nat radix (pred (2)))).
simpl; auto with zarith.
unfold Zpred; auto with zarith.
intros f H.
unfold InDomain in |- *.
intros z.
elim z.
clear z.
intros z H1.
clear H1.
cut (0 < biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2)%Z;
[ intros V1 | idtac ].
2: apply Zplus_lt_reg_l with (- (biais1 + biais2))%Z.
2: ring_simplify.
2: apply Zlt_le_trans with (- dExp b)%Z; auto with zarith float.
2: apply Zle_lt_trans with (-(biais1+biais2))%Z; auto with zarith.
2: apply Zlt_Zopp; unfold b, biais2 in |- *; simpl in |- *.
2: replace (Zpos
(P_of_succ_nat (pred (Zabs_nat (Zpred (Zpred exp_max + precision p)))))) with
(Zpred (Zpred exp_max + precision p)); auto with zarith.
2: unfold biais1, Zpred; auto with zarith.
2: apply trans_eq with
(Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat ((Zpred (Zpred exp_max + precision p)))))))).
2:rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
2: rewrite <- (S_pred (Zabs_nat (Zpred (Zpred exp_max + precision p))) 0); auto with zarith.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: cut (0 < Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z; auto with zarith.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
2: cut (Fbounded b (Fnormalize radix b (precision p) f));
auto with float zarith.
2: apply FnormalizeBounded; auto with float zarith arith.
2: apply vNum_eq_Zpower.
cut
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2 <
two_power_nat (nbexp p))%Z; [ intros V2 | idtac ].
2: apply Zle_lt_trans with (exp_max + exp_max)%Z; auto with zarith.
2: pattern exp_max at 1 in |- *; replace exp_max with biais1;
auto with zarith.
2: rewrite two_power_nat_correct.
2: replace (exp_max + exp_max)%Z with (2 * exp_max)%Z; auto with zarith.
2: unfold exp_max in |- *.
2: apply Zlt_le_trans with (2 * Zpower_nat radix (pred (nbexp p)))%Z;
auto with zarith.
2: apply Zmult_gt_0_lt_compat_l; auto with zarith.
2: pattern (nbexp p) at 2 in |- *;
replace (nbexp p) with (S (pred (nbexp p))); auto with zarith arith.
unfold IEEE_To_R in |- *.
case (Expo_zero_or_pos (Float_To_IEEE f H)).
unfold IEEE_subnormalToR in |- *.
unfold Float_To_IEEE in |- *.
case (FNorm_or_Subnorm f H).
intros H1 H2.
absurd (binary_value (nbexp p) (IEEE_Exp (FNormTo_IEEE f)) = 0%Z); auto.
unfold FNormTo_IEEE in |- *.
cut
(binary_value (nbexp p)
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) + biais2)) <> 0%Z);
[ intros V | idtac ].
case (Z_lt_ge_dec (Fnum f) 0); intros H3.
simpl
(IEEE_Exp
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) +
radix ^ pred (precision p)))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))))
in |- *.
unfold biais1 in |- *; auto.
simpl
(IEEE_Exp
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) + biais2))))
in |- *.
auto.
rewrite Z_to_binary_to_Z; auto with zarith.
replace exp_max with biais1; auto with zarith.
intros H1 H2.
unfold FSubnormTo_IEEE in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H3.
simpl
(Sign
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
simpl
(IEEE_Frac
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
apply
trans_eq
with
((-
binary_value (pred (precision p))
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f))))%Z *
powerRZ radix (Zsucc (- (biais1 + biais2))))%R;
auto.
rewrite Z_to_binary_to_Z; auto with zarith.
rewrite Zopp_involutive.
replace (Zsucc (- (biais1 + biais2))) with
(Fexp (Fnormalize radix b (precision p) f)).
apply trans_eq with (FtoR radix (Fnormalize radix b (precision p) f));
auto with float zarith.
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
elim H1; intros H4 H5; elim H5; intros H6 H7; clear H5; rewrite H6.
unfold b, biais1, biais2 in |- *.
apply trans_eq with (- Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z;
auto.
simpl.
apply
trans_eq
with
(-(Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat (Zpred (Zpred exp_max+precision p))))))))%Z.
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- (S_pred (Zabs_nat ((Zpred (Zpred exp_max+precision p)))) 0);
auto with zarith.
cut (0 < Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
unfold Zpred, Zsucc in |- *; ring.
apply Zle_ge; apply Zle_Zopp_Inv; rewrite Zopp_involutive.
replace (- (0))%Z with
(Fnum (Float 0 (Fexp (Fnormalize radix b (precision p) f))));
[ idtac | simpl in |- *; ring ].
apply Rle_Fexp_eq_Zle with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
unfold FtoR in |- *; simpl in |- *.
ring_simplify (0 * powerRZ 2 (Fexp (Fnormalize radix b (precision p) f)))%R;
auto with zarith real.
apply Rle_trans with (0%Z * powerRZ 2 (Fexp f))%R; auto with real zarith.
rewrite two_power_nat_correct.
elim H1; intros H4 H5; elim H5; intros H6 H7; clear H5.
apply Zmult_gt_0_lt_reg_r with radix; auto with zarith.
apply Zlt_gt; unfold radix in |- *; auto with zarith.
replace (- Fnum (Fnormalize radix b (precision p) f) * radix)%Z with
(- (radix * Fnum (Fnormalize radix b (precision p) f)))%Z;
[ idtac | ring ].
apply
Zle_lt_trans
with (Zabs (- (radix * Fnum (Fnormalize radix b (precision p) f))));
[ apply Zle_Zabs | idtac ].
rewrite Zabs_Zopp; apply Zlt_le_trans with (1 := H7).
apply Zeq_le; rewrite vNum_eq_Zpower.
unfold radix in |- *; pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
auto with zarith arith.
rewrite Zpower_nat_is_exp; auto with zarith arith.
simpl
(Sign
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
simpl
(IEEE_Frac
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
apply
trans_eq
with
(binary_value (pred (precision p))
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f))) *
powerRZ radix (Zsucc (- (biais1 + biais2))))%R;
auto.
rewrite Z_to_binary_to_Z; auto with zarith.
replace (Zsucc (- (biais1 + biais2))) with
(Fexp (Fnormalize radix b (precision p) f)).
apply trans_eq with (FtoR radix (Fnormalize radix b (precision p) f));
auto with float zarith.
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
elim H1; intros H4 H5; elim H5; intros H6 H7; clear H5; rewrite H6.
unfold b, biais1, biais2 in |- *.
apply trans_eq with (- Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z;
auto.
simpl.
apply
trans_eq
with
(-(Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat (Zpred (Zpred exp_max+precision p))))))))%Z.
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- (S_pred (Zabs_nat ((Zpred (Zpred exp_max+precision p)))) 0);
auto with zarith.
cut (0 < Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
unfold Zpred, Zsucc in |- *; ring.
apply Zle_ge.
replace 0%Z with (Fnum (Float 0 (Fexp (Fnormalize radix b (precision p) f))));
[ idtac | simpl in |- *; ring ].
apply Rle_Fexp_eq_Zle with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
unfold FtoR in |- *; simpl in |- *.
ring_simplify (0 * powerRZ 2 (Fexp (Fnormalize radix b (precision p) f)))%R;
auto with zarith real.
apply Rle_trans with (0%Z * powerRZ 2 (Fexp f))%R; auto with real zarith.
rewrite two_power_nat_correct.
elim H1; intros H4 H5; elim H5; intros H6 H7; clear H5.
apply Zmult_gt_0_lt_reg_r with radix; auto with zarith.
apply Zlt_gt; unfold radix in |- *; auto with zarith.
rewrite Zmult_comm.
apply
Zle_lt_trans with (Zabs (radix * Fnum (Fnormalize radix b (precision p) f)));
[ apply Zle_Zabs | idtac ].
apply Zlt_le_trans with (1 := H7).
apply Zeq_le; rewrite vNum_eq_Zpower.
unfold radix in |- *; pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
auto with zarith arith.
rewrite Zpower_nat_is_exp; auto with zarith arith.
unfold IEEE_normalToR in |- *.
unfold Float_To_IEEE in |- *.
case (FNorm_or_Subnorm f H).
2: intros H1 H2.
2: absurd (0 < binary_value (nbexp p) (IEEE_Exp (FSubnormTo_IEEE f)))%Z;
auto with zarith.
2: unfold FSubnormTo_IEEE in |- *.
2: case (Z_lt_ge_dec (Fnum f) 0).
2: simpl
(IEEE_Exp
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
2: rewrite Z_to_binary_to_Z; auto with zarith.
2: simpl
(IEEE_Exp
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) in |- *.
2: rewrite Z_to_binary_to_Z; auto with zarith.
intros H1 H2.
unfold FNormTo_IEEE in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H3.
simpl
(Sign
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))))
in |- *.
apply
trans_eq
with
(-
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p))
(IEEE_Frac
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) +
biais2)))))%Z *
powerRZ radix
(binary_value (nbexp p)
(IEEE_Exp
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) +
biais2)))) - (biais1 + biais2))))%R;
auto.
apply
trans_eq
with
(-
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p))
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)))))%Z *
powerRZ radix
(binary_value (nbexp p)
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2)) -
(biais1 + biais2))))%R; auto.
rewrite Z_to_binary_to_Z; auto with zarith.
rewrite Z_to_binary_to_Z; auto with zarith.
2: unfold biais1 in |- *; auto with zarith.
ring_simplify
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2 -
(biais1 + biais2))%Z.
apply
trans_eq
with
((- - Fnum (Fnormalize radix b (precision p) f))%Z *
powerRZ radix (Fexp (Fnormalize radix b (precision p) f)))%R;
[ rewrite Zopp_involutive | idtac ].
apply trans_eq with (FtoR radix (Fnormalize radix b (precision p) f));
auto with float zarith.
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
ring_simplify
(Zpower_nat radix (pred (precision p)) +
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))%Z.
repeat rewrite Ropp_Ropp_IZR; ring.
apply Zle_ge;
apply Zplus_le_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify.
elim H1; intros G1 H4; clear G1.
apply Zmult_le_reg_r with radix; auto with zarith.
unfold radix in |- *; auto with zarith.
replace (Zpower_nat radix (pred (precision p)) * radix)%Z with
(Zpos (vNum b)).
replace (- Fnum (Fnormalize radix b (precision p) f) * radix)%Z with
(Zabs (radix * Fnum (Fnormalize radix b (precision p) f)));
auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith; [ ring | idtac ].
rewrite Zmult_comm; rewrite <- Zopp_mult_distr_l_reverse;
auto with zarith.
replace 0%Z with (0 * radix)%Z; auto with zarith.
apply Zmult_le_compat_r; auto with zarith.
replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp.
replace 0%Z with (Fnum (Float 0 (Fexp (Fnormalize radix b (precision p) f))));
[ idtac | simpl in |- *; ring ].
apply Rle_Fexp_eq_Zle with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
unfold FtoR in |- *; simpl in |- *.
ring_simplify (0 * powerRZ 2 (Fexp (Fnormalize radix b (precision p) f)))%R;
auto with zarith real.
apply Rle_trans with (0%Z * powerRZ 2 (Fexp f))%R; auto with real zarith.
rewrite vNum_eq_Zpower.
pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
[ rewrite Zpower_nat_is_exp | idtac ]; auto with zarith.
apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z.
apply
Zle_lt_trans with (Zabs (-1 * Fnum (Fnormalize radix b (precision p) f)));
[ apply Zle_Zabs | idtac ].
rewrite <- Zabs_Zopp.
ring_simplify (- (-1 * Fnum (Fnormalize radix b (precision p) f)))%Z.
apply Zlt_le_trans with (Zpos (vNum b)); auto with float zarith.
elim H1; auto with float zarith.
rewrite vNum_eq_Zpower.
rewrite two_power_nat_correct.
pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
[ rewrite Zpower_nat_is_exp | idtac ]; auto with zarith.
replace (Zpower_nat radix 1) with radix; auto with zarith.
unfold radix in |- *; apply Zeq_le; ring.
simpl
(Sign
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) + biais2))))
in |- *.
apply
trans_eq
with
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p))
(IEEE_Frac
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) +
biais2)))))%Z *
powerRZ radix
(binary_value (nbexp p)
(IEEE_Exp
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) +
biais2)))) - (biais1 + biais2)))%R;
auto.
apply
trans_eq
with
((Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p))
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)))))%Z *
powerRZ radix
(binary_value (nbexp p)
(Z_to_binary (nbexp p)
(exp_max + Fexp (Fnormalize radix b (precision p) f) + biais2)) -
(biais1 + biais2)))%R; auto; unfold biais1 in |- *.
rewrite Z_to_binary_to_Z; auto with zarith.
rewrite Z_to_binary_to_Z; auto with zarith.
ring_simplify
(exp_max + Fexp (Fnormalize radix b (precision p) f) + biais2 -
(exp_max + biais2))%Z.
ring_simplify
(Zpower_nat radix (pred (precision p)) +
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))%Z.
apply trans_eq with (FtoR radix (Fnormalize radix b (precision p) f));
auto with float zarith.
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
replace exp_max with biais1; auto with zarith.
apply Zle_ge;
apply Zplus_le_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify (0 + Zpower_nat radix (pred (precision p)))%Z;
ring_simplify
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z.
elim H1; intros G1 H4; clear G1.
apply Zmult_le_reg_r with radix; auto with zarith.
unfold radix in |- *; auto with zarith.
replace (Zpower_nat radix (pred (precision p)) * radix)%Z with
(Zpos (vNum b)).
replace (Fnum (Fnormalize radix b (precision p) f) * radix)%Z with
(Zabs (radix * Fnum (Fnormalize radix b (precision p) f)));
auto.
rewrite Zabs_eq; auto with zarith.
replace 0%Z with (radix * 0)%Z; auto with zarith.
apply Zmult_le_compat_l; auto with zarith.
replace 0%Z with (Fnum (Float 0 (Fexp (Fnormalize radix b (precision p) f))));
[ idtac | simpl in |- *; ring ].
apply Rle_Fexp_eq_Zle with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
unfold FtoR in |- *; simpl in |- *.
ring_simplify (0 * powerRZ 2 (Fexp (Fnormalize radix b (precision p) f)))%R;
auto with zarith real.
apply Rle_trans with (0%Z * powerRZ 2 (Fexp f))%R; auto with real zarith.
rewrite vNum_eq_Zpower.
pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
[ rewrite Zpower_nat_is_exp | idtac ]; auto with zarith.
apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z.
apply Zle_lt_trans with (Zabs (Fnum (Fnormalize radix b (precision p) f)));
[ apply Zle_Zabs | idtac ].
apply Zlt_le_trans with (Zpos (vNum b)); auto with float zarith.
elim H1; auto with float zarith.
rewrite vNum_eq_Zpower.
rewrite two_power_nat_correct.
pattern (precision p) at 1 in |- *;
replace (precision p) with (pred (precision p) + 1);
[ rewrite Zpower_nat_is_exp | idtac ]; auto with zarith.
replace (Zpower_nat radix 1) with radix; auto with zarith.
unfold radix in |- *; apply Zeq_le; ring.
Qed.
Theorem Float_To_IEEE_fn :
forall (f g : float) (Ff : Fbounded b f) (Fg : Fbounded b g),
FtoR radix f = FtoR radix g -> Float_To_IEEE f Ff = Float_To_IEEE g Fg.
generalize vNum_eq_Zpower; intros V.
intros f g Ff Fg H; unfold Float_To_IEEE in |- *.
case (FNorm_or_Subnorm f Ff); case (FNorm_or_Subnorm g Fg).
intros H1 H2; unfold FNormTo_IEEE in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H3.
case (Z_lt_ge_dec (Fnum g) 0); intros H4.
replace (Fnormalize radix b (precision p) f) with
(Fnormalize radix b (precision p) g); auto with real zarith arith.
apply FcanonicUnique with radix b (precision p); auto with float zarith arith.
repeat rewrite FnormalizeCorrect; auto with zarith.
absurd (FtoR radix f < FtoR radix g)%R; auto with real.
rewrite H; auto with real.
unfold FtoR in |- *; simpl in |- *; apply Rlt_le_trans with (0%Z * 0)%R;
auto with real zarith.
apply Rlt_le_trans with (0%Z * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
case (Z_lt_ge_dec (Fnum g) 0); intros H4.
absurd (FtoR radix g < FtoR radix f)%R; auto with real.
rewrite H; auto with real.
unfold FtoR in |- *; simpl in |- *; apply Rlt_le_trans with (0%Z * 0)%R;
auto with real zarith.
apply Rlt_le_trans with (0%Z * powerRZ 2%Z (Fexp g))%R; auto with real zarith.
replace (Fnormalize radix b (precision p) f) with
(Fnormalize radix b (precision p) g); auto with real zarith arith.
apply FcanonicUnique with radix b (precision p); auto with float zarith arith.
repeat rewrite FnormalizeCorrect; auto with zarith.
intros H1 H2; Contradict H.
rewrite <- FnormalizeCorrect with radix b (precision p) f; auto with zarith.
rewrite <- FnormalizeCorrect with radix b (precision p) g; auto with zarith.
apply NormalAndSubNormalNotEq with b (precision p);
auto with arith zarith real.
intros H1 H2; Contradict H.
rewrite <- FnormalizeCorrect with radix b (precision p) f; auto with zarith.
rewrite <- FnormalizeCorrect with radix b (precision p) g; auto with zarith.
apply not_eq_sym; apply NormalAndSubNormalNotEq with b (precision p);
auto with arith zarith real.
intros H1 H2; unfold FSubnormTo_IEEE in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H3.
case (Z_lt_ge_dec (Fnum g) 0); intros H4.
replace (Fnormalize radix b (precision p) f) with
(Fnormalize radix b (precision p) g); auto with real zarith arith.
apply FcanonicUnique with radix b (precision p); auto with float zarith arith.
repeat rewrite FnormalizeCorrect; auto with zarith.
absurd (FtoR radix f < FtoR radix g)%R; auto with real.
rewrite H; auto with real.
unfold FtoR in |- *; simpl in |- *; apply Rlt_le_trans with (0%Z * 0)%R;
auto with real zarith.
apply Rlt_le_trans with (0%Z * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
case (Z_lt_ge_dec (Fnum g) 0); intros H4.
absurd (FtoR radix g < FtoR radix f)%R; auto with real.
rewrite H; auto with real.
unfold FtoR in |- *; simpl in |- *; apply Rlt_le_trans with (0%Z * 0)%R;
auto with real zarith.
apply Rlt_le_trans with (0%Z * powerRZ 2%Z (Fexp g))%R; auto with real zarith.
replace (Fnormalize radix b (precision p) f) with
(Fnormalize radix b (precision p) g); auto with real zarith arith.
apply FcanonicUnique with radix b (precision p); auto with float zarith arith.
repeat rewrite FnormalizeCorrect; auto with zarith.
Qed.
Definition IEEE_Pos_To_Float (x : IEEE_Float) :=
match Expo_zero_or_pos x with
| left _ =>
Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)
| right _ =>
Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))
end.
Definition IEEE_To_Float (x : IEEE_Float) :=
match Sign x with
| false => IEEE_Pos_To_Float x
| true => Fopp (IEEE_Pos_To_Float x)
end.
Theorem binary_value_Zle :
forall (n : nat) (B : Bvector n),
(binary_value n B <= Zpred (two_power_nat n))%Z.
simple induction B; [ simpl in |- *; auto with zarith | idtac ].
intros a m v H.
rewrite binary_value_Sn.
apply Zle_trans with (bit_value a + 2 * Zpred (two_power_nat m))%Z;
auto with zarith.
unfold Zpred in |- *; rewrite two_power_nat_S; case a.
replace (bit_value true) with 1%Z; auto with zarith.
replace (bit_value false) with 0%Z; auto with zarith.
Qed.
Theorem IEEE_To_Float_Bounded :
forall x : IEEE_Float, Fbounded b (IEEE_To_Float x).
intros x.
cut (forall y : IEEE_Float, Fbounded b (IEEE_Pos_To_Float y));
[ intros V | idtac ].
unfold IEEE_To_Float in |- *; case (Sign x); auto.
apply oppBounded; auto.
intros y; unfold IEEE_Pos_To_Float in |- *.
case (Expo_zero_or_pos y); intros H1.
split; auto with zarith.
replace
(Zabs
(Fnum
(Float (binary_value (pred (precision p)) (IEEE_Frac y)) (- dExp b))))
with (Zabs (binary_value (pred (precision p)) (IEEE_Frac y)));
auto.
rewrite Zabs_eq; [ idtac | apply Zge_le; apply binary_value_pos ].
apply Zle_lt_trans with (Zpred (two_power_nat (pred (precision p))));
[ apply binary_value_Zle | idtac ].
rewrite vNum_eq_Zpower; rewrite two_power_nat_correct; auto with zarith arith.
split; auto with zarith.
replace
(Zabs
(Fnum
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac y))
(binary_value (nbexp p) (IEEE_Exp y) - (biais1 + biais2))))) with
(Zabs
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac y)));
auto.
rewrite Zabs_eq; auto with zarith.
rewrite vNum_eq_Zpower;
apply
Zlt_le_trans
with
(Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z; auto with zarith.
apply Zplus_lt_compat_l.
apply Zle_lt_trans with (Zpred (two_power_nat (pred (precision p))));
[ apply binary_value_Zle | idtac ].
rewrite two_power_nat_correct; auto with zarith.
pattern (precision p) at 3 in |- *;
replace (precision p) with (S (pred (precision p)));
auto with zarith arith.
repeat rewrite <- two_power_nat_correct; rewrite two_power_nat_S;
auto with zarith arith.
apply Zle_trans with (0 + 0)%Z; auto with zarith.
apply Zplus_le_compat; auto with zarith.
apply Zge_le; apply binary_value_pos.
replace
(Fexp
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac y))
(binary_value (nbexp p) (IEEE_Exp y) - (biais1 + biais2)))) with
(binary_value (nbexp p) (IEEE_Exp y) - (biais1 + biais2))%Z;
auto.
replace (- dExp b)%Z with (Zsucc 0 + - Zsucc (dExp b))%Z;
[ unfold Zminus in |- *; apply Zplus_le_compat; auto with zarith
| unfold Zsucc, Zpred in |- *; ring ].
apply Zle_Zopp; unfold b ; simpl.
unfold biais1, biais2.
apply Zeq_le.
apply trans_eq with ((Zpos (P_of_succ_nat (pred
(Zabs_nat (Zpred (Zpred exp_max + precision p))))))+1)%Z; auto with zarith.
replace (Zpos
(P_of_succ_nat (pred (Zabs_nat (Zpred (Zpred exp_max + precision p))))))
with (Zpred (Zpred exp_max + precision p)).
unfold Zpred; ring.
assert (Y:(0 < (Zpred (Zpred exp_max + precision p)))%Z).
assert (2 < exp_max+precision p)%Z; unfold Zpred; auto with zarith.
assert (1 < precision p)%Z; auto with zarith.
assert (1 <= exp_max)%Z; auto with zarith.
unfold exp_max; apply Zle_trans with (Zpred (Zpower_nat radix (pred (2)))).
simpl; auto with zarith.
unfold Zpred; auto with zarith.
apply
trans_eq
with
((Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat (Zpred (Zpred exp_max+precision p))))))))%Z.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- (S_pred (Zabs_nat ((Zpred (Zpred exp_max+precision p)))) 0);
auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
cut (0 < Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith arith.
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
Qed.
Theorem IEEE_To_Float_To_IEEE :
forall x : IEEE_Float,
x <>
IEEE_construct true (Z_to_binary (pred (precision p)) 0)
(Z_to_binary (nbexp p) 0) ->
Float_To_IEEE (IEEE_To_Float x) (IEEE_To_Float_Bounded x) = x.
intros x N.
generalize vNum_eq_Zpower; intros V.
generalize (IEEE_To_Float_Bounded x); unfold IEEE_To_Float in |- *.
case (sumbool_of_bool (Sign x)); intros H1; rewrite H1.
unfold IEEE_Pos_To_Float in |- *; case (Expo_zero_or_pos x).
unfold Fopp in |- *.
replace
(Float
(-
Fnum
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))
(Fexp
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b))))
with (Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b));
[ idtac | simpl in |- *; auto ].
intros H2 H3.
unfold Float_To_IEEE in |- *.
cut
(Fsubnormal radix b
(Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)));
[ intros H6 | idtac ].
case
(FNorm_or_Subnorm
(Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)) H3);
intros H4.
generalize
(NormalNotSubNormal radix b
(Fnormalize radix b (precision p)
(Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b))));
intros H5.
Contradict H5; split; auto.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
right; auto.
unfold FSubnormTo_IEEE in |- *.
case
(Z_lt_ge_dec
(Fnum
(Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))
0); intros H5.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
2: right; auto.
rewrite <- H1.
replace
(-
Fnum (Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))%Z
with (- - binary_value (pred (precision p)) (IEEE_Frac x))%Z;
auto.
ring_simplify (- - binary_value (pred (precision p)) (IEEE_Frac x))%Z;
rewrite binary_to_Z_to_binary.
rewrite <- H2; rewrite binary_to_Z_to_binary; elim x; auto.
cut
(0 <=
Fnum (Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))%Z;
auto with zarith; intros H7.
absurd ((0 <= Fnum
(Float (- binary_value (pred (precision p))
(IEEE_Frac x)) (- dExp b)))%Z); trivial.
apply Zgt_not_le; apply Zlt_gt; simpl in |- *.
cut (0 <= binary_value (pred (precision p)) (IEEE_Frac x))%Z;
[ intros T1 | apply Zge_le; apply binary_value_pos ].
cut (binary_value (pred (precision p)) (IEEE_Frac x) <> 0%Z);
auto with zarith.
Contradict N.
rewrite <- H1; pattern 0%Z at 1 in |- *; rewrite <- N; rewrite <- H2.
rewrite binary_to_Z_to_binary; rewrite binary_to_Z_to_binary; elim x; auto.
split; auto with zarith.
split; auto with zarith.
apply
Zle_lt_trans
with (Zabs (radix * - binary_value (pred (precision p)) (IEEE_Frac x)));
[ simpl in |- *; auto with zarith | idtac ].
rewrite <- Zabs_Zopp.
replace (- (radix * - binary_value (pred (precision p)) (IEEE_Frac x)))%Z
with (radix*binary_value (pred (precision p)) (IEEE_Frac x))%Z by ring.
rewrite Zabs_eq; auto with zarith.
rewrite V; rewrite <- two_power_nat_correct.
unfold radix in |- *; pattern (precision p) at 2 in |- *;
replace (precision p) with (S (pred (precision p)));
[ idtac | auto with arith zarith ].
rewrite two_power_nat_S; rewrite Zmult_comm.
rewrite Zmult_comm; apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply Zle_lt_trans with (Zpred (two_power_nat (pred (precision p))));
[ apply binary_value_Zle | auto with zarith ].
apply Zle_trans with (radix*0)%Z; auto with zarith; apply Zmult_le_compat_l;
auto with zarith.
apply Zge_le; apply binary_value_pos.
unfold Fopp in |- *.
replace
(Float
(-
Fnum
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))))
(Fexp
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))))) with
(Float
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)));
auto.
intros H2 H3.
unfold Float_To_IEEE in |- *.
cut
(Fnormal radix b
(Float
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))));
[ intros H6 | idtac ].
case
(FNorm_or_Subnorm
(Float
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))) H3);
intros H4.
unfold FNormTo_IEEE in |- *.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
2: left; auto.
simpl in |- *; clear H4.
ring_simplify
(biais1 + (binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)) +
biais2)%Z.
case
(Z_lt_ge_dec
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))) 0);
intros H4.
rewrite <- H1.
ring_simplify
(-
-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)) -
Zpower_nat radix (pred (precision p)))%Z.
rewrite binary_to_Z_to_binary.
rewrite binary_to_Z_to_binary; elim x; auto.
cut
(0 <=
-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))%Z;
auto with zarith; intros H5.
absurd ((0 <=
-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))%Z); trivial.
apply Zgt_not_le; apply Zlt_gt.
apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)) +
Zpower_nat radix (pred (precision p)))%Z.
ring_simplify (0 + Zpower_nat radix (pred (precision p)))%Z.
apply Zle_lt_trans with 0%Z; auto with zarith.
cut (binary_value (pred (precision p)) (IEEE_Frac x) >= 0)%Z;
[ auto with zarith | apply binary_value_pos ].
generalize
(NormalNotSubNormal radix b
(Fnormalize radix b (precision p)
(Float
(-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)))));
intros H5.
Contradict H5; split; auto.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
left; auto.
split; auto with zarith.
rewrite V.
apply
Zle_trans
with
(Zabs
(radix *
-
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))));
auto with zarith.
rewrite <- Zabs_Zopp.
replace (- (radix * -
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))))%Z with
(radix*binary_value (pred (precision p)) (IEEE_Frac x)
+radix*Zpower_nat radix (pred (precision p)))%Z by ring.
rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (0+Zpower_nat radix (precision p))%Z; auto with zarith;
apply Zplus_le_compat.
apply Zle_trans with (radix*0)%Z; auto with zarith; apply Zmult_le_compat_l;
auto with zarith.
apply Zge_le; apply binary_value_pos.
repeat rewrite <- two_power_nat_correct.
unfold radix in |- *; pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p)));
[ idtac | auto with arith zarith ].
rewrite two_power_nat_S; auto with zarith.
apply Zle_trans with (radix*0 + radix*0)%Z; auto with zarith.
apply Zplus_le_compat; apply Zmult_le_compat_l; auto with zarith.
apply Zge_le; apply binary_value_pos.
unfold IEEE_Pos_To_Float in |- *; case (Expo_zero_or_pos x).
intros H2 H3.
unfold Float_To_IEEE in |- *.
cut
(Fsubnormal radix b
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)));
[ intros H6 | idtac ].
case
(FNorm_or_Subnorm
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)) H3);
intros H4.
generalize
(NormalNotSubNormal radix b
(Fnormalize radix b (precision p)
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b))));
intros H5.
Contradict H5; split; auto.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
right; auto.
unfold FSubnormTo_IEEE in |- *.
case
(Z_lt_ge_dec
(Fnum
(Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))
0); intros H5.
cut
(0 >
Fnum (Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))%Z;
auto with zarith; intros H7.
Contradict H7; apply Zle_not_gt; simpl in |- *; apply Zge_le;
apply binary_value_pos.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
2: right; auto.
rewrite <- H1.
replace
(Fnum (Float (binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))
with (binary_value (pred (precision p)) (IEEE_Frac x));
auto.
rewrite binary_to_Z_to_binary.
rewrite <- H2; rewrite binary_to_Z_to_binary; elim x; auto.
split; auto with zarith.
split; auto with zarith.
apply
Zle_lt_trans
with (Zabs (radix * binary_value (pred (precision p)) (IEEE_Frac x)));
[ simpl in |- *; auto with zarith | idtac ].
rewrite Zabs_eq; auto with zarith.
rewrite V; rewrite <- two_power_nat_correct.
unfold radix in |- *; pattern (precision p) at 2 in |- *;
replace (precision p) with (S (pred (precision p)));
[ idtac | auto with arith zarith ].
rewrite two_power_nat_S.
apply Zmult_gt_0_lt_compat_l; auto with zarith.
apply Zle_lt_trans with (Zpred (two_power_nat (pred (precision p))));
[ apply binary_value_Zle | auto with zarith ].
apply Zle_trans with (radix * 0)%Z; auto with zarith; apply Zmult_le_compat_l;
auto with zarith.
apply Zge_le; apply binary_value_pos.
intros H2 H3.
unfold Float_To_IEEE in |- *.
cut
(Fnormal radix b
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))));
[ intros H6 | idtac ].
case
(FNorm_or_Subnorm
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2))) H3);
intros H4.
unfold FNormTo_IEEE in |- *.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
2: left; auto.
simpl in |- *; clear H4.
ring_simplify
(biais1 + (binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)) +
biais2)%Z.
case
(Z_lt_ge_dec
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)) 0);
intros H4.
cut
(0 >
Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))%Z;
auto with zarith; intros H5; Contradict H5.
apply Zle_not_gt; apply Zle_trans with (0 + 0)%Z; auto with zarith;
apply Zplus_le_compat; auto with zarith.
apply Zge_le; apply binary_value_pos.
rewrite <- H1.
ring_simplify
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x) -
Zpower_nat radix (pred (precision p)))%Z.
rewrite binary_to_Z_to_binary.
rewrite binary_to_Z_to_binary; elim x; auto.
generalize
(NormalNotSubNormal radix b
(Fnormalize radix b (precision p)
(Float
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))
(binary_value (nbexp p) (IEEE_Exp x) - (biais1 + biais2)))));
intros H5.
Contradict H5; split; auto.
rewrite FcanonicFnormalizeEq; auto with arith zarith.
left; auto.
split; auto with zarith.
rewrite V.
apply
Zle_trans
with
(Zabs
(radix *
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x))));
auto with zarith.
rewrite Zabs_eq; auto with zarith.
replace
(radix *
(Zpower_nat radix (pred (precision p)) +
binary_value (pred (precision p)) (IEEE_Frac x)))%Z with
(binary_value (pred (precision p)) (IEEE_Frac x)*radix+
Zpower_nat radix (pred (precision p))*radix)%Z by ring.
apply Zle_trans with (0 * radix + Zpower_nat radix (precision p))%Z;
auto with zarith; apply Zplus_le_compat.
apply Zmult_le_compat_r; auto with zarith.
apply Zge_le; apply binary_value_pos.
repeat rewrite <- two_power_nat_correct.
unfold radix in |- *; pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p)));
[ idtac | auto with arith zarith ].
rewrite two_power_nat_S; auto with zarith.
apply Zle_trans with (0*0)%Z; auto with zarith.
apply Zmult_le_compat; auto with zarith.
apply Zle_trans with (0+0)%Z; auto with zarith.
apply Zplus_le_compat; auto with zarith.
apply Zge_le; apply binary_value_pos.
Qed.
Theorem Float_To_IEEE_To_Float :
forall (f : float) H,
InDomain f ->
IEEE_To_Float (Float_To_IEEE f H) = Fnormalize radix b (precision p) f.
generalize vNum_eq_Zpower; intros V.
intros f H1 H2.
cut (0 < biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2)%Z;
[ intros V1 | idtac ].
2: apply Zplus_lt_reg_l with (- (biais1 + biais2))%Z.
2: ring_simplify
(- (biais1 + biais2) +
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))%Z.
2: replace (- (biais1 + biais2) + 0)%Z with (- (biais1 + biais2))%Z;
[ idtac | ring ].
2: apply Zlt_le_trans with (- dExp b)%Z; auto with zarith float.
2: apply Zlt_Zopp; unfold b, biais2 in |- *; simpl in |- *.
2: assert (Y:(0 < (Zpred (Zpred exp_max + precision p)))%Z).
2: assert (2 < exp_max+precision p)%Z; unfold Zpred; auto with zarith.
2: assert (1 < precision p)%Z; auto with zarith.
2: assert (1 <= exp_max)%Z; auto with zarith.
2: unfold exp_max; apply Zle_trans with (Zpred (Zpower_nat radix (pred (2)))).
2: simpl; auto with zarith.
2: unfold Zpred; auto with zarith.
2: apply Zle_lt_trans with (Zpred (Zpred exp_max + precision p)).
2: apply Zeq_le.
2: apply trans_eq with
(Z_of_nat
(nat_of_P
(P_of_succ_nat
(pred (Zabs_nat ((Zpred (Zpred exp_max + precision p)))))))).
2: unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
auto with zarith.
2:rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
2: rewrite <- (S_pred (Zabs_nat (Zpred (Zpred exp_max + precision p))) 0); auto with zarith.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: cut (0 < Zabs_nat (Zpred (Zpred exp_max + precision p)))%Z; auto with zarith.
2: rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
2: unfold biais1, Zpred; auto with zarith.
elim H2; intros H3 H4; clear H4.
cut
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2 <
two_power_nat (nbexp p))%Z; [ intros V2 | idtac ].
2: apply Zle_lt_trans with (exp_max + exp_max)%Z; auto with zarith.
2: pattern exp_max at 1 in |- *; replace exp_max with biais1;
auto with zarith.
2: rewrite two_power_nat_correct.
2: replace (exp_max + exp_max)%Z with (2 * exp_max)%Z; auto with zarith.
2: unfold exp_max in |- *.
2: apply Zlt_le_trans with (2 * Zpower_nat radix (pred (nbexp p)))%Z;
auto with zarith.
2: apply Zmult_gt_0_lt_compat_l; auto with zarith.
2: pattern (nbexp p) at 2 in |- *;
replace (nbexp p) with (S (pred (nbexp p))); auto with zarith arith.
unfold Float_To_IEEE in |- *.
case (FNorm_or_Subnorm f H1); intros H5.
unfold FNormTo_IEEE in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H4.
unfold IEEE_To_Float in |- *; simpl in |- *.
unfold IEEE_Pos_To_Float in |- *.
case
(Expo_zero_or_pos
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))));
simpl in |- *; intros H6.
Contradict H6.
rewrite Z_to_binary_to_Z; auto with zarith.
rewrite Z_to_binary_to_Z; auto with zarith.
unfold Fopp in |- *; simpl in |- *.
ring_simplify
(-
(Zpower_nat radix (pred (precision p)) +
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)))))%Z.
rewrite Z_to_binary_to_Z; auto with zarith.
ring_simplify
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2 -
(biais1 + biais2))%Z.
elim (Fnormalize radix b (precision p) f); auto.
elim H5; intros T1 T2; clear T1; apply Zle_ge.
apply Zplus_le_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify.
apply Zmult_le_reg_r with radix;
[ unfold radix in |- *; auto with zarith | idtac ].
apply Zle_trans with (Zpos (vNum b));
[ rewrite V | apply Zle_trans with (1 := T2) ].
repeat rewrite <- two_power_nat_correct.
pattern (precision p) at 2 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith.
generalize Prec_Greater_Than_One; auto with arith zarith.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
apply Zeq_le; ring.
apply Zle_trans with (- (0))%Z; auto with zarith; apply Zle_Zopp.
cut (Fnum (Fnormalize radix b (precision p) f) < 0)%Z.
intros T; replace 0%Z with (radix * 0)%Z; auto with zarith.
apply R0LtFnum with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR in |- *;
simpl in |- *; auto with real zarith.
apply Rlt_le_trans with (0 * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
replace 0%R with (IZR 0); auto with real zarith; apply Rlt_IZR; auto.
apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify
(- Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z.
apply Zle_lt_trans with (Zabs (Fnum (Fnormalize radix b (precision p) f)));
auto with zarith.
rewrite <- Zabs_Zopp; auto with zarith.
apply Zlt_le_trans with (Zpos (vNum b)).
elim H5; auto with float zarith.
rewrite V; repeat rewrite <- two_power_nat_correct.
pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith arith.
generalize Prec_Greater_Than_One; auto with arith zarith.
unfold IEEE_To_Float in |- *; simpl in |- *.
unfold IEEE_Pos_To_Float in |- *.
case
(Expo_zero_or_pos
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))
(Z_to_binary (nbexp p)
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2))));
simpl in |- *; intros H6.
Contradict H6.
rewrite Z_to_binary_to_Z; auto with zarith.
rewrite Z_to_binary_to_Z; auto with zarith.
ring_simplify
(Zpower_nat radix (pred (precision p)) +
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p))))%Z.
rewrite Z_to_binary_to_Z; auto with zarith.
ring_simplify
(biais1 + Fexp (Fnormalize radix b (precision p) f) + biais2 -
(biais1 + biais2))%Z.
elim (Fnormalize radix b (precision p) f); auto.
elim H5; intros T1 T2; clear T1; apply Zle_ge.
apply Zplus_le_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify.
apply Zmult_le_reg_r with radix;
[ unfold radix in |- *; auto with zarith | idtac ].
apply Zle_trans with (Zpos (vNum b));
[ rewrite V | apply Zle_trans with (1 := T2) ].
repeat rewrite <- two_power_nat_correct.
pattern (precision p) at 2 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith.
generalize Prec_Greater_Than_One; auto with arith zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zmult_comm; replace 0%Z with (0 * radix)%Z; auto with zarith.
apply Zmult_gt_0_le_compat_r;
[ unfold radix in |- *; auto with zarith | idtac ].
apply LeR0Fnum with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR in |- *;
simpl in |- *; auto with real zarith.
apply Rle_trans with (0 * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
ring_simplify
(Fnum (Fnormalize radix b (precision p) f) -
Zpower_nat radix (pred (precision p)) +
Zpower_nat radix (pred (precision p)))%Z.
apply Zle_lt_trans with (Zabs (Fnum (Fnormalize radix b (precision p) f)));
auto with zarith.
apply Zlt_le_trans with (Zpos (vNum b)).
elim H5; auto with float zarith.
rewrite V; repeat rewrite <- two_power_nat_correct.
pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith arith.
generalize Prec_Greater_Than_One; auto with arith zarith.
unfold FSubnormTo_IEEE in |- *; simpl in |- *.
case (Z_lt_ge_dec (Fnum f) 0); intros H6.
unfold IEEE_To_Float in |- *; simpl in |- *.
unfold IEEE_Pos_To_Float in |- *; simpl in |- *.
case
(Expo_zero_or_pos
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))); intros H7.
rewrite Z_to_binary_to_Z; auto with zarith.
unfold Fopp in |- *; simpl in |- *.
ring_simplify (- (- Fnum (Fnormalize radix b (precision p) f)))%Z.
replace (Zneg
(P_of_succ_nat
(pred (Zabs_nat (Zpred (Zpred exp_max + precision p))))))
with (Fexp (Fnormalize radix b (precision p) f)).
elim (Fnormalize radix b (precision p) f); auto.
elim H5; intros T1 T2; elim T2; intros T3 T4; rewrite T3; clear T1 T2 T3 T4.
unfold b; simpl; auto with zarith.
apply Zle_ge; replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp;
auto with zarith.
apply R0LeFnum with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR in |- *;
simpl in |- *; auto with real zarith.
apply Rle_trans with (0 * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
replace 0%R with (IZR 0); auto with real zarith; apply Rle_IZR; auto.
elim H5; intros T1 T2; elim T2; intros T3 T4; clear T1 T2 T3.
apply Zmult_gt_0_lt_reg_r with radix;
[ unfold radix in |- *; auto with zarith | idtac ].
apply
Zle_lt_trans
with (Zabs (- Fnum (Fnormalize radix b (precision p) f) * radix));
auto with zarith.
rewrite <- Zabs_Zopp.
ring_simplify (- (- Fnum (Fnormalize radix b (precision p) f) * radix))%Z.
rewrite Zmult_comm; apply Zlt_le_trans with (1 := T4); rewrite V.
rewrite <- two_power_nat_correct; pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith arith.
generalize Prec_Greater_Than_One; auto with arith zarith.
cut
(binary_value (nbexp p)
(IEEE_Exp
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) = 0%Z); auto with zarith.
intros H8; Contradict H7; auto with zarith.
simpl in |- *; rewrite Z_to_binary_to_Z; auto with zarith.
unfold IEEE_To_Float in |- *; simpl in |- *.
unfold IEEE_Pos_To_Float in |- *; simpl in |- *.
case
(Expo_zero_or_pos
(IEEE_construct false
(Z_to_binary (pred (precision p))
(Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))); intros H7.
rewrite Z_to_binary_to_Z; auto with zarith.
replace (Zneg
(P_of_succ_nat
(pred (Zabs_nat (Zpred (Zpred exp_max + precision p)))))) with
(Fexp (Fnormalize radix b (precision p) f)).
elim (Fnormalize radix b (precision p) f); auto.
elim H5; intros T1 T2; elim T2; intros T3 T4; rewrite T3; clear T1 T2 T3 T4.
unfold b in |- *; simpl in |- *; auto with zarith.
apply Zle_ge; apply LeR0Fnum with radix; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR in |- *;
simpl in |- *; auto with real zarith.
apply Rle_trans with (0 * powerRZ 2%Z (Fexp f))%R; auto with real zarith.
elim H5; intros T1 T2; elim T2; intros T3 T4; clear T1 T2 T3.
apply Zmult_gt_0_lt_reg_r with radix;
[ unfold radix in |- *; auto with zarith | idtac ].
apply
Zle_lt_trans with (Zabs (Fnum (Fnormalize radix b (precision p) f) * radix));
auto with zarith.
rewrite Zmult_comm; apply Zlt_le_trans with (1 := T4); rewrite V.
rewrite <- two_power_nat_correct; pattern (precision p) at 1 in |- *;
replace (precision p) with (S (pred (precision p))).
rewrite two_power_nat_S; auto with zarith arith.
generalize Prec_Greater_Than_One; auto with arith zarith.
cut
(binary_value (nbexp p)
(IEEE_Exp
(IEEE_construct true
(Z_to_binary (pred (precision p))
(- Fnum (Fnormalize radix b (precision p) f)))
(Z_to_binary (nbexp p) 0))) = 0%Z); auto with zarith.
intros H8; Contradict H7; auto with zarith.
simpl in |- *; rewrite Z_to_binary_to_Z; auto with zarith.
Qed.
End IEEEdefs.