proposition: Theorem Bulp_correct : forall x, is_finite x = true -> B2R (Bulp x) = ulp radix2 fexp (B2R x) /\ is_finite (Bulp x) = true /\ Bsign (Bulp x) = false.
proof: Proof. intros [sx|sx| |sx mx ex Hx] Fx ; try easy ; simpl. - repeat split. change fexp with (FLT_exp emin prec). rewrite ulp_FLT_0 by easy. apply F2R_bpow. - destruct (binary_round_correct mode_ZR false 1 ex) as [H1 H2]. revert H2. simpl. destruct (andb_prop _ _ Hx) as [H5 H6]. replace (round _ _ _ _) with (bpow radix2 ex). rewrite Rlt_bool_true. intros [H2 [H3 H4]]. split ; [|split]. + rewrite B2R_SF2B. rewrite ulp_canonical. exact H2. now case sx. now apply canonical_canonical_mantissa. + now rewrite is_finite_SF2B. + now rewrite Bsign_SF2B. + rewrite Rabs_pos_eq by apply bpow_ge_0. apply bpow_lt. generalize (prec_gt_0 prec) (Zle_bool_imp_le _ _ H6). clear ; lia. + rewrite F2R_bpow. apply sym_eq, round_generic. typeclasses eauto. apply generic_format_FLT_bpow. easy. rewrite (canonical_canonical_mantissa false _ _ H5). apply Z.max_le_iff. now right. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative