proposition: Lemma equivFloat_Op_MUL_BinFloat {Tl} : forall (t1 t2 : ArithExpr Tl BinFloat) (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) -> Rabs (@Rrnd.Rnd md (evalRounded t1 lM md * evalRounded t2 lM md)) <= Rrnd.maxval -> eqExprTypeFloat (evalFloat (Op MUL t1 t2) lC md) (evalRounded (Op MUL t1 t2) lM md).
proof: Proof. intros t1 t2 lC md lM [convt1 isconvt1] [convt2 isconvt2] H. generalize (Bmult_correct _ _ HPrec_gt_0 HPrec_lt_emax md (evalFloat t1 lC md) (evalFloat t2 lC md)). rewrite Rlt_bool_true. 2: { rewrite isconvt1, isconvt2. apply Rle_lt_trans with Rrnd.maxval; [assumption |]. apply Rrnd.maxval_lt. } intros [H1 [H2 H3]]. unfold eqExprTypeFloat. simpl. unfold FPmul. rewrite H2. split; [now apply andb_true_intro |]. rewrite H1. unfold Rrnd.Rnd, SpecFloat.fexp, FLT_exp, SpecFloat.emin, Rrnd.emin. now rewrite isconvt1, isconvt2. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)