proposition: Lemma equivFloat_Fma {Tl} : forall (t1 t2 t3 : ArithExpr Tl BinFloat) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) -> eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) -> eqExprTypeFloat (evalFloat t3 lC md) (evalRounded t3 lM md) -> Rabs (@Rrnd.fma md (evalRounded t1 lM md) (evalRounded t2 lM md) (evalRounded t3 lM md)) <= Rrnd.maxval -> eqExprTypeFloat (evalFloat (Fma t1 t2 t3) lC md) (evalRounded (Fma t1 t2 t3) lM md).
proof: Proof. intros t1 t2 t3 lC md lM [convt1 isconvt1] [convt2 isconvt2] [convt3 isconvt3] H. generalize (Bfma_correct _ _ HPrec_gt_0 HPrec_lt_emax md (evalFloat t1 lC md) (evalFloat t2 lC md) (evalFloat t3 lC md)). unfold eqExprTypeFloat. simpl. rewrite Rlt_bool_true. { intros [H1 [H2 H3]]; [assumption.. |]. now unfold FPfma; rewrite H1, isconvt1, isconvt2, isconvt3. } rewrite isconvt1, isconvt2, isconvt3. simpl round_mode. apply Rle_lt_trans with Rrnd.maxval; [assumption |]. apply Rrnd.maxval_lt. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)