proposition: Lemma equivPrim_OpExact {Tl} : forall (t1 t2 : ArithExpr Tl BinFloat) OP (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) -> match OP with DIV => evalRounded t2 lM mode_NE <> 0 | _ => True end -> Rabs (ROpToFunction OP (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE)) <= Rrnd.maxval -> RrndOpToFunction OP mode_NE (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) = ROpToFunction OP (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE) -> eqExprTypePrim (evalPrim (OpExact OP t1 t2) lP) (evalRounded (OpExact OP t1 t2) lM mode_NE).
proof: Proof. intros t1 t2 OP lC lM eqt1 eqt2 H0 H1 H2. simpl. rewrite <-H2 in H1 |- *. destruct OP. - now apply equivPrim_Op_ADD_BinFloat. - now apply equivPrim_Op_SUB_BinFloat. - now apply equivPrim_Op_MUL_BinFloat. - now apply equivPrim_Op_DIV_BinFloat. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)