ErrorBounds.v 22.4 KB
Newer Older
1
(**
Heiko Becker's avatar
Heiko Becker committed
2
3
Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
4
Bounds are explained in section 5, Deriving Computable Error Bounds
5
**)
6
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Heiko Becker's avatar
Heiko Becker committed
7
8
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
Heiko Becker's avatar
Heiko Becker committed
9

='s avatar
= committed
10
11

Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
12
  eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 ->
13
  eval_exp E2 defVars (Const m n) nF m ->
14
  (Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R.
15
Proof.
Heiko Becker's avatar
Heiko Becker committed
16
  intros eval_real eval_float.
17
  inversion eval_real; subst.
18
  rewrite delta_0_deterministic; auto.
19
20
  inversion eval_float; subst.
  unfold perturb; simpl.
21
  rewrite Rabs_err_simpl, Rabs_mult.
22
  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
23
  simpl (mTypeToQ M0) in *.
24
  apply (Rle_trans _ (Q2R 0) _); try auto.
25
  rewrite Q2R0_is_0; lra.
26
27
Qed.

28

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

(**
  Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
97
Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
98
      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
99
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
100
  eval_exp E2 defVars (toRExp e1) e1F m1 ->
101
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
102
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
103
  eval_exp E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
='s avatar
= committed
104
105
106
  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Sub (Var R 1) (Var R 2)) vF m ->
Heiko Becker's avatar
Heiko Becker committed
107
108
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
109
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (mTypeToQ m))))%R.
110
Proof.
Heiko Becker's avatar
Heiko Becker committed
111
  intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
112
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
113
  inversion sub_real; subst;
114
115
116
  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
117
118
  rewrite delta_0_deterministic in sub_real; auto.
  rewrite delta_0_deterministic; auto.
119
  unfold evalBinop in *; simpl in *.
120
  clear delta H3.
121
122
123
124
  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.
125
  clear H5 H6 H7 v1 v2.
126
127
128
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion sub_float; subst.
  unfold perturb; simpl.
129
  inversion H4; subst; inversion H7; subst.
130
  unfold updEnv; simpl.
131
132
133
134
  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.
135
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
136
  clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H1 H6.
137
138
139
140
141
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  repeat rewrite Rsub_eq_Ropp_Rplus.
  repeat rewrite Ropp_plus_distr.
  rewrite plus_bounds_simplify.
142
  rewrite Ropp_involutive.
143
144
  rewrite Rplus_assoc.
  eapply Rle_trans.
145
  apply Rabs_triang.
146
  eapply Rle_trans.
147
148
  eapply Rplus_le_compat_l.
  apply Rabs_triang.
149
  rewrite <- Rplus_assoc.
150
  setoid_rewrite Rplus_comm at 4.
151
152
  repeat rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite Rabs_Ropp.
153
154
155
156
  rewrite Rabs_minus_sym in bound_e2.
  apply Rplus_le_compat; [apply Rplus_le_compat; auto | ].
  rewrite Rabs_mult.
  eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
157
158
Qed.

159
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
160
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
161
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
162
  eval_exp E2 defVars (toRExp e1) e1F m1 ->
163
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
164
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
165
  eval_exp E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
='s avatar
= committed
166
167
168
  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Mult (Var R 1) (Var R 2)) vF m ->
169
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ m)))%R.
170
Proof.
Heiko Becker's avatar
Heiko Becker committed
171
  intros e1_real e1_float e2_real e2_float mult_real mult_float.
172
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
173
  inversion mult_real; subst;
174
175
176
  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
177
178
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
179
  unfold evalBinop in *; simpl in *.
180
  clear delta H3.
181
182
183
184
  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.
185
  clear H5 H6 v1 v2 H7 H2.
186
187
188
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion mult_float; subst.
  unfold perturb; simpl.
189
  inversion H3; subst; inversion H6; subst.
190
    unfold updEnv in *; simpl in *.
191
192
    inversion H6; inversion H1; subst.
    simpl in H8; simpl in H9; intros; inversion H5; subst.
193
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
194
  clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
195
196
197
198
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Ropp_plus_distr.
Heiko Becker's avatar
Heiko Becker committed
199
200
  rewrite <- Rplus_assoc.
  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
201
202
203
  eapply Rle_trans.
  eapply Rabs_triang.
  eapply Rplus_le_compat_l.
Heiko Becker's avatar
Heiko Becker committed
204
  rewrite Rabs_Ropp.
205
  repeat rewrite Rabs_mult.
Heiko Becker's avatar
Heiko Becker committed
206
  eapply Rmult_le_compat_l; auto.
207
208
  rewrite <- Rabs_mult.
  apply Rabs_pos.
209
210
Qed.

211
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
212
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
213
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
214
  eval_exp E2 defVars (toRExp e1) e1F m1 ->
215
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
216
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
217
  eval_exp E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
='s avatar
= committed
218
219
220
  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
           (updDefVars 2 m2 (updDefVars 1 m1 defVars))
           (Binop Div (Var R 1) (Var R 2)) vF m ->
221
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ m)))%R.
222
Proof.
Heiko Becker's avatar
Heiko Becker committed
223
  intros e1_real e1_float e2_real e2_float div_real div_float.
224
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
225
  inversion div_real; subst;
226
227
228
  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
  assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
229
230
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
231
  unfold evalBinop in *; simpl in *.
232
  clear delta H3 H2.
233
234
235
236
  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.
237
  (* clear H5 H6 v1 v2. *)
238
239
240
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
241
  inversion H3; subst; inversion H9; subst.
242
    unfold updEnv in *; simpl in *.
243
    inversion H8; inversion H1; subst.
244
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
245
  clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
246
247
248
249
250
251
252
253
254
255
256
257
258
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Ropp_plus_distr.
  rewrite <- Rplus_assoc.
  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
  eapply Rle_trans.
  eapply Rabs_triang.
  eapply Rplus_le_compat_l.
  rewrite Rabs_Ropp.
  repeat rewrite Rabs_mult.
  eapply Rmult_le_compat_l; auto.
  apply Rabs_pos.
259
260
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
261
262
Lemma fma_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
      (e3:exp Q) (e3R:R) (e3F:R)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
263
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
Nikita Zyuzin's avatar
Nikita Zyuzin committed
264
265
266
267
268
  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
  eval_exp E2 defVars (toRExp e1) e1F m1->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
  eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
269
  eval_exp E2 defVars (toRExp e3) e3F m3->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
270
  eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
271
  eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
Nikita Zyuzin's avatar
Nikita Zyuzin committed
272
273
           (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
           (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
274
  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
275
Proof.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
  intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
  inversion fma_real; subst;
  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
  assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
  assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
  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.
  rewrite Ropp_plus_distr.
  rewrite <- Rplus_assoc.
  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite <- Rplus_assoc.
  setoid_rewrite Rplus_comm at 8.
  rewrite <- Rplus_assoc.
  setoid_rewrite Rplus_comm at 9.
  rewrite Rplus_assoc.
  setoid_rewrite Rplus_assoc at 2.
  rewrite <- Rplus_assoc.
  rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite <- Ropp_plus_distr.
  rewrite <- Rsub_eq_Ropp_Rplus.
  eapply Rle_trans.
  eapply Rabs_triang.
  eapply Rplus_le_compat_l.
  rewrite Rabs_Ropp.
  repeat rewrite Rabs_mult.
  eapply Rmult_le_compat_l; auto.
  apply Rabs_pos.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
327
Qed.
Heiko Becker's avatar
Heiko Becker committed
328

Nikita Zyuzin's avatar
Nikita Zyuzin committed
329

330
331
332
333
334
335
336
337
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.
338
Proof.
339
340
341
342
343
344
345
346
347
348
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
378
379
380
381
382
383
384
385
386
387
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
  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.
469
        rewrite equal_naming_inv; try lra.
470
471
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
472
        unfold Rdiv.
473
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
474
475
476
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
477
478
479
480
481
482
483
484
485
486
487
488
489
490
          - 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).
491
492
Qed.

493
494
495
496
497
498
499
500
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.
501
Proof.
502
503
504
505
506
  eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
  rewrite <- Q2R_plus ; auto.
  apply valid_bounds_e.
  auto.
Qed.
507

508
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
509
  eval_exp E1 (toRMap defVars) (toREval e) nR M0 ->
510
  eval_exp E2 defVars e nF1 m ->
='s avatar
= committed
511
512
513
  eval_exp (updEnv 1 nF1 emptyEnv)
           (updDefVars 1 m defVars)
           (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
514
  (Rabs (nR - nF1) <= err)%R ->
515
  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (mTypeToQ machineEpsilon))%R.
516
517
518
519
520
521
522
523
524
525
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.
526
    inversion H0; subst.
527
    unfold perturb; simpl.
528
    unfold updEnv in H3; simpl in H3; inversion H3; subst.
529
530
531
532
533
    replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra.
    replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp).
    rewrite Rabs_mult.
    apply Rmult_le_compat_l.
    + apply Rabs_pos.
='s avatar
= committed
534
    + auto.
535
Qed.