proposition: Theorem binary_float_of_bits_of_binary_float : forall x, binary_float_of_bits (bits_of_binary_float x) = x.
proof: Proof. intros x. apply B2FF_inj. unfold binary_float_of_bits. rewrite B2FF_FF2B. unfold binary_float_of_bits_aux. rewrite split_bits_of_binary_float_correct. destruct x as [sx|sx|sx plx Hplx|sx mx ex Bx]. apply refl_equal. simpl. rewrite Zeq_bool_false. now rewrite Zeq_bool_true. cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). simpl. rewrite Zeq_bool_false. rewrite Zeq_bool_true; auto. cut (1 < 2^ew)%Z. clear ; lia. now apply (Zpower_gt_1 radix2). unfold split_bits_of_binary_float. case Zle_bool_spec ; intros Hm. rewrite Zeq_bool_false. rewrite Zeq_bool_false. now ring_simplify (Zpos mx - 2 ^ mw + 2 ^ mw)%Z (ex - emin + 1 + emin - 1)%Z. destruct (andb_prop _ _ Bx) as (_, H1). generalize (Zle_bool_imp_le _ _ H1). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. clear ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. clear -Hew ; lia. destruct (andb_prop _ _ Bx) as (H1, _). generalize (Zeq_bool_eq _ _ H1). rewrite Zpos_digits2_pos. unfold FLT_exp, emin. generalize (Zdigits radix2 (Zpos mx)). clear. unfold fexp, emin. intros ; lia. rewrite Zeq_bool_true. 2: apply refl_equal. simpl. apply f_equal. destruct (andb_prop _ _ Bx) as (H1, _). generalize (Zeq_bool_eq _ _ H1). rewrite Zpos_digits2_pos. unfold FLT_exp, emin, prec. apply -> Z.lt_sub_0 in Hm. generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm). generalize (Zdigits radix2 (Zpos mx)). clear. unfold fexp, emin. intros ; lia. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary