ErrorBounds.v 16.9 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.
7
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
Heiko Becker's avatar
Heiko Becker committed
8

9
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R):
10
  forall cenv:nat -> R,
11
12
  eval_exp 0%R cenv P (Const n) nR ->
  eval_exp (Q2R machineEpsilon) cenv P (Const n) nF ->
13
  (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
14
15
16
Proof.
  intros cenv eval_real eval_float.
  inversion eval_real; subst.
17
  rewrite delta_0_deterministic; auto.
18
19
  inversion eval_float; subst.
  unfold perturb; simpl.
20
  rewrite Rabs_err_simpl, Rabs_mult.
21
22
23
  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.

24
25
26
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (cenv:nat->R):
  eval_exp 0%R cenv P (Param R n) nR ->
  eval_exp (Q2R machineEpsilon) cenv P (Param R n) nF ->
27
  (Rabs (nR - nF) <= Rabs (cenv n) * (Q2R machineEpsilon))%R.
28
29
30
Proof.
  intros eval_real eval_float.
  inversion eval_real; subst.
31
  rewrite delta_0_deterministic; auto.
32
33
34
35
36
37
38
  inversion eval_float; subst.
  unfold perturb; simpl.
  rewrite Rabs_err_simpl.
  repeat rewrite Rabs_mult.
  apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Qed.

39
40
41
42
43
44
45
Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (P:precond) (err1:R) (err2:R):
  eval_exp 0%R cenv P e1 e1R ->
  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
  eval_exp 0%R cenv P e2 e2R ->
  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
  eval_exp 0%R cenv P (Binop Plus e1 e2) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Plus (Var R 1) (Var R 2)) vF ->
46
47
  (Rabs (e1R - e1F) <= err1)%R ->
  (Rabs (e2R - e2F) <= err2)%R ->
48
  (Rabs (vR - vF) <= err1 + err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
49
50
51
52
Proof.
  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion plus_real; subst.
53
  rewrite delta_0_deterministic in plus_real; auto.
54
55
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
  unfold evalBinop in *; simpl in *.
56
  clear delta H2.
57
58
59
60
  rewrite (meps_0_deterministic H4 e1_real);
    rewrite (meps_0_deterministic H5 e2_real).
  rewrite (meps_0_deterministic H4 e1_real) in plus_real.
  rewrite (meps_0_deterministic H5 e2_real) in plus_real.
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
  clear H4 H5 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion plus_float; subst.
  unfold perturb; simpl.
  inversion H4; subst; inversion H5; subst.
  unfold updEnv; simpl.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float.
  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))).
  pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
  eapply Rle_trans.
  apply H1.
  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.
    apply H2.
    apply Req_le; auto.
Qed.

(**
  Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
98
99
100
101
102
103
104
Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) P (err1:R) (err2:R):
  eval_exp 0%R cenv P e1 e1R ->
  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
  eval_exp 0%R cenv P e2 e2R ->
  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
  eval_exp 0%R cenv P (Binop Sub e1 e2) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Sub (Var R 1) (Var R 2)) vF ->
105
106
  (Rabs (e1R - e1F) <= err1)%R ->
  (Rabs (e2R - e2F) <= err2)%R ->
107
  (Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
108
109
110
111
Proof.
  intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion sub_real; subst.
112
113
  rewrite delta_0_deterministic in sub_real; auto.
  rewrite delta_0_deterministic; auto.
114
  unfold evalBinop in *; simpl in *.
115
  clear delta H2.
116
117
118
119
  rewrite (meps_0_deterministic H4 e1_real);
    rewrite (meps_0_deterministic H5 e2_real).
  rewrite (meps_0_deterministic H4 e1_real) in sub_real.
  rewrite (meps_0_deterministic H5 e2_real) in sub_real.
120
121
122
123
124
125
126
127
128
129
130
131
132
  clear H4 H5 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion sub_float; subst.
  unfold perturb; simpl.
  inversion H4; subst; inversion H5; subst.
  unfold updEnv; simpl.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
  clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  repeat rewrite Rsub_eq_Ropp_Rplus.
  repeat rewrite Ropp_plus_distr.
  rewrite plus_bounds_simplify.
133
  rewrite Ropp_involutive.
134
135
  rewrite Rplus_assoc.
  eapply Rle_trans.
136
  apply Rabs_triang.
137
  eapply Rle_trans.
138
139
  eapply Rplus_le_compat_l.
  apply Rabs_triang.
140
  rewrite <- Rplus_assoc.
141
  setoid_rewrite Rplus_comm at 4.
142
143
  repeat rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite Rabs_Ropp.
144
145
146
147
  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].
