mult_abs 2.63 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
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.
15 16
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
  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.