proposition: Lemma equivPrim_Op_ADD_BinFloat {Tl} : forall (t1 t2 : 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) -> Rabs (@Rrnd.Rnd mode_NE (evalRounded t1 lM mode_NE + evalRounded t2 lM mode_NE)) <= Rrnd.maxval -> eqExprTypePrim (evalPrim (Op ADD t1 t2) lP) (evalRounded (Op ADD t1 t2) lM mode_NE).
proof: Proof. intros t1 t2 lP lM [convt1 isconvt1] [convt2 isconvt2] H. unfold eqExprTypePrim; simpl. generalize (Bplus_correct _ _ HPrec_gt_0 HPrec_lt_emax mode_NE (Prim2B (evalPrim t1 lP)) (Prim2B (evalPrim t2 lP))). rewrite <-add_equiv, <-3is_finite_SF_B2SF, <-3SF2R_B2SF, 3B2SF_Prim2B. rewrite Rlt_bool_true. 2: { rewrite isconvt1, isconvt2. simpl round_mode. apply Rle_lt_trans with Rrnd.maxval; [assumption |]. apply Rrnd.maxval_lt. } intros [H1 [H2 H3]]; [assumption.. |]. unfold eqExprTypePrim. simpl. unfold FloatOps.prec, FloatOps.emax, Rrnd.prec, Rrnd.emax, Format64.prec, Format64.emax in *. unfold HPrec_gt_0, HPrec_lt_emax in H1. now rewrite H1, isconvt1, isconvt2. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)