proposition: Theorem Bulp'_correct : (2 < emax)%Z -> forall x, is_finite x = true -> Bulp' x = Bulp x.
proof: Proof. intros Hp x Fx. assert (B2R (Bulp' x) = ulp radix2 fexp (B2R x) /\ is_finite (Bulp' x) = true /\ Bsign (Bulp' x) = false) as [H1 [H2 H3]]. { destruct x as [sx|sx| |sx mx ex Hx] ; unfold Bulp'. - replace (fexp _) with emin. + generalize (Bldexp_correct mode_NE Bone emin). rewrite Bone_correct, Rmult_1_l, round_generic; [|now apply valid_rnd_N|apply generic_format_bpow; unfold fexp, FLT_exp; rewrite Z.max_r; unfold Prec_gt_0 in prec_gt_0_; lia]. rewrite Rlt_bool_true. * intros (Hr, (Hf, Hs)); rewrite Hr, Hf, Hs. split; [|now split; [apply is_finite_Bone|apply Bsign_Bone]]. simpl; unfold ulp; rewrite Req_bool_true; [|reflexivity]. destruct (negligible_exp_FLT emin prec) as (n, (Hn, Hn')). change fexp with (FLT_exp emin prec); rewrite Hn. now unfold FLT_exp; rewrite Z.max_r; [|unfold Prec_gt_0 in prec_gt_0_; lia]. * rewrite Rabs_pos_eq; [|now apply bpow_ge_0]; apply bpow_lt. apply emin_lt_emax. + simpl; change (fexp _) with (fexp (-2 * emax - prec)). unfold fexp, FLT_exp; rewrite Z.max_r; [reflexivity|]. unfold emin; unfold Prec_gt_0 in prec_gt_0_; lia. - discriminate. - discriminate. - unfold ulp, cexp. set (f := B754_finite _ _ _ _). rewrite Req_bool_false. + destruct (Bfrexp_correct f (eq_refl _)) as (Hfr1, (Hfr2, Hfr3)). apply Hp. simpl. rewrite Hfr3. set (e' := fexp _). generalize (Bldexp_correct mode_NE Bone e'). rewrite Bone_correct, Rmult_1_l, round_generic; [|now apply valid_rnd_N|]. { rewrite Rlt_bool_true. - intros (Hr, (Hf, Hs)); rewrite Hr, Hf, Hs. now split; [|split; [apply is_finite_Bone|apply Bsign_Bone]]. - rewrite Rabs_pos_eq; [|now apply bpow_ge_0]. unfold e', fexp, FLT_exp. apply bpow_lt. case (Z.max_spec (mag radix2 (B2R f) - prec) emin) as [(_, Hm)|(_, Hm)]; rewrite Hm. apply emin_lt_emax. apply (Zplus_lt_reg_r _ _ prec); ring_simplify. assert (mag radix2 (B2R f) <= emax)%Z; [|now unfold Prec_gt_0 in prec_gt_0_; lia]. apply mag_le_bpow; [|now apply abs_B2R_lt_emax]. now unfold f, B2R; apply F2R_neq_0; case sx. } apply generic_format_bpow, Z.max_lub. * unfold Prec_gt_0 in prec_gt_0_; lia. * apply Z.le_max_r. + now unfold f, B2R; apply F2R_neq_0; case sx. } destruct (Bulp_correct x Fx) as [H4 [H5 H6]]. apply B2R_Bsign_inj ; try easy. now rewrite H4. now rewrite H3. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative