Commit 31abb240 authored by LEROY Xavier's avatar LEROY Xavier Committed by Guillaume Melquiond

Prove bits_of_binary_float_range.

parent 6c331877
......@@ -254,6 +254,57 @@ discriminate.
now apply Zlt_0_le_0_pred.
Qed.
Theorem bits_of_binary_float_range:
forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
Proof.
intros.
Local Open Scope Z_scope.
assert (J: forall s m e,
0 <= m < 2^mw -> 0 <= e < 2^ew ->
0 <= join_bits s m e < 2^(mw+ew+1)).
{
intros. unfold join_bits.
set (se := (if s then 2 ^ ew else 0) + e).
assert (0 <= se < 2^(ew+1)).
{ rewrite (Zpower_plus radix2) by omega. change (radix2^1) with 2. simpl.
unfold se. destruct s; omega. }
assert (0 <= se * 2^mw <= (2^(ew+1) - 1) * 2^mw).
{ split. apply Zmult_gt_0_le_0_compat; omega.
apply Zmult_le_compat_r; omega. }
rewrite Z.mul_sub_distr_r in H2.
replace (mw + ew + 1) with ((ew + 1) + mw) by omega.
rewrite (Zpower_plus radix2) by omega. simpl. omega.
}
assert (D: forall p n, Z.of_nat (S (digits2_Pnat p)) <= n ->
0 <= Z.pos p < 2^n).
{
intros.
generalize (digits2_Pnat_correct p). simpl. rewrite ! Zpower_nat_Z. intros [A B].
split. zify; omega. eapply Zlt_le_trans. eassumption.
apply (Zpower_le radix2); auto.
}
destruct x; unfold bits_of_binary_float.
- apply J; omega.
- apply J; omega.
- destruct n as [pl pl_range]. apply Z.ltb_lt in pl_range.
apply J. apply D. unfold prec, Z_of_nat' in pl_range; omega. omega.
- unfold bounded in e0. apply Bool.andb_true_iff in e0; destruct e0 as [A B].
apply Z.leb_le in B.
unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
assert (G: Z.of_nat (S (digits2_Pnat m)) <= prec) by (zify; omega).
assert (M: emin <= e) by (unfold emin; zify; omega).
generalize (Zle_bool_spec (2^mw) (Z.pos m)); intro SPEC; inversion SPEC.
+ apply J.
* split. omega. generalize (D _ _ G). unfold prec.
rewrite (Zpower_plus radix2) by omega.
change (radix2^1) with 2. simpl radix_val. omega.
* split. omega. unfold emin. replace (2^ew) with (2 * emax). omega.
symmetry. replace ew with (1 + (ew - 1)) by omega.
apply (Zpower_plus radix2); omega.
+ apply J. zify; omega. omega.
Local Close Scope Z_scope.
Qed.
Definition binary_float_of_bits_aux x :=
let '(sx, mx, ex) := split_bits x in
if Zeq_bool ex 0 then
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment