proposition: Theorem Bplus_correct : forall plus_nan m x y, is_finite x = true -> is_finite y = true -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x + B2R y))) (bpow radix2 emax) then B2R (Bplus plus_nan m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\ is_finite (Bplus plus_nan m x y) = true /\ Bsign (Bplus plus_nan m x y) = match Rcompare (B2R x + B2R y) 0 with | Eq => match m with mode_DN => orb (Bsign x) (Bsign y) | _ => andb (Bsign x) (Bsign y) end | Lt => true | Gt => false end else (B2FF (Bplus plus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
proof: Proof. Proof with auto with typeclass_instances. intros plus_nan mode x y Fx Fy. rewrite <- is_finite_B2BSN in Fx, Fy. generalize (Bplus_correct prec emax _ _ mode _ _ Fx Fy). replace (BinarySingleNaN.Bplus _ _ _) with (B2BSN (Bplus plus_nan mode x y)) by apply B2BSN_BSN2B. rewrite 2!B2R_B2BSN. rewrite (Bsign_B2BSN x) by (clear -Fx ; now destruct x). rewrite (Bsign_B2BSN y) by (clear -Fy ; now destruct y). destruct Rlt_bool. - now destruct Bplus. - intros [H1 H2]. refine (conj _ H2). 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