proposition: Lemma equivPrim_Fma {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 (@Rrnd.fma mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) (evalRounded t3 lM mode_NE)) <= Rrnd.maxval -> eqExprTypePrim (evalPrim (Fma t1 t2 t3) lP) (evalRounded (Fma t1 t2 t3) lM mode_NE).
proof: Proof. intros t1 t2 t3 lP lM [convt1 isconvt1] [convt2 isconvt2] [convt3 isconvt3] H. generalize (Bfma_correct _ _ HPrec_gt_0 HPrec_lt_emax mode_NE (P2C (evalPrim t1 lP)) (P2C (evalPrim t2 lP)) (P2C (evalPrim t3 lP))). unfold eqExprTypePrim. simpl. unfold isConversionPrim in isconvt1, isconvt2, isconvt3. rewrite <-4is_finite_SF_B2SF, 3B2SF_Prim2B. rewrite <-B2SF_Prim2B, SF2R_B2SF in isconvt1, isconvt2, isconvt3. rewrite Rlt_bool_true. { intros [H1 [H2 H3]]; [assumption.. |]. rewrite Prim2SF_B2Prim. split; [easy |]. unfold FPfma. change Rrnd.prec with prec in H1 |- *. change Rrnd.emax with emax in H1 |- *. rewrite SF2R_B2SF. now rewrite H1, isconvt1, isconvt2, isconvt3. } change Rrnd.prec with prec. change Rrnd.emax with emax. 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)