proposition: Theorem Bmult_correct : forall mult_nan m x y, if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then B2R (Bmult mult_nan m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\ is_finite (Bmult mult_nan m x y) = andb (is_finite x) (is_finite y) /\ (is_nan (Bmult mult_nan m x y) = false -> Bsign (Bmult mult_nan m x y) = xorb (Bsign x) (Bsign y)) else B2FF (Bmult mult_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
proof: Proof. intros mult_nan mode x y. generalize (Bmult_correct prec emax _ _ mode (B2BSN x) (B2BSN y)). replace (BinarySingleNaN.Bmult _ _ _) with (B2BSN (Bmult mult_nan mode x y)) by apply B2BSN_BSN2B. intros H. destruct x as [sx|sx|sx plx Hplx|sx mx ex Hx] ; destruct y as [sy|sy|sy ply Hply|sy my ey Hy] ; try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ try easy | apply bpow_gt_0 | now auto with typeclass_instances ]). revert H. rewrite 2!B2R_B2BSN. destruct Rlt_bool. - now destruct Bmult. - intros H. apply eq_binary_overflow_FF2SF. now rewrite FF2SF_B2FF, <- B2SF_B2BSN. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN