ErrorBounds.v 20 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

10
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars:
11
  eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 ->
12
  eval_exp E2 defVars (Const m n) nF m ->
13
  (Rabs (nR - nF) <= Rabs n * (Q2R (meps 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
  rewrite Rabs_err_simpl, Rabs_mult.
21
  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
22 23
  simpl (meps M0) in *.
  apply (Rle_trans _ (Q2R 0) _); try auto.
24
  rewrite Q2R0_is_0; lra.
25 26
Qed.

27 28 29 30 31
(*
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
  eval_exp 0%R E1 P (Param R n) nR ->
  eval_exp (Q2R machineEpsilon) E2 P (Param R n) nF ->
  (Rabs (nR - nF) <=  * (Q2R machineEpsilon))%R.
32
Proof.
Heiko Becker's avatar
Heiko Becker committed
33
  intros eval_real eval_float.
34
  inversion eval_real; subst.
35
  rewrite delta_0_deterministic; auto.
36 37
  inversion eval_float; subst.
  unfold perturb; simpl.
38 39
  exists v; split; try auto.
  rewrite H3 in H8; inversion H8.
40 41 42 43
  rewrite Rabs_err_simpl.
  repeat rewrite Rabs_mult.
  apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Qed.
44
*)
45

46
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
47
      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
48
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
49
  eval_exp E2 defVars (toRExp e1) e1F m1->
50
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
51
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
52 53
  eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Plus (Var R 1) (Var R 2)) vF m->
Heiko Becker's avatar
Heiko Becker committed
54 55
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
56
  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
57
Proof.
Heiko Becker's avatar
Heiko Becker committed
58
  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
59 60
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion plus_real; subst.
61
  destruct m0; destruct m3; inversion H2;
62
      simpl in H3; rewrite Q2R0_is_0 in H3; auto.
63
  rewrite delta_0_deterministic in plus_real; auto.
64 65
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
  unfold evalBinop in *; simpl in *.
66
  clear delta H3.
67 68 69 70
  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.
71
  clear H5 H6 H7 v1 v2.
72 73 74
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion plus_float; subst.
  unfold perturb; simpl.
75
  inversion H4; subst; inversion H7; subst.
76
  unfold updEnv; simpl.
77 78 79
  unfold updEnv in H1,H6; simpl in *.
  symmetry in H1,H6.
  inversion H1; inversion H6; subst.
80
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
81
  clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
82 83 84 85 86 87 88 89 90 91
  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))).
92
  pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H1).
93
  eapply Rle_trans.
94
  apply H4.
95 96 97 98 99 100 101 102 103
  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.
104
    apply H3.
105 106 107 108 109 110
    apply Req_le; auto.
Qed.

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

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

219
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
220
      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
221
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
222
  eval_exp E2 defVars (toRExp e1) e1F m1 ->
223
  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
224
  eval_exp E2 defVars (toRExp e2) e2F m2 ->
225 226
  eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Div (Var R 1) (Var R 2)) vF m ->
227
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
228
Proof.
Heiko Becker's avatar
Heiko Becker committed
229
  intros e1_real e1_float e2_real e2_float div_real div_float.
230
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
231
  inversion div_real; subst;
232
  destruct m0; destruct m3; inversion H2;
233
    simpl in H3; rewrite Q2R0_is_0 in H3; auto.
234 235
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
236
  unfold evalBinop in *; simpl in *.
237
  clear delta H3 H2.
238 239 240 241
  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.
242
  (* clear H5 H6 v1 v2. *)
243 244 245
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
246
  inversion H3; subst; inversion H9; subst.
247
    unfold updEnv in *; simpl in *.
248
    inversion H8; inversion H1; subst.
249
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
250
  clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
251 252 253 254 255 256 257 258 259 260 261 262 263
  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.
264 265
Qed.

266 267 268 269 270 271 272 273
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.
274
Proof.
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 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
  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.
405
        rewrite equal_naming_inv; try lra.
406 407
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
408
        unfold Rdiv.
409
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
410 411 412
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
413 414 415 416 417 418 419 420 421 422 423 424 425 426
          - 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).
427 428
Qed.

429 430 431 432 433 434 435 436
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.
437
Proof.
438 439 440 441 442 443
  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.
444

445
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
446
  eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 ->
447
  eval_exp E2 defVars e nF1 m ->
448
  eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n)  (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
449 450 451 452 453 454 455 456 457 458 459 460
  (Rabs (nR - nF1) <= err)%R ->
  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%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.
461
    inversion H0; subst.
462
    unfold perturb; simpl.
463
    unfold updEnv in H3; simpl in H3; inversion H3; subst.
464 465 466 467 468 469 470
    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.
    + auto. 
Qed.