148
149
Qed.

150
151
152
153
154
155
156
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (P:precond) (err1:R) (err2:R):
  eval_exp 0%R cenv P e1 e1R ->
  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
  eval_exp 0%R cenv P e2 e2R ->
  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
  eval_exp 0%R cenv P (Binop Mult e1 e2) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Mult (Var R 1) (Var R 2)) vF ->
157
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
158
Proof.
159
160
  intros e1_real e1_float e2_real e2_float mult_real mult_float.
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
161
  inversion mult_real; subst.
162
163
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
164
  unfold evalBinop in *; simpl in *.
165
  clear delta H2.
166
167
168
169
  rewrite (meps_0_deterministic H4 e1_real);
    rewrite (meps_0_deterministic H5 e2_real).
  rewrite (meps_0_deterministic H4 e1_real) in mult_real.
  rewrite (meps_0_deterministic H5 e2_real) in mult_real.
170
171
172
173
174
175
176
177
178
179
180
181
  clear H4 H5 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion mult_float; subst.
  unfold perturb; simpl.
  inversion H4; subst; inversion H5; subst.
  unfold updEnv; simpl.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
  clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Ropp_plus_distr.
Heiko Becker's avatar
Heiko Becker committed
182
183
  rewrite <- Rplus_assoc.
  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
184
185
186
  eapply Rle_trans.
  eapply Rabs_triang.
  eapply Rplus_le_compat_l.
Heiko Becker's avatar
Heiko Becker committed
187
  rewrite Rabs_Ropp.
188
  repeat rewrite Rabs_mult.
Heiko Becker's avatar
Heiko Becker committed
189
  eapply Rmult_le_compat_l; auto.
190
191
  rewrite <- Rabs_mult.
  apply Rabs_pos.
192
193
Qed.

194
195
196
197
198
199
200
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (P:precond) (err1:R) (err2:R):
  eval_exp 0%R cenv P e1 e1R ->
  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
  eval_exp 0%R cenv P e2 e2R ->
  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
  eval_exp 0%R cenv P (Binop Div e1 e2) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Div (Var R 1) (Var R 2)) vF ->
201
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
202
203
204
205
Proof.
  intros e1_real e1_float e2_real e2_float div_real div_float.
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
  inversion div_real; subst.
206
207
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
208
  unfold evalBinop in *; simpl in *.
209
  clear delta H2.
210
211
212
213
  rewrite (meps_0_deterministic H4 e1_real);
    rewrite (meps_0_deterministic H5 e2_real).
  rewrite (meps_0_deterministic H4 e1_real) in div_real.
  rewrite (meps_0_deterministic H5 e2_real) in div_real.
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
  clear H4 H5 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
  inversion H4; subst; inversion H5; subst.
  unfold updEnv; simpl.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
  clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float.
  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.
235
236
Qed.

237
238
239
240
241
242
243
244
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.
245
Proof.
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
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
327
328
329
330
331
332
333
334
335
336
337
338
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
  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.
376
        rewrite equal_naming_inv; try lra.
377
378
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
379
        unfold Rdiv.
380
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
381
382
383
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
384
385
386
387
388
389
390
391
392
393
394
395
396
397
          - 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).
398
399
Qed.

400
401
402
403
404
405
406
407
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.
408
Proof.
409
410
411
412
413
414
  eapply err_prop_inversion_neg_real; try rewrite <- Q2R0_is_0; try lra.
  rewrite <- Q2R_plus ; auto.
  apply valid_bounds_e.
  auto.
  rewrite Q2R0_is_0; auto.
Qed.