ErrorBounds.v 17.8 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.
8
Require Import Daisy.Environments.
Heiko Becker's avatar
Heiko Becker committed
9

10 11 12
Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (VarEnv ParamEnv:env):
  eval_exp 0%R VarEnv ParamEnv P (Const n) nR ->
  eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Const n) nF ->
13
  (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
14
Proof.
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 22 23
  apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.

24 25 26 27
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv ParamEnv:env):
  eval_exp 0%R VarEnv ParamEnv P (Param R n) nR ->
  eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P (Param R n) nF ->
  (Rabs (nR - nF) <= Rabs (ParamEnv 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 46 47 48 49 50
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
  approxEnv VarEnv1 absenv VarEnv2 ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
  eval_exp 0%R VarEnv1 ParamEnv P (Binop Plus (toRExp e1) (toRExp e2)) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var R 1) (Var R 2)) vF ->
  (Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
  (Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
  (Rabs (vR - vF) <= Q2R (snd(absenv e1)) + Q2R (snd (absenv e2)) + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
51
Proof.
52
  intros approxCEnv e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
53 54
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion plus_real; subst.
55
  rewrite delta_0_deterministic in plus_real; auto.
56 57
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
  unfold evalBinop in *; simpl in *.
58
  clear delta H2.
59 60 61 62
  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.
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 98 99
  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
**)
100 101 102 103 104 105 106 107 108 109 110 111
Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
      (e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P absenv:
  approxEnv VarEnv1 absenv VarEnv2 ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
  eval_exp 0%R VarEnv1 ParamEnv P (Binop Sub (toRExp e1) (toRExp e2)) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF ->
  (Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
  (Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
  (Rabs (vR - vF) <= Q2R (snd (absenv e1)) + Q2R (snd (absenv e2)) + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
112
Proof.
113
  intros approxCEnv e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
114 115
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion sub_real; subst.
116 117
  rewrite delta_0_deterministic in sub_real; auto.
  rewrite delta_0_deterministic; auto.
118
  unfold evalBinop in *; simpl in *.
119
  clear delta H2.
120 121 122 123
  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.
124 125 126 127 128 129 130 131 132 133 134 135 136
  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.
137
  rewrite Ropp_involutive.
138 139
  rewrite Rplus_assoc.
  eapply Rle_trans.
140
  apply Rabs_triang.
141
  eapply Rle_trans.
142 143
  eapply Rplus_le_compat_l.
  apply Rabs_triang.
144
  rewrite <- Rplus_assoc.
145
  setoid_rewrite Rplus_comm at 4.
146 147
  repeat rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite Rabs_Ropp.
148 149 150 151
  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].
152 153
Qed.

154 155 156 157 158 159 160 161 162
Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
  approxEnv VarEnv1 absenv VarEnv2 ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
  eval_exp 0%R VarEnv1 ParamEnv P (Binop Mult (toRExp e1) (toRExp e2)) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
163
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
164
Proof.
165
  intros approxCEnv e1_real e1_float e2_real e2_float mult_real mult_float.
166
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
167
  inversion mult_real; subst.
168 169
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
170
  unfold evalBinop in *; simpl in *.
171
  clear delta H2.
172 173 174 175
  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.
176 177 178 179 180 181 182 183 184 185 186 187
  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
188 189
  rewrite <- Rplus_assoc.
  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
190 191 192
  eapply Rle_trans.
  eapply Rabs_triang.
  eapply Rplus_le_compat_l.
Heiko Becker's avatar
Heiko Becker committed
193
  rewrite Rabs_Ropp.
194
  repeat rewrite Rabs_mult.
Heiko Becker's avatar
Heiko Becker committed
195
  eapply Rmult_le_compat_l; auto.
196 197
  rewrite <- Rabs_mult.
  apply Rabs_pos.
198 199
Qed.

200 201 202 203 204 205 206 207 208
Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
  approxEnv VarEnv1 absenv VarEnv2 ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
  eval_exp 0%R VarEnv1 ParamEnv P (Binop Div (toRExp e1) (toRExp e2)) vR ->
  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
209
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
210
Proof.
211
  intros approxCenv e1_real e1_float e2_real e2_float div_real div_float.
212 213
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
  inversion div_real; subst.
214 215
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
216
  unfold evalBinop in *; simpl in *.
217
  clear delta H2.
218 219 220 221
  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.
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
  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.
243 244
Qed.

245 246 247 248 249 250 251 252
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.
253
Proof.
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 376 377 378 379 380 381 382 383
  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.
384
        rewrite equal_naming_inv; try lra.
385 386
        assert (nR + - (nR + err) = - err)%R as simpl_up by lra.
        rewrite simpl_up.
387
        unfold Rdiv.
388
        rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute.
389 390 391
        { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive.
          apply Rmult_le_compat_l; try auto.
          apply Rinv_le_contravar.
392 393 394 395 396 397 398 399 400 401 402 403 404 405
          - 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).
406 407
Qed.

408 409 410 411 412 413 414 415
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.
416
Proof.
417 418 419 420 421 422
  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.