Commit 25fa9f62 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean valid_binary.

parent 6165fc73
......@@ -58,18 +58,19 @@ Definition canonical_mantissa m e :=
Definition bounded m e :=
andb (canonical_mantissa m e) (Zle_bool e (emax - prec)).
Definition nan_pl pl :=
Zlt_bool (Zpos (digits2_pos pl)) prec.
Definition valid_binary x :=
match x with
| F754_finite _ m e => bounded m e
| F754_nan _ pl => (Zpos (digits2_pos pl) <? prec)%Z
| F754_nan _ pl => nan_pl pl
| _ => true
end.
(** Basic type used for representing binary FP numbers.
Note that there is exactly one such object per FP datum. *)
Definition nan_pl pl := (Zpos (digits2_pos pl) <? prec)%Z.
Inductive binary_float :=
| B754_zero (s : bool)
| B754_infinity (s : bool)
......
......@@ -360,6 +360,10 @@ Lemma binary_float_of_bits_aux_correct :
Proof.
intros x.
unfold binary_float_of_bits_aux, split_bits.
assert (Hnan: nan_pl prec 1 = true).
apply Z.ltb_lt.
simpl. unfold prec.
clear -Hmw ; omega.
case Zeq_bool_spec ; intros He1.
case_eq (x mod 2^mw)%Z ; try easy.
(* subnormal *)
......@@ -390,7 +394,6 @@ cut (0 < emax)%Z. clear -H Hew ; omega.
apply (Zpower_gt_0 radix2).
clear -Hew ; omega.
apply bpow_gt_0.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
case Zeq_bool_spec ; intros He2.
case_eq (x mod 2 ^ mw)%Z; try easy.
(* nan *)
......@@ -401,9 +404,7 @@ apply Zdigits_le_Zpower. simpl.
rewrite <- Eqplx. edestruct Z_mod_lt; eauto.
change 2%Z with (radix_val radix2).
apply Z.lt_gt, Zpower_gt_0. omega.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
case_eq (x mod 2^mw + 2^mw)%Z ; try easy.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
(* normal *)
intros px Hm.
assert (prec = Zdigits radix2 (Zpos px)).
......@@ -474,7 +475,6 @@ apply Zlt_gt.
apply (Zpower_gt_0 radix2).
now apply Zlt_le_weak.
apply bpow_gt_0.
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
Qed.
Definition binary_float_of_bits x :=
......
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