proposition: Lemma equivFloat_FmaExact {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 (evalRounded t1 lM md * evalRounded t2 lM md + evalRounded t3 lM md) <= Rrnd.maxval -> (@Rrnd.fma md (evalRounded t1 lM md) (evalRounded t2 lM md) (evalRounded t3 lM md)) = evalRounded t1 lM md * evalRounded t2 lM md + evalRounded t3 lM md-> eqExprTypeFloat (evalFloat (FmaExact t1 t2 t3) lC md) (evalRounded (FmaExact t1 t2 t3) lM md).
proof: Proof. intros t1 t2 t3 lC md lM [convt1 isconvt1] [convt2 isconvt2] [convt3 isconvt3] H0 H1. simpl. rewrite <-H1 in H0 |- *. now apply equivFloat_Fma. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)