proposition: Lemma equivPrim_FmaExact {Tl} : forall (t1 t2 t3 : ArithExpr Tl BinFloat) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) -> eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) -> eqExprTypePrim (evalPrim t3 lP) (evalRounded t3 lM mode_NE) -> Rabs (evalRounded t1 lM mode_NE * evalRounded t2 lM mode_NE + evalRounded t3 lM mode_NE) <= Rrnd.maxval -> (@Rrnd.fma mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) (evalRounded t3 lM mode_NE)) = evalRounded t1 lM mode_NE * evalRounded t2 lM mode_NE + evalRounded t3 lM mode_NE -> eqExprTypePrim (evalPrim (FmaExact t1 t2 t3) lP) (evalRounded (FmaExact t1 t2 t3) lM mode_NE).
proof: Proof. intros t1 t2 t3 lP lM [convt1 isconvt1] [convt2 isconvt2] [convt3 isconvt3] H0 H1. simpl. rewrite <-H1 in H0 |- *. now apply equivPrim_Fma. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)