proposition: Theorem Bfma_correct: forall 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 m x y z) = round radix2 fexp (round_mode m) res /\ is_finite (Bfma m x y z) = true /\ Bsign (Bfma m x y z) = match Rcompare res 0 with | Eq => Bfma_szero m x y z | Lt => true | Gt => false end else B2SF (Bfma m x y z) = binary_overflow m (Rlt_bool res 0).
proof: Proof. intros. pattern (Bfma m x y z). match goal with |- ?p ?x => set (PROP := p) end. set (szero := Bfma_szero m x y z). assert (BINORM: forall mr er, F2R (Float radix2 mr er) = res -> PROP (binary_normalize m mr er szero)). { intros mr er E. specialize (binary_normalize_correct m mr er szero). change (FLT_exp (3 - emax - prec) prec) with fexp. rewrite E. tauto. } set (add_zero := match z with | B754_nan => B754_nan | B754_zero sz => B754_zero szero | _ => z end). assert (ADDZERO: B2R x = 0%R \/ B2R y = 0%R -> PROP add_zero). { intros Z. assert (RES: res = B2R z). { unfold res. destruct Z as [E|E]; rewrite E, ?Rmult_0_l, ?Rmult_0_r, Rplus_0_l; auto. } unfold PROP, add_zero; destruct z as [ sz | sz | | sz mz ez Bz]; try discriminate. - simpl in RES; rewrite RES; rewrite round_0 by apply valid_rnd_round_mode. rewrite Rlt_bool_true. split. reflexivity. split. reflexivity. rewrite Rcompare_Eq by auto. reflexivity. rewrite Rabs_R0; apply bpow_gt_0. - rewrite RES, round_generic, Rlt_bool_true. split. reflexivity. split. reflexivity. unfold B2R. destruct sz. rewrite Rcompare_Lt. auto. apply F2R_lt_0. reflexivity. rewrite Rcompare_Gt. auto. apply F2R_gt_0. reflexivity. apply abs_B2R_lt_emax. apply valid_rnd_round_mode. apply generic_format_B2R. } destruct x as [ sx | sx | | sx mx ex Bx]; destruct y as [ sy | sy | | sy my ey By]; try discriminate. - apply ADDZERO; auto. - apply ADDZERO; auto. - apply ADDZERO; auto. - destruct z as [ sz | sz | | sz mz ez Bz]; try discriminate; unfold Bfma. + set (X := Float radix2 (cond_Zopp sx (Zpos mx)) ex). set (Y := Float radix2 (cond_Zopp sy (Zpos my)) ey). destruct (Fmult X Y) as [mr er] eqn:FRES. apply BINORM. unfold res. rewrite <- FRES, F2R_mult, Rplus_0_r. auto. + set (X := Float radix2 (cond_Zopp sx (Zpos mx)) ex). set (Y := Float radix2 (cond_Zopp sy (Zpos my)) ey). set (Z := Float radix2 (cond_Zopp sz (Zpos mz)) ez). destruct (Fplus (Fmult X Y) Z) as [mr er] eqn:FRES. apply BINORM. unfold res. rewrite <- FRES, F2R_plus, F2R_mult. auto. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative