ErrorBounds.v 24.9 KB
Newer Older
1
(**
2
Proofs of general bounds on the error of arithmetic exprressions.
Heiko Becker's avatar
Heiko Becker committed
3
This shortens soundness proofs later.
4
Bounds are exprlained in section 5, Deriving Computable Error Bounds
5
**)
6 7 8 9 10 11 12
From Coq
     Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals.

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealSimps
     Infra.RealRationalProps Environments Infra.ExpressionAbbrevs
     ExpressionSemantics.
Heiko Becker's avatar
Heiko Becker committed
13

14 15 16
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (Const REAL n) nR REAL ->
  eval_expr E2 defVars DeltaMap (Const m n) nF m ->
17
  (Rabs (nR - nF) <= computeErrorR n m)%R.
18
Proof.
Heiko Becker's avatar
Heiko Becker committed
19
  intros eval_real eval_float.
20
  inversion eval_real; subst.
21
  rewrite delta_0_deterministic; auto.
22 23
  inversion eval_float; subst.
  unfold perturb; simpl.
24 25 26 27 28 29 30 31 32 33
  unfold computeErrorR.
  destruct m.
  { unfold Rminus. rewrite Rplus_opp_r. rewrite Rabs_R0; lra. }
  all: try rewrite Rabs_err_simpl, Rabs_mult.
  all: try apply Rmult_le_compat_l; try auto using Rabs_pos.
  unfold Rminus.
  rewrite Ropp_plus_distr.
  rewrite <- Rplus_assoc.
  rewrite Rplus_opp_r, Rplus_0_l.
  rewrite Rabs_Ropp; auto.
34 35
Qed.

36
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
37 38 39 40 41 42
      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e1)) e1R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e1) e1F m1->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e2)) e2R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e2) e2F m2 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
43
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
44 45
            (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
46 47
            DeltaMap
            (Binop Plus (Var R 1) (Var R 2)) vF m ->
Heiko Becker's avatar
Heiko Becker committed
48 49
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
50
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F + e2F) m)%R.
51
Proof.
Heiko Becker's avatar
Heiko Becker committed
52
  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
53 54
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion plus_real; subst.
55 56
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
57
  subst; simpl in H3; auto.
58
  rewrite delta_0_deterministic in plus_real; auto.
59
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
60
  unfold evalBinop in *; simpl in *.
61 62 63 64
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H9 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in plus_real.
  rewrite (meps_0_deterministic (toRExp e2) H9 e2_real) in plus_real.
65 66 67
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion plus_float; subst.
  unfold perturb; simpl.
68 69 70 71
  inversion H13; subst; inversion H16; subst.
  unfold updEnv in H1, H15; simpl in *.
  symmetry in H1,H15.
  inversion H1; inversion H15; subst.
72
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
73
  clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
74 75 76
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
77
  unfold computeErrorR.
78
  pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta0))).
79
  destruct m;
80 81 82 83 84 85 86 87 88
    repeat rewrite Ropp_plus_distr; try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
  { repeat rewrite <- Rplus_assoc.
    assert (e1R + e2R + - e1F + - e2F = e1R + - e1F + e2R + - e2F)%R by lra.
    rewrite H1; clear H1.
    rewrite Rplus_assoc.
    eapply Rle_trans.
    apply Rabs_triang; apply Rplus_le_compat; try auto.
    rewrite Rplus_0_r.
    apply Rplus_le_compat; try auto. }
Heiko Becker's avatar
Heiko Becker committed
89 90 91 92 93 94
  Focus 4.
  eapply Rle_trans; [ apply Rabs_triang | rewrite (Rplus_assoc (Q2R err1)) ].
  apply Rplus_le_compat; try auto.
  eapply Rle_trans; [ apply Rabs_triang |].
  apply Rplus_le_compat; try auto.
  rewrite Rabs_Ropp; simpl. auto.
95 96 97 98 99 100 101
  all: eapply Rle_trans; try eapply H.
  all: setoid_rewrite Rplus_assoc at 2.
  all: eapply Rplus_le_compat; try auto.
  all: eapply Rle_trans; try eapply Rabs_triang.
  all: eapply Rplus_le_compat; try auto.
  all: rewrite Rabs_Ropp, Rabs_mult.
  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
102 103 104 105 106
Qed.

(**
  Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
107
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
108 109 110 111 112 113
      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e1)) e1R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e1) e1F m1 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e2)) e2R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e2) e2F m2 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
114
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
115
            (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
116 117 118
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
            DeltaMap
            (Binop Sub (Var R 1) (Var R 2)) vF m ->
Heiko Becker's avatar
Heiko Becker committed
119 120
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
121
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F - e2F) m)%R.
122
Proof.
Heiko Becker's avatar
Heiko Becker committed
123
  intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
124
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
125
  inversion sub_real; subst.
126 127
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
128
  subst; simpl in H3; auto.
129
  rewrite delta_0_deterministic in sub_real; auto.
130
  rewrite (delta_0_deterministic (evalBinop Sub v1 v2) REAL delta); auto.
131
  unfold evalBinop in *; simpl in *.
132 133 134 135
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H9 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in sub_real.
  rewrite (meps_0_deterministic (toRExp e2) H9 e2_real) in sub_real.
136 137 138
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion sub_float; subst.
  unfold perturb; simpl.
139 140 141 142
  inversion H13; subst; inversion H16; subst.
  unfold updEnv in H1,H15; simpl in *.
  symmetry in H1,H15.
  inversion H1; inversion H15; subst.
143
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
144
  clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H6 H1.
145 146 147
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  repeat rewrite Rsub_eq_Ropp_Rplus.
148 149
  unfold computeErrorR.
  pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
150
  destruct m;
151 152 153 154
    repeat rewrite Ropp_plus_distr; try rewrite Ropp_involutive;
      try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
  { repeat rewrite <- Rplus_assoc.
    assert (e1R + - e2R + - e1F + e2F = e1R + - e1F + - e2R + e2F)%R by lra.
155
    rewrite H1; clear H1.
156 157 158 159 160 161 162
    rewrite Rplus_assoc.
    eapply Rle_trans.
    apply Rabs_triang; apply Rplus_le_compat; try auto.
    rewrite Rplus_0_r.
    apply Rplus_le_compat; try auto.
    rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
    auto. }
Heiko Becker's avatar
Heiko Becker committed
163
  Focus 4.
164 165 166 167 168 169 170
    eapply Rle_trans.
    apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
    apply Rplus_le_compat; try auto.
    eapply Rle_trans.
    apply Rabs_triang.
    rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
    rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
Heiko Becker's avatar
Heiko Becker committed
171 172
    auto.

173 174 175 176 177 178 179 180
  all: eapply Rle_trans; try eapply Rabs_triang.
  all: setoid_rewrite Rplus_assoc at 2.
  all: eapply Rplus_le_compat; try auto.
  all: eapply Rle_trans; try eapply Rabs_triang.
  all: eapply Rplus_le_compat.
  all: try (rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym; auto; fail).
  all: rewrite Rabs_Ropp, Rabs_mult, <- Rsub_eq_Ropp_Rplus.
  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
181 182
Qed.

183
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
184 185 186 187 188 189
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e1)) e1R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e1) e1F m1 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e2)) e2R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e2) e2F m2 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
190
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
191
            (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
192 193 194
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
            DeltaMap
            (Binop Mult (Var R 1) (Var R 2)) vF m ->
195
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
196
Proof.
Heiko Becker's avatar
Heiko Becker committed
197
  intros e1_real e1_float e2_real e2_float mult_real mult_float.
198
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
199
  inversion mult_real; subst;
200 201
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
202
  subst; simpl in H3; auto.
203 204
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
205
  unfold evalBinop in *; simpl in *.
206 207 208 209
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H9 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in mult_real.
  rewrite (meps_0_deterministic (toRExp e2) H9 e2_real) in mult_real.
210 211 212
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion mult_float; subst.
  unfold perturb; simpl.
213 214 215 216
  inversion H13; subst; inversion H16; subst.
  unfold updEnv in H1,H15; simpl in *.
  symmetry in H1,H15.
  inversion H1; inversion H15; subst.
217
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
218
  clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
219 220 221
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
222
  unfold computeErrorR.
223
  destruct m.
224 225 226 227 228 229
  all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
  { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
  all: eapply Rle_trans; try apply Rabs_triang.
  all: try rewrite <- Rsub_eq_Ropp_Rplus, Rabs_Ropp; try rewrite Rabs_mult.
  all: eapply Rplus_le_compat_l; try auto.
  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
230 231
Qed.

232
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
233 234 235 236 237 238
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e1)) e1R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e1) e1F m1 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e2)) e2R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e2) e2F m2 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
239
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
240
            (updDefVars (Binop Div (Var R 1) (Var R 2)) m
241 242 243
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
            DeltaMap
            (Binop Div (Var R 1) (Var R 2)) vF m ->
244
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
245
Proof.
Heiko Becker's avatar
Heiko Becker committed
246
  intros e1_real e1_float e2_real e2_float div_real div_float.
247
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
248
  inversion div_real; subst;
249 250
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
251
  subst; simpl in H3; auto.
252 253
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
254
  unfold evalBinop in *; simpl in *.
255 256 257 258
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H9 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in div_real.
  rewrite (meps_0_deterministic (toRExp e2) H9 e2_real) in div_real.
259 260 261
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
262 263 264 265
  inversion H13; subst; inversion H16; subst.
  unfold updEnv in H1,H15; simpl in *.
  symmetry in H1,H15.
  inversion H1; inversion H15; subst.
266
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
267
  clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
268 269 270
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
271
  unfold computeErrorR.
272
  destruct m.
273 274 275 276 277 278
  all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
  { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
  all: eapply Rle_trans; try apply Rabs_triang.
  all: try rewrite <- Rsub_eq_Ropp_Rplus, Rabs_Ropp; try rewrite Rabs_mult.
  all: eapply Rplus_le_compat_l; try auto.
  all: eapply Rmult_le_compat_l; try auto using Rabs_pos.
279 280
Qed.

281 282
Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
      (e3:expr Q) (e3R:R) (e3F:R)
283 284 285 286 287 288 289 290 291
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e1)) e1R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e1) e1F m1->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e2)) e2R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e2) e2F m2 ->
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval (toRExp e3)) e3R REAL ->
  eval_expr E2 defVars DeltaMap (toRExp e3) e3F m3->
  eval_expr E1 (toRTMap defVars) DeltaMapR
            (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
292
  eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
293
            (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
294 295 296 297
                        (updDefVars (Var R 3) m3
                                    (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
            DeltaMap
            (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
298
  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
299
Proof.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
300 301
  intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
  inversion fma_real; subst;
302 303 304
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
305
  subst; simpl in H3; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
306 307 308
  rewrite delta_0_deterministic in fma_real; auto.
  rewrite delta_0_deterministic; auto.
  unfold evalFma in *; simpl in *.
309 310 311 312 313 314
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H9 e2_real);
    rewrite (meps_0_deterministic (toRExp e3) H10 e3_real).
  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in fma_real.
  rewrite (meps_0_deterministic (toRExp e2) H9 e2_real) in fma_real.
  rewrite (meps_0_deterministic (toRExp e3) H10 e3_real) in fma_real.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
315 316 317
  inversion fma_float; subst.
  unfold evalFma in *.
  unfold perturb; simpl.
318
  inversion H13; subst; inversion H16; subst; inversion H17; subst.
319
  cbn in *.
320 321
  inversion H0; inversion H1; inversion H14; inversion H15; inversion H18;
    inversion H19; subst.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
322 323 324 325
  clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
326
  unfold computeErrorR.
327
  destruct m; rewrite Ropp_plus_distr.
328
  { rewrite Rplus_0_r; hnf; right; f_equal; lra. }
Heiko Becker's avatar
Heiko Becker committed
329 330 331 332 333 334 335 336
  Focus 4.
  rewrite <- Rplus_assoc.
  eapply Rle_trans.
  eapply Rabs_triang.
  rewrite Rabs_Ropp.
  eapply Rplus_le_compat; try auto.
  hnf; right; f_equal; lra.

337 338 339 340 341 342 343 344 345 346 347 348 349
  all: repeat rewrite <- Rplus_assoc.
  all: setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
  all: repeat rewrite Rsub_eq_Ropp_Rplus.
  all: rewrite <- Rplus_assoc.
  all: setoid_rewrite Rplus_comm at 8.
  all: try rewrite <- Rplus_assoc.
  all: try setoid_rewrite Rplus_comm at 9.
  all: eapply Rle_trans; try eapply Rabs_triang.
  all: rewrite Rabs_Ropp.
  all: repeat rewrite Rplus_assoc.
  all: try rewrite <- Ropp_plus_distr.
  all: apply Rplus_le_compat_l.
  all: rewrite Rabs_mult; apply Rmult_le_compat_l; auto using Rabs_pos.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
350
Qed.
Heiko Becker's avatar
Heiko Becker committed
351

352
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
353 354 355
      (mEps m:mType) defVars DeltaMap:
  eval_expr E1 (toRTMap defVars) DeltaMapR (toREval e) nR REAL ->
  eval_expr E2 defVars DeltaMap e nF1 m ->
356
  eval_expr (updEnv 1 nF1 emptyEnv)
357
            (updDefVars (Downcast mEps (Var R 1)) mEps
358 359 360
                        (updDefVars (Var R 1) m defVars))
            DeltaMap
            (toRExp (Downcast mEps (Var Q 1))) nF mEps->
361 362 363 364 365 366 367 368 369 370 371
  (Rabs (nR - nF1) <= err)%R ->
  (Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.
Proof.
  intros eval_real eval_float eval_float_rnd err_bounded.
  replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra.
  eapply Rle_trans.
  apply (Rabs_triang (nR - nF1) (nF1 - nF)).
  apply (Rle_trans _ (err + Rabs (nF1 - nF))  _).
  - apply Rplus_le_compat_r; assumption.
  - apply Rplus_le_compat_l.
    inversion eval_float_rnd; subst.
372
    inversion H7; subst.
373 374
    inversion H0; subst.
    unfold perturb; simpl.
375
    unfold updEnv in H5; simpl in H5; inversion H5; subst.
376 377 378 379 380 381 382 383 384 385
    unfold computeErrorR.
    destruct mEps.
    { unfold Rminus. rewrite Rplus_opp_r, Rabs_R0; lra. }
    all: replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
    all: replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
    all: try rewrite Rabs_mult; try apply Rmult_le_compat_l; auto using Rabs_pos.
    unfold Rminus.
    rewrite Ropp_plus_distr, <- Rplus_assoc.
    rewrite Rplus_opp_r, Rplus_0_l, Rabs_Ropp; auto.
Qed.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
386

387 388 389 390 391 392 393 394
Lemma err_prop_inversion_pos_real nF nR err elo ehi
      (float_iv_pos : (0 < elo - err)%R)
      (real_iv_pos : (0 < elo)%R)
      (err_bounded : (Rabs (nR - nF) <= err)%R)
      (valid_bounds_e2 : (elo <= nR <= ehi)%R)
      (valid_bounds_e2_err : (elo - err <= nF <= ehi + err)%R)
      (err_pos : (0 <= err)%R):
  (Rabs (/nR - / nF) <= err * / ((elo - err) * (elo- err)))%R.
395
Proof.
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525
  rewrite Rabs_case_inverted in err_bounded.
  assert (0 < nF)%R as nF_pos by lra.
  destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]].
  - cut (0 < /nF - / nR)%R.
    + intros abs_neg.
      rewrite Rabs_left; try lra.
      rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive.
      rewrite Ropp_inv_permute; try lra.
      apply (Rle_trans _ (/ - nR + / (nR - err))).
      * apply Rplus_le_compat_l.
        apply Rinv_le_contravar; lra.
      * rewrite equal_naming_inv; try lra.
        assert (- nR + (nR - err) = - err)%R as simplify_up by lra.
        rewrite simplify_up.
        unfold Rdiv.
        repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute.
        {
          rewrite <- Ropp_mult_distr_r, Ropp_involutive.
          apply Rmult_le_compat_l; try lra.
          apply Rinv_le_contravar.
          - apply Rmult_0_lt_preserving; lra.
          - apply Rmult_le_compat; lra.
        }
        { assert (0 < nR * (nR - err))%R by (apply Rmult_0_lt_preserving; lra); lra. }
    + cut (/ nR < /nF)%R.
      * intros; lra.
      * apply Rinv_lt_contravar; try lra.
        apply Rmult_0_lt_preserving; lra.
  - cut (0 <= /nR - /nF)%R.
    + intros abs_pos.
      rewrite Rabs_right; try lra.
      rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded.
      rewrite Rsub_eq_Ropp_Rplus.
      apply (Rle_trans _ (/nR - / (nR + err))).
      * apply Rplus_le_compat_l.
        apply Ropp_le_contravar.
        apply Rinv_le_contravar; lra.
      * rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra.
        rewrite equal_naming_inv; try lra.
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
        unfold Rdiv.
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
          - apply Rmult_0_lt_preserving; lra.
          - apply Rmult_le_compat; lra.
        }
        { assert (0 < nR * (nR + err))%R by (apply Rmult_0_lt_preserving; lra); lra. }
    + cut (/nF <= /nR)%R.
      * intros; lra.
      * apply Rinv_le_contravar; try lra.
Qed.

Lemma err_prop_inversion_pos nF nR err (elo ehi:Q)
      (float_iv_pos : (Q2R 0 < Q2R (elo - err))%R)
      (real_iv_pos : (Q2R 0 < Q2R elo)%R)
      (err_bounded : (Rabs (nR - nF) <= Q2R err)%R)
      (valid_bounds_e2 : (Q2R elo <= nR <= Q2R ehi)%R)
      (valid_bounds_e2_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R)
      (err_pos : (0 <= Q2R err)%R):
  (Rabs (/nR - / nF) <= Q2R err * / ((Q2R elo- Q2R err) * (Q2R elo- Q2R err)))%R.
Proof.
  eapply err_prop_inversion_pos_real; try rewrite <- Q2R0_is_0; eauto.
  rewrite <- Q2R_minus; auto.
  rewrite Q2R0_is_0; auto.
Qed.

Lemma err_prop_inversion_neg_real nF nR err elo ehi
      (float_iv_neg : (ehi + err < 0)%R)
      (real_iv_neg : (ehi < 0)%R)
      (err_bounded : (Rabs (nR - nF) <= err)%R)
      (valid_bounds_e : (elo <= nR <= ehi)%R)
      (valid_bounds_e_err : (elo - err <= nF <= ehi + err)%R)
      (err_pos : (0 <= err)%R):
  (Rabs (/nR - / nF) <= err * / ((ehi + err) * (ehi + err)))%R.
Proof.
  rewrite Rabs_case_inverted in err_bounded.
  assert (nF < 0)%R as nF_neg by lra.
  destruct err_bounded as [ [diff_pos err_bounded] | [diff_neg err_bounded]].
  - cut (0 < /nF - / nR)%R.
    + intros abs_neg.
      rewrite Rabs_left; try lra.
      rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive.
      rewrite Ropp_inv_permute; try lra.
      apply (Rle_trans _ (/ - nR + / (nR - err))).
      * apply Rplus_le_compat_l.
        assert (0 < - nF)%R by lra.
        assert (0 < - (nR - err))%R by lra.
        assert (nR - err <= nF)%R as nR_lower by lra.
        apply Ropp_le_contravar in nR_lower.
        apply Rinv_le_contravar in nR_lower; try lra.
        repeat (rewrite <- Ropp_inv_permute in nR_lower; try lra).
      * rewrite equal_naming_inv; try lra.
        assert (- nR + (nR - err) = - err)%R as simplify_up by lra.
        rewrite simplify_up.
        unfold Rdiv.
        repeat(rewrite <- Ropp_mult_distr_l); rewrite <- Ropp_inv_permute.
        {
          rewrite <- Ropp_mult_distr_r, Ropp_involutive.
          apply Rmult_le_compat_l; try lra.
          apply Rinv_le_contravar.
          - apply Rmult_lt_0_inverting; lra.
          - eapply Rle_trans.
            eapply Rmult_le_compat_neg_l; try lra.
            instantiate (1 := (nR - err)%R); try lra.
            setoid_rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l; lra.
        }
        { assert (0 < nR * (nR - err))%R by (apply Rmult_lt_0_inverting; lra); lra. }
    + cut (/ nR < /nF)%R.
      * intros; lra.
      * apply Rinv_lt_contravar; try lra.
        apply Rmult_lt_0_inverting; lra.
  - cut (0 <= /nR - /nF)%R.
    + intros abs_pos.
      rewrite Rabs_right; try lra.
      rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr, Ropp_involutive in err_bounded.
      rewrite Rsub_eq_Ropp_Rplus.
      apply (Rle_trans _ (/nR - / (nR + err))).
      * apply Rplus_le_compat_l.
        apply Ropp_le_contravar.
        assert (0 < - nF)%R by lra.
        assert (0 < - (nR + err))%R by lra.
        assert (nF <= nR + err)%R as nR_upper by lra.
        apply Ropp_le_contravar in nR_upper.
        apply Rinv_le_contravar in nR_upper; try lra.
        repeat (rewrite <- Ropp_inv_permute in nR_upper; try lra).
      * rewrite Rsub_eq_Ropp_Rplus, Ropp_inv_permute; try lra.
526
        rewrite equal_naming_inv; try lra.
527 528
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
529
        unfold Rdiv.
530
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
531 532 533
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
534 535 536 537 538 539 540 541 542 543 544 545 546 547
          - apply Rmult_lt_0_inverting; lra.
          - eapply Rle_trans.
            eapply Rmult_le_compat_neg_l; try lra.
            instantiate (1:= (nR + err)%R); try lra.
            setoid_rewrite Rmult_comm.
            eapply Rmult_le_compat_neg_l; lra.
        }
        { assert (0 < nR * (nR + err))%R by (apply Rmult_lt_0_inverting; lra); lra. }
    + cut (/nF <= /nR)%R.
      * intros; lra.
      * assert (nR <= nF)%R by lra.
        assert (- nF <= - nR)%R as le_inv by lra.
        apply Rinv_le_contravar in le_inv; try lra.
        repeat (rewrite <- Ropp_inv_permute in le_inv; try lra).
548 549
Qed.

550 551 552 553 554 555 556 557
Lemma err_prop_inversion_neg nF nR err (elo ehi:Q)
      (float_iv_neg : (Q2R (ehi + err) < Q2R 0)%R)
      (real_iv_neg : (Q2R ehi < Q2R 0)%R)
      (err_bounded : (Rabs (nR - nF) <= Q2R err)%R)
      (valid_bounds_e : (Q2R elo <= nR <= Q2R ehi)%R)
      (valid_bounds_e_err : (Q2R elo - Q2R err <= nF <= Q2R ehi + Q2R err)%R)
      (err_pos : (0 <= Q2R err)%R):
  (Rabs (/nR - / nF) <= Q2R err * / ((Q2R ehi + Q2R err) * (Q2R ehi + Q2R err)))%R.
558
Proof.
559 560 561 562 563
  eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
  rewrite <- Q2R_plus ; auto.
  apply valid_bounds_e.
  auto.
Qed.