proposition: Theorem split_bits_of_binary_float_correct : forall x, split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
proof: Proof. intros [sx|sx|sx plx Hplx|sx mx ex Hx] ; try ( simpl ; apply split_join_bits ; split ; try apply Z.le_refl ; try apply Zlt_pred ; trivial ; lia ). simpl. apply split_join_bits; split; try lia. destruct (digits2_Pnat_correct plx). unfold nan_pl in Hplx. rewrite Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx. rewrite Zpower_nat_Z in H0. eapply Z.lt_le_trans. apply H0. change 2%Z with (radix_val radix2). apply Zpower_le. rewrite Z.ltb_lt in Hplx. unfold prec in *. lia. unfold bits_of_binary_float, split_bits_of_binary_float. assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z). destruct (andb_prop _ _ Hx) as (Hx', _). unfold canonical_mantissa in Hx'. rewrite Zpos_digits2_pos in Hx'. generalize (Zeq_bool_eq _ _ Hx'). unfold fexp, FLT_exp, emin. clear ; lia. case Zle_bool_spec ; intros H ; [ apply -> Z.le_0_sub in H | apply -> Z.lt_sub_0 in H ] ; apply split_join_bits ; try now split. split. clear -He_gt_0 H ; lia. cut (Zpos mx < 2 * 2^mw)%Z. clear ; lia. replace (2 * 2^mw)%Z with (2^prec)%Z. apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)). apply Hf. unfold prec. rewrite Zplus_comm. apply Zpower_exp ; apply Z.le_ge. discriminate. now apply Zlt_le_weak. split. generalize (proj1 Hf). clear ; lia. destruct (andb_prop _ _ Hx) as (_, Hx'). unfold emin. replace (2^ew)%Z with (2 * emax)%Z. generalize (Zle_bool_imp_le _ _ Hx'). clear ; lia. apply sym_eq. rewrite (Zsucc_pred ew). unfold Z.succ. rewrite Zplus_comm. apply Zpower_exp ; apply Z.le_ge. discriminate. now apply Zlt_0_le_0_pred. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary