ErrorBounds.v 22.4 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 `````` `````` = committed May 02, 2017 10 11 `````` Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 12 `````` eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 -> `````` = committed Apr 04, 2017 13 `````` eval_exp E2 defVars (Const m n) nF m -> `````` Heiko Becker committed Jun 29, 2017 14 `````` (Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R. `````` Heiko Becker committed Aug 18, 2016 15 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 16 `````` intros eval_real eval_float. `````` Heiko Becker committed Aug 18, 2016 17 `````` inversion eval_real; subst. `````` Heiko Becker committed Oct 13, 2016 18 `````` rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Aug 18, 2016 19 20 `````` inversion eval_float; subst. unfold perturb; simpl. `````` Heiko Becker committed Jan 09, 2017 21 `````` rewrite Rabs_err_simpl, Rabs_mult. `````` Heiko Becker committed Aug 18, 2016 22 `````` apply Rmult_le_compat_l; [apply Rabs_pos | auto]. `````` Heiko Becker committed Jun 29, 2017 23 `````` simpl (mTypeToQ M0) in *. `````` Raphaël Monat committed Mar 01, 2017 24 `````` apply (Rle_trans _ (Q2R 0) _); try auto. `````` Raphaël Monat committed Mar 03, 2017 25 `````` rewrite Q2R0_is_0; lra. `````` Heiko Becker committed Aug 18, 2016 26 27 ``````Qed. `````` Heiko Becker committed Sep 18, 2017 28 `````` `````` Heiko Becker committed Feb 01, 2017 29 ``````Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` = committed Apr 04, 2017 30 `````` (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 31 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> `````` = committed Apr 04, 2017 32 `````` eval_exp E2 defVars (toRExp e1) e1F m1-> `````` Heiko Becker committed Jun 29, 2017 33 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> `````` = committed Apr 04, 2017 34 `````` eval_exp E2 defVars (toRExp e2) e2F m2 -> `````` Heiko Becker committed Jun 29, 2017 35 `````` eval_exp E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> `````` = committed May 02, 2017 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 committed Feb 13, 2017 39 40 `````` (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> `````` Heiko Becker committed Jun 29, 2017 41 `````` (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R. `````` Heiko Becker committed Aug 18, 2016 42 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 43 `````` intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2. `````` Heiko Becker committed Aug 18, 2016 44 45 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) inversion plus_real; subst. `````` Heiko Becker committed Sep 18, 2017 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. `````` Heiko Becker committed Oct 13, 2016 49 `````` rewrite delta_0_deterministic in plus_real; auto. `````` Heiko Becker committed Oct 31, 2016 50 51 `````` rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto. unfold evalBinop in *; simpl in *. `````` = committed Mar 28, 2017 52 `````` clear delta H3. `````` Raphaël Monat committed Mar 10, 2017 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. `````` = committed Mar 28, 2017 57 `````` clear H5 H6 H7 v1 v2. `````` Heiko Becker committed Aug 18, 2016 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. `````` = committed Mar 28, 2017 61 `````` inversion H4; subst; inversion H7; subst. `````` Heiko Becker committed Aug 18, 2016 62 `````` unfold updEnv; simpl. `````` = committed Apr 04, 2017 63 64 65 `````` unfold updEnv in H1,H6; simpl in *. symmetry in H1,H6. inversion H1; inversion H6; subst. `````` Heiko Becker committed Aug 18, 2016 66 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` = committed Apr 04, 2017 67 `````` clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1. `````` Heiko Becker committed Aug 18, 2016 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))). `````` = committed Apr 04, 2017 78 `````` pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H1). `````` Heiko Becker committed Aug 18, 2016 79 `````` eapply Rle_trans. `````` = committed Apr 04, 2017 80 `````` apply H4. `````` Heiko Becker committed Aug 18, 2016 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. `````` Raphaël Monat committed Mar 10, 2017 90 `````` apply H3. `````` Heiko Becker committed Aug 18, 2016 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 **) `````` Heiko Becker committed Feb 03, 2017 97 ``````Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) `````` = committed Apr 04, 2017 98 `````` (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 99 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> `````` = committed Apr 04, 2017 100 `````` eval_exp E2 defVars (toRExp e1) e1F m1 -> `````` Heiko Becker committed Jun 29, 2017 101 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> `````` = committed Apr 04, 2017 102 `````` eval_exp E2 defVars (toRExp e2) e2F m2 -> `````` Heiko Becker committed Jun 29, 2017 103 `````` eval_exp E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> `````` = committed May 02, 2017 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 committed Feb 08, 2017 107 108 `````` (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> `````` Heiko Becker committed Jun 29, 2017 109 `````` (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (mTypeToQ m))))%R. `````` Heiko Becker committed Aug 18, 2016 110 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 111 `````` intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2. `````` Heiko Becker committed Aug 18, 2016 112 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) `````` Raphaël Monat committed Mar 01, 2017 113 `````` inversion sub_real; subst; `````` Heiko Becker committed Sep 18, 2017 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. `````` Heiko Becker committed Oct 13, 2016 117 118 `````` rewrite delta_0_deterministic in sub_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 119 `````` unfold evalBinop in *; simpl in *. `````` = committed Mar 28, 2017 120 `````` clear delta H3. `````` Raphaël Monat committed Mar 10, 2017 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. `````` = committed Mar 28, 2017 125 `````` clear H5 H6 H7 v1 v2. `````` Heiko Becker committed Aug 18, 2016 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. `````` = committed Mar 28, 2017 129 `````` inversion H4; subst; inversion H7; subst. `````` Heiko Becker committed Aug 18, 2016 130 `````` unfold updEnv; simpl. `````` = committed Apr 04, 2017 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. `````` Heiko Becker committed Aug 18, 2016 135 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` = committed Apr 04, 2017 136 `````` clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H1 H6. `````` Heiko Becker committed Aug 18, 2016 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. `````` Heiko Becker committed Sep 21, 2016 142 `````` rewrite Ropp_involutive. `````` Heiko Becker committed Aug 18, 2016 143 144 `````` rewrite Rplus_assoc. eapply Rle_trans. `````` Heiko Becker committed Sep 21, 2016 145 `````` apply Rabs_triang. `````` Heiko Becker committed Aug 18, 2016 146 `````` eapply Rle_trans. `````` Heiko Becker committed Sep 21, 2016 147 148 `````` eapply Rplus_le_compat_l. apply Rabs_triang. `````` Heiko Becker committed Aug 18, 2016 149 `````` rewrite <- Rplus_assoc. `````` Heiko Becker committed Sep 21, 2016 150 `````` setoid_rewrite Rplus_comm at 4. `````` Heiko Becker committed Aug 18, 2016 151 152 `````` repeat rewrite <- Rsub_eq_Ropp_Rplus. rewrite Rabs_Ropp. `````` Heiko Becker committed Sep 21, 2016 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]. `````` Heiko Becker committed Aug 23, 2016 157 158 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 159 ``````Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` = committed Apr 04, 2017 160 `````` (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 161 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> `````` = committed Apr 04, 2017 162 `````` eval_exp E2 defVars (toRExp e1) e1F m1 -> `````` Heiko Becker committed Jun 29, 2017 163 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> `````` = committed Apr 04, 2017 164 `````` eval_exp E2 defVars (toRExp e2) e2F m2 -> `````` Heiko Becker committed Jun 29, 2017 165 `````` eval_exp E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> `````` = committed May 02, 2017 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 -> `````` Heiko Becker committed Jun 29, 2017 169 `````` (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ m)))%R. `````` Heiko Becker committed Aug 23, 2016 170 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 171 `````` intros e1_real e1_float e2_real e2_float mult_real mult_float. `````` Heiko Becker committed Oct 07, 2016 172 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) `````` Raphaël Monat committed Mar 01, 2017 173 `````` inversion mult_real; subst; `````` Heiko Becker committed Sep 18, 2017 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. `````` Heiko Becker committed Oct 13, 2016 177 178 `````` rewrite delta_0_deterministic in mult_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 179 `````` unfold evalBinop in *; simpl in *. `````` = committed Mar 28, 2017 180 `````` clear delta H3. `````` Raphaël Monat committed Mar 10, 2017 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. `````` = committed Mar 28, 2017 185 `````` clear H5 H6 v1 v2 H7 H2. `````` Heiko Becker committed Aug 23, 2016 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. `````` = committed Mar 28, 2017 189 `````` inversion H3; subst; inversion H6; subst. `````` Heiko Becker committed Feb 17, 2017 190 `````` unfold updEnv in *; simpl in *. `````` = committed Apr 04, 2017 191 192 `````` inversion H6; inversion H1; subst. simpl in H8; simpl in H9; intros; inversion H5; subst. `````` Heiko Becker committed Aug 23, 2016 193 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` = committed Apr 04, 2017 194 `````` clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1. `````` Heiko Becker committed Aug 23, 2016 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 committed Aug 24, 2016 199 200 `````` rewrite <- Rplus_assoc. setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2. `````` Heiko Becker committed Aug 23, 2016 201 202 203 `````` eapply Rle_trans. eapply Rabs_triang. eapply Rplus_le_compat_l. `````` Heiko Becker committed Aug 24, 2016 204 `````` rewrite Rabs_Ropp. `````` Heiko Becker committed Aug 23, 2016 205 `````` repeat rewrite Rabs_mult. `````` Heiko Becker committed Aug 24, 2016 206 `````` eapply Rmult_le_compat_l; auto. `````` Heiko Becker committed Aug 23, 2016 207 208 `````` rewrite <- Rabs_mult. apply Rabs_pos. `````` Heiko Becker committed Oct 07, 2016 209 210 ``````Qed. `````` Heiko Becker committed Feb 03, 2017 211 ``````Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) `````` = committed Apr 04, 2017 212 `````` (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 213 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> `````` = committed Apr 04, 2017 214 `````` eval_exp E2 defVars (toRExp e1) e1F m1 -> `````` Heiko Becker committed Jun 29, 2017 215 `````` eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> `````` = committed Apr 04, 2017 216 `````` eval_exp E2 defVars (toRExp e2) e2F m2 -> `````` Heiko Becker committed Jun 29, 2017 217 `````` eval_exp E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> `````` = committed May 02, 2017 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 -> `````` Heiko Becker committed Jun 29, 2017 221 `````` (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ m)))%R. `````` Heiko Becker committed Oct 07, 2016 222 ``````Proof. `````` Heiko Becker committed Feb 08, 2017 223 `````` intros e1_real e1_float e2_real e2_float div_real div_float. `````` Heiko Becker committed Oct 07, 2016 224 `````` (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) `````` Raphaël Monat committed Mar 01, 2017 225 `````` inversion div_real; subst; `````` Heiko Becker committed Sep 18, 2017 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. `````` Heiko Becker committed Oct 13, 2016 229 230 `````` rewrite delta_0_deterministic in div_real; auto. rewrite delta_0_deterministic; auto. `````` Heiko Becker committed Oct 31, 2016 231 `````` unfold evalBinop in *; simpl in *. `````` = committed Mar 28, 2017 232 `````` clear delta H3 H2. `````` Raphaël Monat committed Mar 10, 2017 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. `````` = committed Mar 28, 2017 237 `````` (* clear H5 H6 v1 v2. *) `````` Heiko Becker committed Oct 07, 2016 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. `````` = committed Mar 28, 2017 241 `````` inversion H3; subst; inversion H9; subst. `````` Heiko Becker committed Feb 17, 2017 242 `````` unfold updEnv in *; simpl in *. `````` = committed Apr 04, 2017 243 `````` inversion H8; inversion H1; subst. `````` Heiko Becker committed Oct 07, 2016 244 `````` (* We have now obtained all necessary values from the evaluations --> remove them for readability *) `````` = committed Apr 04, 2017 245 `````` clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float. `````` Heiko Becker committed Oct 07, 2016 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. `````` Heiko Becker committed Nov 08, 2016 259 260 ``````Qed. `````` Nikita Zyuzin committed Nov 09, 2017 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 committed Nov 13, 2017 263 `````` (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars: `````` Nikita Zyuzin committed Nov 09, 2017 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 committed Nov 13, 2017 269 `````` eval_exp E2 defVars (toRExp e3) e3F m3-> `````` Nikita Zyuzin committed Nov 09, 2017 270 `````` eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 -> `````` Nikita Zyuzin committed Nov 13, 2017 271 `````` eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) `````` Nikita Zyuzin committed Nov 09, 2017 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 committed Nov 13, 2017 274 `````` (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R. `````` Nikita Zyuzin committed Nov 09, 2017 275 ``````Proof. `````` Nikita Zyuzin committed Nov 13, 2017 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 committed Nov 09, 2017 327 ``````Qed. `````` Heiko Becker committed Feb 28, 2018 328 `````` `````` Nikita Zyuzin committed Nov 09, 2017 329 `````` `````` Heiko Becker committed Jan 13, 2017 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. `````` Heiko Becker committed Nov 08, 2016 338 ``````Proof. `````` Heiko Becker committed Jan 13, 2017 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. `````` Heiko Becker committed Nov 08, 2016 469 `````` rewrite equal_naming_inv; try lra. `````` Heiko Becker committed Jan 13, 2017 470 471 `````` assert (nR + - (nR + err) = - err)%R as simpl_up by lra. rewrite simpl_up. `````` Heiko Becker committed Nov 08, 2016 472 `````` unfold Rdiv. `````` Heiko Becker committed Jan 13, 2017 473 `````` rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, <- Ropp_inv_permute. `````` Heiko Becker committed Nov 08, 2016 474 475 476 `````` { 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 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). `````` Heiko Becker committed Nov 08, 2016 491 492 ``````Qed. `````` Heiko Becker committed Jan 13, 2017 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. `````` Heiko Becker committed Nov 08, 2016 501 ``````Proof. `````` Heiko Becker committed Jan 13, 2017 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. `````` Raphaël Monat committed Mar 03, 2017 507 `````` `````` = committed Apr 04, 2017 508 ``````Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars: `````` Heiko Becker committed Jun 29, 2017 509 `````` eval_exp E1 (toRMap defVars) (toREval e) nR M0 -> `````` = committed Apr 04, 2017 510 `````` eval_exp E2 defVars e nF1 m -> `````` = committed May 02, 2017 511 512 513 `````` eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon-> `````` Raphaël Monat committed Mar 03, 2017 514 `````` (Rabs (nR - nF1) <= err)%R -> `````` Heiko Becker committed Jun 29, 2017 515 `````` (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (mTypeToQ machineEpsilon))%R. `````` Raphaël Monat committed Mar 03, 2017 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. `````` = committed Apr 04, 2017 526 `````` inversion H0; subst. `````` Raphaël Monat committed Mar 03, 2017 527 `````` unfold perturb; simpl. `````` = committed Apr 04, 2017 528 `````` unfold updEnv in H3; simpl in H3; inversion H3; subst. `````` Raphaël Monat committed Mar 03, 2017 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. `````` = committed Apr 25, 2017 534 `````` + auto. `````` Raphaël Monat committed Mar 03, 2017 535 ``Qed.``