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 B2FF (Bldexp m f e) = binary_overflow m (Bsign f).
proof: Proof. intros mode x e. generalize (Bldexp_correct prec emax _ _ mode (B2BSN x) e). replace (BinarySingleNaN.Bldexp _ _ _) with (B2BSN (Bldexp mode x e)) by apply B2BSN_lift. rewrite B2R_B2BSN. destruct Rlt_bool. - destruct x as [sx|sx|sx px Px|sx mx ex Bx] ; try easy. now destruct Bldexp. - intros H. apply eq_binary_overflow_FF2SF. rewrite B2SF_B2BSN in H. rewrite FF2SF_B2FF, H. destruct x as [sx|sx|sx px Px|sx mx ex Bx] ; simpl in H ; try easy. contradict H. unfold BinarySingleNaN.binary_overflow. now destruct overflow_to_inf. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN