ErrorBounds.v 24.5 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
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
15
  eval_expr E1 (toRTMap defVars) (Const REAL n) nR REAL ->
16
  eval_expr E2 defVars (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
      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
38
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
39
  eval_expr E2 defVars (toRExp e1) e1F m1->
40
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
41
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
42
  eval_expr E1 (toRTMap defVars) (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)))
='s avatar
= committed
46
           (Binop Plus (Var R 1) (Var R 2)) vF m ->
Heiko Becker's avatar
Heiko Becker committed
47 48
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
49
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F + e2F) m)%R.
50
Proof.
Heiko Becker's avatar
Heiko Becker committed
51
  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
52 53
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion plus_real; subst.
54 55
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
56
  subst; simpl in H3; auto.
57
  rewrite delta_0_deterministic in plus_real; auto.
58
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
59
  unfold evalBinop in *; simpl in *.
60 61 62 63
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H8 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
  rewrite (meps_0_deterministic (toRExp e2) H8 e2_real) in plus_real.
64 65 66
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion plus_float; subst.
  unfold perturb; simpl.
67 68 69 70
  inversion H11; subst; inversion H14; subst.
  unfold updEnv in H1, H13; simpl in *.
  symmetry in H1,H13.
  inversion H1; inversion H13; subst.
71
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
72
  clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
73 74 75
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
76
  unfold computeErrorR.
77
  pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta0))).
78
  destruct m;
79 80 81 82 83 84 85 86 87
    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
88 89 90 91 92 93
  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.
94 95 96 97 98 99 100
  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.
101 102 103 104 105
Qed.

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

171 172 173 174 175 176 177 178
  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.
179 180
Qed.

181
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
182
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
183
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
184
  eval_expr E2 defVars (toRExp e1) e1F m1 ->
185
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
186
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
187
  eval_expr E1 (toRTMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
188
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
189 190
            (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
           (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
='s avatar
= committed
191
           (Binop Mult (Var R 1) (Var R 2)) vF m ->
192
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
193
Proof.
194 195 196
  admit.
Admitted.
(*
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 210
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in mult_real.
  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in mult_real.
  clear H3 H4.
211 212 213
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion mult_float; subst.
  unfold perturb; simpl.
214
  inversion H4; subst; inversion H6; subst.
215
    unfold updEnv in *; simpl in *.
216 217
    inversion H1; inversion H11; subst.
    cbn in *. inversion H0; inversion H10; subst.
218
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
219
  clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
220 221 222
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
223
  unfold computeErrorR.
224
  destruct m.
225 226 227 228 229 230
  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.
231
Qed.
232
 *)
233

234
Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
235
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
236
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
237
  eval_expr E2 defVars (toRExp e1) e1F m1 ->
238
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
239
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
240
  eval_expr E1 (toRTMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
241
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
242 243
            (updDefVars (Binop Div (Var R 1) (Var R 2)) m
           (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
='s avatar
= committed
244
           (Binop Div (Var R 1) (Var R 2)) vF m ->
245
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
246
Proof.
247 248 249
  admit.
Admitted.
(*
Heiko Becker's avatar
Heiko Becker committed
250
  intros e1_real e1_float e2_real e2_float div_real div_float.
251
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
252
  inversion div_real; subst;
253 254
  assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
255
  subst; simpl in H3; auto.
256 257
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
258
  unfold evalBinop in *; simpl in *.
259 260 261 262 263
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in div_real.
  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in div_real.
  clear H3 H4.
264 265 266
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
267
  inversion H4; subst; inversion H6; subst.
268
    unfold updEnv in *; simpl in *.
269 270
    inversion H1; inversion H11; subst.
    cbn in *. inversion H0; inversion H10; subst.
271
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
272
  clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
273 274 275
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
276
  unfold computeErrorR.
277
  destruct m.
278 279 280 281 282 283
  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.
284
Qed.
285
 *)
286

287 288
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)
289
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
290
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e1)) e1R REAL ->
291
  eval_expr E2 defVars (toRExp e1) e1F m1->
292
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e2)) e2R REAL ->
293
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
294
  eval_expr E1 (toRTMap defVars) (toREval (toRExp e3)) e3R REAL ->
295
  eval_expr E2 defVars (toRExp e3) e3F m3->
296
  eval_expr E1 (toRTMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
297
  eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
298 299
            (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
           (updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
Nikita Zyuzin's avatar
Nikita Zyuzin committed
300
           (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
301
  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
302
Proof.
303 304 305
  admit.
Admitted.
(*
Nikita Zyuzin's avatar
Nikita Zyuzin committed
306 307
  intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
  inversion fma_real; subst;
308 309 310
  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).
311
  subst; simpl in H3; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
312 313 314
  rewrite delta_0_deterministic in fma_real; auto.
  rewrite delta_0_deterministic; auto.
  unfold evalFma in *; simpl in *.
315 316 317 318 319 320 321 322
  clear delta H2.
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real);
    rewrite (meps_0_deterministic (toRExp e3) H5 e3_real).
  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in fma_real.
  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in fma_real.
  rewrite (meps_0_deterministic (toRExp e3) H5 e3_real) in fma_real.
  clear H3 H4 H5 v1 v2 v3.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
323 324 325
  inversion fma_float; subst.
  unfold evalFma in *.
  unfold perturb; simpl.
326 327 328
  inversion H3; subst; inversion H4; subst; inversion H5; subst.
  cbn in *.
  inversion H0; inversion H1; inversion H6; inversion H7; inversion H12; inversion H13; subst.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
329 330 331 332
  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.
333
  unfold computeErrorR.
334
  destruct m; rewrite Ropp_plus_distr.
335
  { rewrite Rplus_0_r; hnf; right; f_equal; lra. }
Heiko Becker's avatar
Heiko Becker committed
336 337 338 339 340 341 342 343
  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.

344 345 346 347 348 349 350 351 352 353 354 355 356
  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
357
Qed.
358
 *)
Heiko Becker's avatar
Heiko Becker committed
359

360
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
361
      (mEps m:mType) defVars:
362
  eval_expr E1 (toRTMap defVars) (toREval e) nR REAL ->
363
  eval_expr E2 defVars e nF1 m ->
364
  eval_expr (updEnv 1 nF1 emptyEnv)
365
           (updDefVars (Var R 1) m defVars)
366 367 368 369
           (toRExp (Downcast mEps (Var Q 1))) nF mEps->
  (Rabs (nR - nF1) <= err)%R ->
  (Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.
Proof.
370 371 372 373
  admit.
Admitted.

(*
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
  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.
    inversion H5; subst.
    inversion H0; subst.
    unfold perturb; simpl.
    unfold updEnv in H3; simpl in H3; inversion H3; subst.
    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.
396
 *)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
397

398 399 400 401 402 403 404 405
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.
406
Proof.
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 526 527 528 529 530 531 532 533 534 535 536
  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.
537
        rewrite equal_naming_inv; try lra.
538 539
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
540
        unfold Rdiv.
541
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
542 543 544
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
545 546 547 548 549 550 551 552 553 554 555 556 557 558
          - 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).
559 560
Qed.

561 562 563 564 565 566 567 568
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.
569
Proof.
570 571 572 573 574
  eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
  rewrite <- Q2R_plus ; auto.
  apply valid_bounds_e.
  auto.
Qed.