ErrorBounds.v 16.9 KB
 Heiko Becker committed Aug 18, 2016 1 ``````(** `````` Heiko Becker committed Sep 18, 2016 2 3 ``````Proofs of general bounds on the error of arithmetic expressions. This shortens soundness proofs later. `````` Heiko Becker committed Oct 06, 2016 4 ``````Bounds are explained in section 5, Deriving Computable Error Bounds `````` Heiko Becker committed Aug 18, 2016 5 ``````**) `````` Heiko Becker committed Nov 08, 2016 6 ``````Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals. `````` Heiko Becker committed Feb 07, 2017 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 committed Sep 18, 2016 9 `````` `````` Heiko Becker committed Feb 19, 2017 10 11 12 ``````Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult): eval_exp 0%R E1 (Const n) nR -> eval_exp (Q2R machineEpsilon) E2 (Const n) nF -> `````` Heiko Becker committed Nov 17, 2016 13 `````` (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R. `````` Heiko Becker committed Aug 18, 2016 14 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 15 `````` intros eval_real eval_float. `````` Heiko Becker committed Aug 18, 2016 16 `````` inversion eval_real; subst. `````` Heiko Becker committed Oct 13, 2016 17 `````` rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Aug 18, 2016 18 19 `````` inversion eval_float; subst. unfold perturb; simpl. `````` Heiko Becker committed Jan 09, 2017 20 `````` rewrite Rabs_err_simpl, Rabs_mult. `````` Heiko Becker committed Aug 18, 2016 21 22 23 `````` apply Rmult_le_compat_l; [apply Rabs_pos | auto]. Qed. `````` Heiko Becker committed Feb 01, 2017 24 ``````Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` Heiko Becker committed Feb 19, 2017 25 26 27 28 29 30 31 `````` (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q): eval_exp 0%R E1 (toRExp e1) e1R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> eval_exp 0%R E1 (toRExp e2) e2R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> eval_exp 0%R E1 (Binop Plus (toRExp e1) (toRExp e2)) vR -> eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var R 1) (Var R 2)) vF -> `````` Heiko Becker committed Feb 13, 2017 32 33 34 `````` (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R. `````` Heiko Becker committed Aug 18, 2016 35 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 36 `````` intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2. `````` Heiko Becker committed Aug 18, 2016 37 38 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) inversion plus_real; subst. `````` Heiko Becker committed Oct 13, 2016 39 `````` rewrite delta_0_deterministic in plus_real; auto. `````` Heiko Becker committed Oct 31, 2016 40 41 `````` rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto. unfold evalBinop in *; simpl in *. `````` Heiko Becker committed Aug 18, 2016 42 `````` clear delta H2. `````` 43 `````` rewrite (meps_0_deterministic H3 e1_real); `````` Heiko Becker committed Oct 13, 2016 44 `````` rewrite (meps_0_deterministic H5 e2_real). `````` 45 `````` rewrite (meps_0_deterministic H3 e1_real) in plus_real. `````` Heiko Becker committed Oct 13, 2016 46 `````` rewrite (meps_0_deterministic H5 e2_real) in plus_real. `````` 47 `````` clear H3 H5 H6 v1 v2. `````` Heiko Becker committed Aug 18, 2016 48 49 50 `````` (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion plus_float; subst. unfold perturb; simpl. `````` 51 `````` inversion H3; subst; inversion H5; subst. `````` Heiko Becker committed Aug 18, 2016 52 `````` unfold updEnv; simpl. `````` Heiko Becker committed Feb 19, 2017 53 54 55 `````` unfold updEnv in H0,H1; simpl in *. symmetry in H0, H1. inversion H0; inversion H1; subst. `````` Heiko Becker committed Aug 18, 2016 56 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` 57 `````` clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1. `````` Heiko Becker committed Aug 18, 2016 58 59 60 61 62 63 64 65 66 67 68 69 `````` 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. `````` Heiko Becker committed Feb 19, 2017 70 `````` apply H1. `````` Heiko Becker committed Aug 18, 2016 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 `````` 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 **) `````` Heiko Becker committed Feb 03, 2017 87 ``````Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) `````` Heiko Becker committed Feb 19, 2017 88 89 90 91 92 93 94 `````` (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2: eval_exp 0%R E1 (toRExp e1) e1R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> eval_exp 0%R E1 (toRExp e2) e2R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> eval_exp 0%R E1 (Binop Sub (toRExp e1) (toRExp e2)) vR -> eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var R 1) (Var R 2)) vF -> `````` Heiko Becker committed Feb 08, 2017 95 96 97 `````` (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R. `````` Heiko Becker committed Aug 18, 2016 98 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 99 `````` intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2. `````` Heiko Becker committed Aug 18, 2016 100 101 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) inversion sub_real; subst. `````` Heiko Becker committed Oct 13, 2016 102 103 `````` rewrite delta_0_deterministic in sub_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 104 `````` unfold evalBinop in *; simpl in *. `````` Heiko Becker committed Aug 18, 2016 105 `````` clear delta H2. `````` 106 `````` rewrite (meps_0_deterministic H3 e1_real); `````` Heiko Becker committed Oct 13, 2016 107 `````` rewrite (meps_0_deterministic H5 e2_real). `````` 108 `````` rewrite (meps_0_deterministic H3 e1_real) in sub_real. `````` Heiko Becker committed Oct 13, 2016 109 `````` rewrite (meps_0_deterministic H5 e2_real) in sub_real. `````` 110 `````` clear H3 H5 H6 v1 v2. `````` Heiko Becker committed Aug 18, 2016 111 112 113 `````` (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion sub_float; subst. unfold perturb; simpl. `````` 114 `````` inversion H3; subst; inversion H5; subst. `````` Heiko Becker committed Aug 18, 2016 115 `````` unfold updEnv; simpl. `````` Heiko Becker committed Feb 19, 2017 116 117 118 `````` symmetry in H0, H1. unfold updEnv in H0, H1; simpl in H0, H1. inversion H0; inversion H1; subst. `````` Heiko Becker committed Aug 18, 2016 119 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` 120 `````` clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1. `````` Heiko Becker committed Aug 18, 2016 121 122 123 124 125 `````` 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. `````` Heiko Becker committed Sep 21, 2016 126 `````` rewrite Ropp_involutive. `````` Heiko Becker committed Aug 18, 2016 127 128 `````` rewrite Rplus_assoc. eapply Rle_trans. `````` Heiko Becker committed Sep 21, 2016 129 `````` apply Rabs_triang. `````` Heiko Becker committed Aug 18, 2016 130 `````` eapply Rle_trans. `````` Heiko Becker committed Sep 21, 2016 131 132 `````` eapply Rplus_le_compat_l. apply Rabs_triang. `````` Heiko Becker committed Aug 18, 2016 133 `````` rewrite <- Rplus_assoc. `````` Heiko Becker committed Sep 21, 2016 134 `````` setoid_rewrite Rplus_comm at 4. `````` Heiko Becker committed Aug 18, 2016 135 136 `````` repeat rewrite <- Rsub_eq_Ropp_Rplus. rewrite Rabs_Ropp. `````` Heiko Becker committed Sep 21, 2016 137 138 139 140 `````` 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]. `````` Heiko Becker committed Aug 23, 2016 141 142 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 143 ``````Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` Heiko Becker committed Feb 19, 2017 144 145 146 147 148 149 150 `````` (vR:R) (vF:R) (E1 E2:env): eval_exp 0%R E1 (toRExp e1) e1R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> eval_exp 0%R E1 (toRExp e2) e2R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> eval_exp 0%R E1 (Binop Mult (toRExp e1) (toRExp e2)) vR -> eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var R 1) (Var R 2)) vF -> `````` Heiko Becker committed Nov 17, 2016 151 `````` (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R. `````` Heiko Becker committed Aug 23, 2016 152 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 153 `````` intros e1_real e1_float e2_real e2_float mult_real mult_float. `````` Heiko Becker committed Oct 07, 2016 154 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) `````` Heiko Becker committed Aug 23, 2016 155 `````` inversion mult_real; subst. `````` Heiko Becker committed Oct 13, 2016 156 157 `````` rewrite delta_0_deterministic in mult_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 158 `````` unfold evalBinop in *; simpl in *. `````` Heiko Becker committed Aug 23, 2016 159 `````` clear delta H2. `````` 160 `````` rewrite (meps_0_deterministic H3 e1_real); `````` Heiko Becker committed Oct 13, 2016 161 `````` rewrite (meps_0_deterministic H5 e2_real). `````` 162 `````` rewrite (meps_0_deterministic H3 e1_real) in mult_real. `````` Heiko Becker committed Oct 13, 2016 163 `````` rewrite (meps_0_deterministic H5 e2_real) in mult_real. `````` 164 `````` clear H3 H5 H6 v1 v2. `````` Heiko Becker committed Aug 23, 2016 165 166 167 `````` (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion mult_float; subst. unfold perturb; simpl. `````` 168 `````` inversion H3; subst; inversion H5; subst. `````` Heiko Becker committed Feb 19, 2017 169 `````` symmetry in H0, H1; `````` Heiko Becker committed Feb 17, 2017 170 `````` unfold updEnv in *; simpl in *. `````` Heiko Becker committed Feb 19, 2017 171 `````` inversion H0; inversion H1; subst. `````` Heiko Becker committed Aug 23, 2016 172 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` 173 `````` clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1. `````` Heiko Becker committed Aug 23, 2016 174 175 176 177 `````` repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. `````` Heiko Becker committed Aug 24, 2016 178 179 `````` rewrite <- Rplus_assoc. setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2. `````` Heiko Becker committed Aug 23, 2016 180 181 182 `````` eapply Rle_trans. eapply Rabs_triang. eapply Rplus_le_compat_l. `````` Heiko Becker committed Aug 24, 2016 183 `````` rewrite Rabs_Ropp. `````` Heiko Becker committed Aug 23, 2016 184 `````` repeat rewrite Rabs_mult. `````` Heiko Becker committed Aug 24, 2016 185 `````` eapply Rmult_le_compat_l; auto. `````` Heiko Becker committed Aug 23, 2016 186 187 `````` rewrite <- Rabs_mult. apply Rabs_pos. `````` Heiko Becker committed Oct 07, 2016 188 189 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 190 ``````Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` Heiko Becker committed Feb 19, 2017 191 192 193 194 195 196 197 `````` (vR:R) (vF:R) (E1 E2:env): eval_exp 0%R E1 (toRExp e1) e1R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> eval_exp 0%R E1 (toRExp e2) e2R -> eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> eval_exp 0%R E1 (Binop Div (toRExp e1) (toRExp e2)) vR -> eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Div (Var R 1) (Var R 2)) vF -> `````` Heiko Becker committed Nov 17, 2016 198 `````` (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R. `````` Heiko Becker committed Oct 07, 2016 199 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 200 `````` intros e1_real e1_float e2_real e2_float div_real div_float. `````` Heiko Becker committed Oct 07, 2016 201 202 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) inversion div_real; subst. `````` Heiko Becker committed Oct 13, 2016 203 204 `````` rewrite delta_0_deterministic in div_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 205 `````` unfold evalBinop in *; simpl in *. `````` Heiko Becker committed Oct 07, 2016 206 `````` clear delta H2. `````` 207 `````` rewrite (meps_0_deterministic H3 e1_real); `````` Heiko Becker committed Oct 13, 2016 208 `````` rewrite (meps_0_deterministic H5 e2_real). `````` 209 `````` rewrite (meps_0_deterministic H3 e1_real) in div_real. `````` Heiko Becker committed Oct 13, 2016 210 `````` rewrite (meps_0_deterministic H5 e2_real) in div_real. `````` 211 `````` clear H3 H5 H6 v1 v2. `````` Heiko Becker committed Oct 07, 2016 212 213 214 `````` (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion div_float; subst. unfold perturb; simpl. `````` 215 `````` inversion H3; subst; inversion H5; subst. `````` Heiko Becker committed Feb 19, 2017 216 `````` symmetry in H0, H1; `````` Heiko Becker committed Feb 17, 2017 217 `````` unfold updEnv in *; simpl in *. `````` Heiko Becker committed Feb 19, 2017 218 `````` inversion H0; inversion H1; subst. `````` Heiko Becker committed Oct 07, 2016 219 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` 220 `````` clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1. `````` Heiko Becker committed Oct 07, 2016 221 222 223 224 225 226 227 228 229 230 231 232 233 `````` 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. `````` Heiko Becker committed Nov 08, 2016 234 235 ``````Qed. `````` Heiko Becker committed Jan 13, 2017 236 237 238 239 240 241 242 243 ``````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. `````` Heiko Becker committed Nov 08, 2016 244 ``````Proof. `````` Heiko Becker committed Jan 13, 2017 245 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 `````` 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. `````` Heiko Becker committed Nov 08, 2016 375 `````` rewrite equal_naming_inv; try lra. `````` Heiko Becker committed Jan 13, 2017 376 377 `````` assert (nR + - (nR + err) = - err)%R as simpl_up by lra. rewrite simpl_up. `````` Heiko Becker committed Nov 08, 2016 378 `````` unfold Rdiv. `````` Heiko Becker committed Jan 13, 2017 379 `````` rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute. `````` Heiko Becker committed Nov 08, 2016 380 381 382 `````` { rewrite <- Ropp_mult_distr_r. rewrite Ropp_involutive. apply Rmult_le_compat_l; try auto. apply Rinv_le_contravar. `````` Heiko Becker committed Jan 13, 2017 383 384 385 386 387 388 389 390 391 392 393 394 395 396 `````` - 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). `````` Heiko Becker committed Nov 08, 2016 397 398 ``````Qed. `````` Heiko Becker committed Jan 13, 2017 399 400 401 402 403 404 405 406 ``````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. `````` Heiko Becker committed Nov 08, 2016 407 ``````Proof. `````` Heiko Becker committed Jan 13, 2017 408 409 410 411 412 413 `````` 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.``````