proposition: Theorem bits_of_binary_float_of_bits : forall x, (0 <= x < 2^(mw+ew+1))%Z -> bits_of_binary_float (binary_float_of_bits x) = x.
proof: Proof. intros x Hx. unfold binary_float_of_bits, bits_of_binary_float. set (Cx := binary_float_of_bits_aux_correct x). clearbody Cx. rewrite match_FF2B. revert Cx. generalize (join_split_bits x Hx). unfold binary_float_of_bits_aux. case_eq (split_bits x). intros (sx, mx) ex Sx. assert (Bm: (0 <= mx < 2^mw)%Z). inversion_clear Sx. apply Z_mod_lt. now apply Z.lt_gt. case Zeq_bool_spec ; intros He1. case_eq mx. intros Hm Jx _. now rewrite He1 in Jx. intros px Hm Jx _. rewrite Zle_bool_false. now rewrite <- He1. apply <- Z.lt_sub_0. now rewrite <- Hm. intros px Hm _ _. apply False_ind. apply Zle_not_lt with (1 := proj1 Bm). now rewrite Hm. case Zeq_bool_spec ; intros He2. case_eq mx; intros Hm. now rewrite He2. now rewrite He2. intros ; lia. case_eq (mx + 2 ^ mw)%Z. intros Hm. apply False_ind. clear -Bm Hm ; lia. intros p Hm Jx Cx. rewrite <- Hm. rewrite Zle_bool_true. now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z. now ring_simplify. intros p Hm. apply False_ind. clear -Bm Hm ; lia. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary