proposition: Theorem Bldexp_correct : forall m (f : binary_float) e, if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R f * bpow radix2 e))) (bpow radix2 emax) then (B2R (Bldexp m f e) = round radix2 fexp (round_mode m) (B2R f * bpow radix2 e))%R /\ is_finite (Bldexp m f e) = is_finite f /\ Bsign (Bldexp m f e) = Bsign f else B2SF (Bldexp m f e) = binary_overflow m (Bsign f).
proof: Proof. intros m f e. case f. - intro s; simpl; rewrite Rmult_0_l, round_0; [|apply valid_rnd_round_mode]. now rewrite Rabs_R0, Rlt_bool_true; [|now apply bpow_gt_0]. - intro s; simpl; rewrite Rmult_0_l, round_0; [|apply valid_rnd_round_mode]. now rewrite Rabs_R0, Rlt_bool_true; [|now apply bpow_gt_0]. - simpl; rewrite Rmult_0_l, round_0; [|apply valid_rnd_round_mode]. now rewrite Rabs_R0, Rlt_bool_true; [|now apply bpow_gt_0]. - intros s mf ef Hmef. case (Rlt_bool_spec _ _); intro Hover. + unfold Bldexp; rewrite B2R_SF2B, is_finite_SF2B, Bsign_SF2B. simpl; unfold F2R; simpl; rewrite Rmult_assoc, <-bpow_plus. destruct (binary_round_correct m s mf (ef + e)) as (Hf, Hr). fold emin in Hr; simpl in Hr; rewrite Rlt_bool_true in Hr. * now destruct Hr as (Hr, (Hfr, Hsr)); rewrite Hr, Hfr, Hsr. * now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus. + unfold Bldexp; rewrite B2SF_SF2B; simpl. destruct (binary_round_correct m s mf (ef + e)) as (Hf, Hr). fold emin in Hr; simpl in Hr; rewrite Rlt_bool_false in Hr; [exact Hr|]. now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative