proposition: Theorem Bfma_correct: forall fma_nan m x y z, is_finite x = true -> is_finite y = true -> is_finite z = true -> let res := (B2R x * B2R y + B2R z)%R in if Rlt_bool (Rabs (round radix2 fexp (round_mode m) res)) (bpow radix2 emax) then B2R (Bfma fma_nan m x y z) = round radix2 fexp (round_mode m) res /\ is_finite (Bfma fma_nan m x y z) = true /\ Bsign (Bfma fma_nan m x y z) = match Rcompare res 0 with | Eq => Bfma_szero m x y z | Lt => true | Gt => false end else B2FF (Bfma fma_nan m x y z) = binary_overflow m (Rlt_bool res 0).
proof: Proof. intros fma_nan mode x y z Fx Fy Fz. rewrite <- is_finite_B2BSN in Fx, Fy, Fz. generalize (Bfma_correct prec emax _ _ mode _ _ _ Fx Fy Fz). replace (BinarySingleNaN.Bfma _ _ _ _) with (B2BSN (Bfma fma_nan mode x y z)) by apply B2BSN_BSN2B. rewrite 3!B2R_B2BSN. cbv zeta. destruct Rlt_bool. - now destruct Bfma. - 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