Commit 6a16979d authored by Heiko Becker's avatar Heiko Becker

Add draft for multiplication error in attic

parent e8dd12b6
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 perturb_0_val in mult_real; auto.
rewrite perturb_0_val; 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment