Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R): eval_exp 0%R cenv e1 e1R -> eval_exp machineEpsilon cenv e1 e1F -> eval_exp 0%R cenv e2 e2R -> eval_exp machineEpsilon cenv e2 e2F -> eval_exp 0%R cenv (Binop Mult e1 e2) vR -> eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF -> (Rabs e1F <= Rabs (e1R * (1 + err1)))%R -> (Rabs e2F <= Rabs (e2R * (1 + err2)))%R -> (Rabs (vR - vF) <= 0)%R. Proof. intros e1_real e1_float e2_real e2_float mult_real mult_float bound_e1 bound_e2. (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) inversion mult_real; subst. rewrite delta_0_deterministic in mult_real; auto. rewrite delta_0_deterministic; auto. unfold eval_binop in *; simpl in *. clear delta H2. rewrite (eval_det H4 e1_real); rewrite (eval_det H5 e2_real). rewrite (eval_det H4 e1_real) in mult_real. rewrite (eval_det H5 e2_real) in mult_real. clear H4 H5 v1 v2. (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion mult_float; subst. unfold perturb; simpl. inversion H4; subst; inversion H5; subst. unfold updEnv; simpl. (* We have now obtained all necessary values from the evaluations --> remove them for readability *) clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float. repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. repeat rewrite Rsub_eq_Ropp_Rplus. repeat rewrite Ropp_plus_distr. pose proof (Rabs_triang (e1R * e2R) (- (e1F * e2F) + - (e1F * e2F * delta))). eapply Rle_trans. apply H. pose proof (Rabs_triang (- (e1F * e2F)) (- (e1F * e2F * delta))). pose proof (Rplus_le_compat_l (Rabs (e1R * e2R)) _ _ H0). eapply Rle_trans. apply H1. repeat rewrite Rabs_Ropp, Rabs_mult. repeat rewrite Rabs_mult. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rplus_le_compat_r. eapply Rmult_le_compat. apply Rabs_pos. apply Rabs_pos. apply bound_e1. apply bound_e2. repeat rewrite Rmult_plus_distr_l. repeat rewrite Rmult_1_r. eapply Rle_trans. apply H1. rewrite <- Rplus_assoc. repeat rewrite <- Rmult_eq_Ropp_Rplus. rewrite Rabs_Ropp. assert (Rabs (- e2R - - e2F)%R = Rabs (e2R - e2F)). - rewrite Rmult_eq_Ropp_Rplus. rewrite <- Ropp_plus_distr. rewrite Rabs_Ropp. rewrite <- Rmult_eq_Ropp_Rplus; auto. - rewrite H3. eapply Rplus_le_compat. + eapply Rplus_le_compat; auto. + rewrite Rabs_mult. eapply Rle_trans. eapply Rmult_le_compat_l. apply Rabs_pos. apply H2. apply Req_le; auto. Qed.