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