proposition: Lemma binary_float_of_bits_aux_correct : forall x, valid_binary prec emax (binary_float_of_bits_aux x) = true.
proof: 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 ; lia. case Zeq_bool_spec ; intros He1. case_eq (x mod 2^mw)%Z ; try easy. intros px Hm. assert (Zdigits radix2 (Zpos px) <= mw)%Z. apply Zdigits_le_Zpower. simpl. rewrite <- Hm. eapply Z_mod_lt. now apply Z.lt_gt. apply bounded_canonical_lt_emax ; try assumption. unfold canonical, cexp. fold emin. rewrite mag_F2R_Zdigits. 2: discriminate. unfold Fexp, FLT_exp. apply sym_eq. apply Zmax_right. clear -H Hprec. unfold prec ; lia. apply Rnot_le_lt. intros H0. refine (_ (mag_le radix2 _ _ _ H0)). rewrite mag_bpow. rewrite mag_F2R_Zdigits. 2: discriminate. unfold emin, prec. apply Zlt_not_le. cut (0 < emax)%Z. clear -H Hew ; lia. apply (Zpower_gt_0 radix2). clear -Hew ; lia. apply bpow_gt_0. case Zeq_bool_spec ; intros He2. case_eq (x mod 2 ^ mw)%Z; try easy. intros plx Eqplx. apply Z.ltb_lt. rewrite Zpos_digits2_pos. assert (forall a b, a <= b -> a < b+1)%Z by (intros; lia). apply H. clear H. 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. lia. case_eq (x mod 2^mw + 2^mw)%Z ; try easy. intros px Hm. assert (prec = Zdigits radix2 (Zpos px)). rewrite Zdigits_mag. 2: discriminate. apply sym_eq. apply mag_unique. rewrite <- abs_IZR. unfold Z.abs. replace (prec - 1)%Z with mw by ( unfold prec ; ring ). rewrite <- IZR_Zpower with (1 := Zlt_le_weak _ _ Hmw). rewrite <- IZR_Zpower. 2: now apply Zlt_le_weak. rewrite <- Hm. split. apply IZR_le. change (radix2^mw)%Z with (0 + 2^mw)%Z. apply Zplus_le_compat_r. eapply Z_mod_lt. now apply Z.lt_gt. apply IZR_lt. unfold prec. rewrite Zpower_exp. 2: now apply Z.le_ge ; apply Zlt_le_weak. 2: discriminate. rewrite <- Zplus_diag_eq_mult_2. apply Zplus_lt_compat_r. eapply Z_mod_lt. now apply Z.lt_gt. apply bounded_canonical_lt_emax ; try assumption. unfold canonical, cexp. rewrite mag_F2R_Zdigits. 2: discriminate. unfold Fexp, fexp, FLT_exp. rewrite <- H. set (ex := ((x / 2^mw) mod 2^ew)%Z). replace (prec + (ex + emin - 1) - prec)%Z with (ex + emin - 1)%Z by ring. apply sym_eq. apply Zmax_left. revert He1. fold ex. cut (0 <= ex)%Z. unfold emin. clear ; intros H1 H2 ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. apply Rnot_le_lt. intros H0. refine (_ (mag_le radix2 _ _ _ H0)). rewrite mag_bpow. rewrite mag_F2R_Zdigits. 2: discriminate. rewrite <- H. apply Zlt_not_le. unfold emin. apply Zplus_lt_reg_r with (emax - 1)%Z. ring_simplify. revert He2. set (ex := ((x / 2^mw) mod 2^ew)%Z). cut (ex < 2^ew)%Z. replace (2^ew)%Z with (2 * emax)%Z. clear ; intros H1 H2 ; lia. replace ew with (1 + (ew - 1))%Z by ring. rewrite Zpower_exp. apply refl_equal. discriminate. clear -Hew ; lia. eapply Z_mod_lt. apply Z.lt_gt. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary