ErrorBounds.v 24.3 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
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
7
8
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Heiko Becker's avatar
Heiko Becker committed
9

='s avatar
= committed
10
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
11
  eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
12
  eval_expr E2 defVars (Const m n) nF m ->
13
  (Rabs (nR - nF) <= computeErrorR n m)%R.
14
Proof.
Heiko Becker's avatar
Heiko Becker committed
15
  intros eval_real eval_float.
16
  inversion eval_real; subst.
17
  rewrite delta_0_deterministic; auto.
18
19
  inversion eval_float; subst.
  unfold perturb; simpl.
20
21
22
23
24
25
26
27
28
29
  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.
30
31
Qed.

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

(**
  Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
105
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
106
      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
107
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
108
  eval_expr E2 defVars (toRExp e1) e1F m1 ->
109
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
110
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
111
  eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
112
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
='s avatar
= committed
113
114
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Sub (Var R 1) (Var R 2)) vF m ->
Heiko Becker's avatar
Heiko Becker committed
115
116
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
117
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + computeErrorR (e1F - e2F) m)%R.
118
Proof.
Heiko Becker's avatar
Heiko Becker committed
119
  intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
120
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
121
  inversion sub_real; subst;
122
123
  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
124
  subst; simpl in H3; auto.
125
126
  rewrite delta_0_deterministic in sub_real; auto.
  rewrite delta_0_deterministic; auto.
127
  unfold evalBinop in *; simpl in *.
128
  clear delta H3.
129
130
131
132
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real.
133
  clear H5 H6 H7 v1 v2.
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
  inversion H4; subst; inversion H7; subst.
138
  unfold updEnv; simpl.
139
140
141
142
  simpl in H0; simpl in H5; inversion H0; inversion H5; subst; clear H0 H5.
  symmetry in H6, H1.
  unfold updEnv in H6, H1; simpl in H6, H1.
  inversion H6; inversion H1; 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 H1 H6.
145
146
147
148
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  repeat rewrite Rsub_eq_Ropp_Rplus.
  repeat rewrite Ropp_plus_distr.
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
  unfold computeErrorR.
  pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
  destruct (join m0 m3);
    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.
    rewrite H0; clear H0.
    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. }
  Focus 4.
    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.
    auto.
  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
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
185
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
186
  eval_expr E2 defVars (toRExp e1) e1F m1 ->
187
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
188
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
189
  eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
190
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
='s avatar
= committed
191
192
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Mult (Var R 1) (Var R 2)) vF m ->
193
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
194
Proof.
Heiko Becker's avatar
Heiko Becker committed
195
  intros e1_real e1_float e2_real e2_float mult_real mult_float.
196
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
197
  inversion mult_real; subst;
198
199
  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
200
  subst; simpl in H3; auto.
201
202
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
203
  unfold evalBinop in *; simpl in *.
204
  clear delta H3.
205
206
207
208
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real.
  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real.
209
  clear H5 H6 v1 v2 H7 H2.
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
  inversion H3; subst; inversion H6; subst.
214
    unfold updEnv in *; simpl in *.
215
216
    inversion H6; inversion H1; subst.
    simpl in H8; simpl in H9; intros; inversion H5; 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
223
224
225
226
227
228
229
  unfold computeErrorR.
  destruct (join m0 m3).
  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
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
234
  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
235
  eval_expr E2 defVars (toRExp e1) e1F m1 ->
236
  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
237
  eval_expr E2 defVars (toRExp e2) e2F m2 ->
238
  eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
239
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
='s avatar
= committed
240
241
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Div (Var R 1) (Var R 2)) vF m ->
242
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
243
Proof.
Heiko Becker's avatar
Heiko Becker committed
244
  intros e1_real e1_float e2_real e2_float div_real div_float.
245
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
246
  inversion div_real; subst;
247
248
  assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
  assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
249
  subst; simpl in H3; auto.
250
251
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
252
  unfold evalBinop in *; simpl in *.
253
  clear delta H3 H2.
254
255
256
257
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in div_real.
  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in div_real.
258
  (* clear H5 H6 v1 v2. *)
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
  inversion H3; subst; inversion H9; subst.
263
    unfold updEnv in *; simpl in *.
264
    inversion H8; inversion H1; subst.
265
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
266
  clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
267
268
269
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
270
271
272
273
274
275
276
277
  unfold computeErrorR.
  destruct (join m0 m3).
  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.
278
279
Qed.

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

347
Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (mEps m:mType) defVars:
348
  eval_expr E1 (toRMap defVars) (toREval e) nR REAL ->
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
  eval_expr E2 defVars e nF1 m ->
  eval_expr (updEnv 1 nF1 emptyEnv)
           (updDefVars 1 m defVars)
           (toRExp (Downcast mEps (Var Q 1))) nF mEps->
  (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.
    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.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
378

379
380
381
382
383
384
385
386
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.
387
Proof.
388
389
390
391
392
393
394
395
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
  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.
518
        rewrite equal_naming_inv; try lra.
519
520
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
521
        unfold Rdiv.
522
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
523
524
525
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
526
527
528
529
530
531
532
533
534
535
536
537
538
539
          - 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).
540
541
Qed.

542
543
544
545
546
547
548
549
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.
550
Proof.
551
552
553
554
555
  eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
  rewrite <- Q2R_plus ; auto.
  apply valid_bounds_e.
  auto.
Qed.