proposition: Theorem Bplus_correct : forall 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 m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\ is_finite (Bplus m x y) = true /\ Bsign (Bplus 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 (B2SF (Bplus m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y).
proof: Proof. Proof with auto with typeclass_instances. intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy. rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true... simpl. rewrite Rcompare_Eq by auto. destruct sx, sy; try easy; now case m. apply bpow_gt_0. rewrite Rplus_0_l, round_generic, Rlt_bool_true... split... split... simpl. unfold F2R. erewrite <- Rmult_0_l, Rcompare_mult_r. rewrite Rcompare_IZR with (y:=0%Z). destruct sy... apply bpow_gt_0. apply abs_B2R_lt_emax. apply generic_format_B2R. rewrite Rplus_0_r, round_generic, Rlt_bool_true... split... split... simpl. unfold F2R. erewrite <- Rmult_0_l, Rcompare_mult_r. rewrite Rcompare_IZR with (y:=0%Z). destruct sx... apply bpow_gt_0. apply abs_B2R_lt_emax. apply generic_format_B2R. clear Fx Fy. simpl. set (szero := match m with mode_DN => true | _ => false end). set (ez := Z.min ex ey). assert (Hp := Fplus_naive_correct sx mx ex sy my ey ez (Z.le_min_l _ _) (Z.le_min_r _ _)). set (mz := Fplus_naive sx mx ex sy my ey ez). simpl in Hp. fold mz in Hp. rewrite <- Hp. generalize (binary_normalize_correct m mz ez szero). simpl. case Rlt_bool_spec ; intros Hz. intros [H1 [H2 H3]]. apply (conj H1). apply (conj H2). rewrite H3. case Rcompare_spec ; try easy. intros Hz'. rewrite Hz' in Hp. apply eq_sym, Rplus_opp_r_uniq in Hp. rewrite <- F2R_Zopp in Hp. eapply canonical_unique in Hp. inversion Hp. clear -H0. destruct sy, sx, m ; easy. now apply canonical_bounded. rewrite <- cond_Zopp_negb. now apply canonical_bounded. intros Vz. rewrite Hp in Hz. assert (Sz := sign_plus_overflow m sx mx ex sy my ey Hx Hy Hz). split. rewrite Vz. apply f_equal. now rewrite Hp. apply Sz. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative