IntervalArith.v 11.7 KB
 1 2 ``````(** Formalization of real valued interval arithmetic `````` Heiko Becker committed Oct 06, 2016 3 `````` Used in soundness proofs for error bound validator. `````` 4 ``````**) `````` Heiko Becker committed Sep 05, 2016 5 ``````Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals. `````` Heiko Becker committed Feb 17, 2017 6 ``````Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps. `````` Heiko Becker committed Jun 29, 2017 7 `````` `````` 8 9 10 11 ``````(** Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound. Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound. **) `````` Heiko Becker committed Jun 29, 2017 12 ``````Notation valid intv := `````` 13 14 `````` (IVlo intv <= IVhi intv)%R. `````` Heiko Becker committed Jun 29, 2017 15 ``````Notation contained x intv := `````` 16 17 `````` (IVlo intv <= x <= IVhi intv)%R. `````` Heiko Becker committed Jan 03, 2017 18 19 20 ``````Lemma contained_implies_valid (a:R) (iv:interval) : contained a iv -> valid iv. `````` 21 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 22 `````` intros inIntv; apply (Rle_trans _ a _); destruct inIntv; auto. `````` 23 24 25 26 ``````Qed. (** Subset definition; when an interval is a subinterval of another `````` Heiko Becker committed Aug 10, 2016 27 ``````**) `````` Heiko Becker committed Jun 29, 2017 28 29 30 31 32 33 34 35 36 37 ``````Notation isSupersetInterval iv1 iv2 := ((IVlo iv2 <= IVlo iv1)%R /\ (IVhi iv1 <= IVhi iv2)%R). Lemma contained_superset a iv1 iv2: contained a iv1 -> isSupersetInterval iv1 iv2 -> contained a iv2. Proof. intros; simpl in *. lra. Qed. `````` 38 39 40 `````` Definition pointInterval (x:R) := mkInterval x x. `````` Heiko Becker committed Jan 03, 2017 41 42 43 ``````Lemma contained_implies_subset (a:R) (iv:interval): contained a iv -> isSupersetInterval (pointInterval a) iv. `````` 44 45 ``````Proof. intros containedIntv. `````` Heiko Becker committed Jun 29, 2017 46 `````` unfold pointInterval in *; destruct containedIntv; split; auto. `````` 47 48 ``````Qed. `````` Heiko Becker committed Aug 09, 2016 49 ``````Lemma validPointInterval (a:R) : `````` Heiko Becker committed Aug 10, 2016 50 `````` contained a (pointInterval a). `````` Heiko Becker committed Aug 09, 2016 51 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 52 `````` split; simpl; apply Req_le; auto. `````` Heiko Becker committed Aug 09, 2016 53 54 ``````Qed. `````` 55 56 57 58 59 60 61 62 63 64 65 ``````(** Now comes the old part with the computational definitions. Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for daisy. **) (** TODO: Refactor into a list manipulating function instead **) Definition min4 (a:R) (b:R) (c:R) (d:R) := Rmin a (Rmin b (Rmin c d)). Definition max4 (a:R) (b:R) (c:R) (d:R) := Rmax a (Rmax b (Rmax c d)). `````` Heiko Becker committed Aug 10, 2016 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 100 101 102 103 104 105 ``````Lemma min4_correct (a b c d:R) : (let m := min4 a b c d in m <= a /\ m <= b /\ m <= c /\ m <= d)%R. Proof. intros m. repeat split; unfold m, min4. - apply Rmin_l. - assert (forall c, Rmin b c <= b)%R by (apply Rmin_l). apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto. apply Rmin_r. - assert (Rmin c d <= c)%R by (apply Rmin_l). assert (Rmin b (Rmin c d) <= c)%R. + apply (Rle_trans _ (Rmin c d) _); auto. apply Rmin_r. + apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto. apply Rmin_r. - assert (Rmin c d <= d)%R by (apply Rmin_r). assert (Rmin b (Rmin c d) <= d)%R. + apply (Rle_trans _ (Rmin c d) _); auto. apply Rmin_r. + apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto. apply Rmin_r. Qed. Lemma max4_correct (a b c d:R) : (let m := max4 a b c d in a <= m /\ b <= m /\ c <= m /\ d <= m)%R. Proof. intros m. repeat split; unfold m, max4. - apply Rmax_l. - assert (forall c, b <= Rmax b c)%R by (apply Rmax_l). apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r. - assert (c <= Rmax c d)%R by (apply Rmax_l). assert (c <= Rmax b (Rmax c d))%R. + apply (Rle_trans _ (Rmax c d) _); auto. apply Rmax_r. + apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r. - assert (d <= Rmax c d)%R by (apply Rmax_r). assert (d <= Rmax b (Rmax c d))%R. + apply (Rle_trans _ (Rmax c d) _); auto. apply Rmax_r. + apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r. Qed. `````` 106 107 108 ``````(** Asbtract interval update function, parametric by actual operator applied. **) `````` Heiko Becker committed Jan 03, 2017 109 ``````Definition absIntvUpd (op:R->R->R) (iv1:interval) (iv2:interval) := `````` 110 `````` ( `````` Heiko Becker committed Jan 03, 2017 111 112 113 114 115 116 117 118 `````` min4 (op (IVlo iv1) (IVlo iv2)) (op (IVlo iv1) (IVhi iv2)) (op (IVhi iv1) (IVlo iv2)) (op (IVhi iv1) (IVhi iv2)), max4 (op (IVlo iv1) (IVlo iv2)) (op (IVlo iv1) (IVhi iv2)) (op (IVhi iv1) (IVlo iv2)) (op (IVhi iv1) (IVhi iv2)) `````` 119 120 121 122 `````` ). Definition widenInterval (Iv:interval) (v:R) := mkInterval (IVlo Iv - v) (IVhi Iv + v). `````` Heiko Becker committed Jan 03, 2017 123 ``````Definition negateInterval (iv:interval) := mkInterval (- IVhi iv) (- IVlo iv). `````` 124 `````` `````` Heiko Becker committed Jan 03, 2017 125 126 ``````Lemma interval_negation_valid (iv:interval) (a:R) : contained a iv -> contained (- a) (negateInterval iv). `````` 127 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 128 `````` destruct iv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi]. `````` 129 130 131 `````` split; apply Ropp_ge_le_contravar; apply Rle_ge; auto. Qed. `````` Heiko Becker committed Jan 03, 2017 132 ``````Definition invertInterval (iv:interval) := mkInterval (/ IVhi iv) (/ IVlo iv). `````` Heiko Becker committed Aug 17, 2016 133 `````` `````` Heiko Becker committed Oct 04, 2016 134 135 136 ``````Lemma interval_inversion_valid (iv:interval) (a:R) : (IVhi iv < 0 \/ 0 < IVlo iv -> contained a iv -> contained (/ a) (invertInterval iv))%R. Proof. `````` Heiko Becker committed Jun 29, 2017 137 `````` destruct iv as [ivlo ivhi]; simpl; `````` Heiko Becker committed Oct 04, 2016 138 139 140 141 142 143 144 145 146 147 `````` intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi]; assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto); split. - assert (- / a <= - / ivhi)%R. + assert (0 < - ivhi)%R by lra. repeat rewrite Ropp_inv_permute; try lra. eapply RIneq.Rinv_le_contravar; try lra. + apply Ropp_le_ge_contravar in H0; repeat rewrite Ropp_involutive in H0; lra. - assert (- / ivlo <= - / a)%R. `````` Heiko Becker committed Oct 09, 2016 148 `````` + repeat rewrite Ropp_inv_permute; try lra. `````` Heiko Becker committed Oct 04, 2016 149 150 151 152 153 154 155 156 `````` eapply RIneq.Rinv_le_contravar; try lra. + apply Ropp_le_ge_contravar in H0; repeat rewrite Ropp_involutive in H0; lra. - eapply RIneq.Rinv_le_contravar; try lra. - eapply RIneq.Rinv_le_contravar; try lra. Qed. `````` 157 158 159 ``````Definition addInterval (iv1:interval) (iv2:interval) := absIntvUpd Rplus iv1 iv2. `````` Heiko Becker committed Jun 29, 2017 160 161 162 163 ``````Lemma interval_addition_valid iv1 iv2 a b: contained a iv1 -> contained b iv2 -> contained (a + b) (addInterval iv1 iv2). `````` 164 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 165 `````` unfold addInterval, absIntvUpd, min4, max4. `````` 166 167 168 169 170 171 172 173 174 175 176 177 178 179 `````` intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi]. simpl; split. (** Lower Bound **) - assert ( fst iv1 + fst iv2 <= a + b)%R as lower_bound by (apply Rplus_le_compat; auto). apply (Rle_trans _ (fst iv1 + fst iv2) _); [apply Rmin_l | auto]. (** Upper Bound **) - assert (a + b <= snd iv1 + snd iv2)%R as upper_bound by (apply Rplus_le_compat; auto). apply (Rle_trans _ (snd iv1 + snd iv2) _); [ auto | ]. apply (Rle_trans _ (Rmax (fst iv1 + snd iv2) (Rmax (snd iv1 + fst iv2) (snd iv1 + snd iv2))) _); [ | apply Rmax_r]. apply (Rle_trans _ (Rmax (snd iv1 + fst iv2) (snd iv1 + snd iv2)) _ ); [ | apply Rmax_r]. apply (Rle_trans _ (snd iv1 + snd iv2) _); [ apply Req_le; auto | apply Rmax_r]. Qed. `````` Heiko Becker committed Jan 03, 2017 180 181 ``````Definition subtractInterval (iv1:interval) (iv2:interval) := addInterval iv1 (negateInterval iv2). `````` 182 `````` `````` Heiko Becker committed Jun 29, 2017 183 184 185 186 ``````Corollary interval_subtraction_valid iv1 iv2 a b: contained a iv1 -> contained b iv2 -> contained (a - b) (subtractInterval iv1 iv2). `````` 187 ``````Proof. `````` Heiko Becker committed Sep 07, 2016 188 `````` unfold subtractInterval. `````` Heiko Becker committed Jan 03, 2017 189 `````` intros contained_1 contained_iv2. `````` Heiko Becker committed Aug 15, 2016 190 `````` rewrite Rsub_eq_Ropp_Rplus. `````` Heiko Becker committed Jan 04, 2017 191 `````` apply interval_addition_valid; auto. `````` Heiko Becker committed Aug 17, 2016 192 `````` apply interval_negation_valid; auto. `````` 193 194 195 196 197 ``````Qed. Definition multInterval (iv1:interval) (iv2:interval) := absIntvUpd Rmult iv1 iv2. `````` Heiko Becker committed Aug 10, 2016 198 199 200 201 202 ``````(** Prove validity of multiplication for the interval lattice. Prove is structurally the same as the proof done Jourdan et al. in Verasco, in FloatIntervalsForward.v TODO: Credit **) `````` Heiko Becker committed Jan 03, 2017 203 204 205 206 ``````Lemma interval_multiplication_valid (iv1:interval) (iv2:interval) (a:R) (b:R) : contained a iv1 -> contained b iv2 -> contained (a * b) (multInterval iv1 iv2). `````` 207 ``````Proof. `````` Heiko Becker committed Jun 29, 2017 208 `````` unfold multInterval, absIntvUpd, IVlo, IVhi. `````` Heiko Becker committed Jan 03, 2017 209 `````` destruct iv1 as [ivlo1 ivhi1]; destruct iv2 as [ivlo2 ivhi2]; simpl. `````` Heiko Becker committed Aug 10, 2016 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 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 `````` intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi]. pose proof (min4_correct (ivlo1 * ivlo2) (ivlo1 * ivhi2) (ivhi1 * ivlo2) (ivhi1 * ivhi2)) as [leq_lolo [leq_lohi [leq_hilo leq_hihi]]]; pose proof (max4_correct (ivlo1 * ivlo2) (ivlo1 * ivhi2) (ivhi1 * ivlo2) (ivhi1 * ivhi2)) as [lolo_leq [lohi_leq [hilo_leq hihi_leq]]]. split. (* Lower Bound *) - destruct (Rle_lt_dec a 0). + destruct (Rle_lt_dec ivhi2 0). * pose proof (Rmult_le_compat_neg_l a b ivhi2 r b_leq_hi) as ahi2_leq_ab. pose proof (Rmult_le_compat_neg_l ivhi2 a ivhi1 r0 a_leq_hi) as hihi_leq_ahi2. eapply Rle_trans. apply leq_hihi. rewrite Rmult_comm. eapply Rle_trans. apply hihi_leq_ahi2. rewrite Rmult_comm; auto. * eapply Rle_trans. apply leq_lohi. apply Rlt_le in r0. pose proof (Rmult_le_compat_l ivhi2 ivlo1 a). rewrite Rmult_comm. eapply (Rle_trans). apply H; auto. rewrite Rmult_comm. eapply (Rmult_le_compat_neg_l a); auto. + destruct (Rle_lt_dec ivlo2 0). * eapply Rle_trans. apply leq_hilo. rewrite Rmult_comm. eapply Rle_trans. apply (Rmult_le_compat_neg_l ivlo2 a ivhi1 r0 a_leq_hi). rewrite Rmult_comm. eapply (Rmult_le_compat_l a); auto. exact (Rlt_le _ _ r). * eapply Rle_trans. apply leq_lolo. apply Rlt_le in r; apply Rlt_le in r0. rewrite Rmult_comm. apply (Rle_trans _ (ivlo2 * a)). eapply (Rmult_le_compat_l ivlo2 ); auto. rewrite Rmult_comm. eapply (Rmult_le_compat_l a); auto. - destruct (Rle_lt_dec a 0). + eapply Rle_trans. apply (Rmult_le_compat_neg_l a ivlo2); auto. destruct (Rle_lt_dec ivlo2 0). * rewrite Rmult_comm. eapply Rle_trans. eapply (Rmult_le_compat_neg_l ivlo2 ivlo1); auto. rewrite Rmult_comm; auto. * rewrite Rmult_comm. eapply Rle_trans. eapply (Rmult_le_compat_l ivlo2 a ivhi1); auto. apply Rlt_le; auto. rewrite Rmult_comm; auto. + eapply Rle_trans. apply (Rmult_le_compat_l) with (r2 := ivhi2); auto. apply Rlt_le; auto. destruct (Rle_lt_dec ivhi2 0). * rewrite Rmult_comm. eapply Rle_trans. eapply (Rmult_le_compat_neg_l) with (r1:= ivlo1); auto. rewrite Rmult_comm; auto. * rewrite Rmult_comm; eapply Rle_trans. apply (Rmult_le_compat_l) with (r2 := ivhi1); auto. apply Rlt_le; auto. rewrite Rmult_comm; auto. `````` 274 275 ``````Qed. `````` Heiko Becker committed Jan 03, 2017 276 277 ``````Definition divideInterval (iv1:interval) (iv2:interval) := multInterval iv1 (mkInterval (/ (IVhi iv2)) (/ (IVlo iv2))). `````` Heiko Becker committed Aug 17, 2016 278 `````` `````` Heiko Becker committed Jan 04, 2017 279 ``````Corollary interval_division_valid a b iv1 iv2: `````` Heiko Becker committed Jan 03, 2017 280 `````` (IVhi iv2 < 0 \/ 0 < IVlo iv2 -> contained a iv1 -> contained b iv2 -> contained (a / b) (divideInterval iv1 iv2))%R. `````` Heiko Becker committed Oct 04, 2016 281 282 283 284 285 286 287 288 ``````Proof. intros nodiv0 c_a c_b. unfold divideInterval. unfold Rdiv. eapply interval_multiplication_valid; auto. apply interval_inversion_valid; auto. Qed. `````` Heiko Becker committed Sep 07, 2016 289 290 291 ``````Lemma contained_leq_maxAbs a iv: contained a iv -> (Rabs a <= RmaxAbsFun iv)%R. `````` Heiko Becker committed Sep 05, 2016 292 293 294 ``````Proof. intros contained_a. unfold RmaxAbsFun. `````` Heiko Becker committed Jun 29, 2017 295 `````` simpl in contained_a; destruct contained_a. `````` Heiko Becker committed Sep 05, 2016 296 297 298 `````` eapply RmaxAbs; auto. Qed. `````` Heiko Becker committed Sep 07, 2016 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 ``````Lemma contained_leq_maxAbs_val a iv: contained a iv -> (a <= RmaxAbsFun (iv))%R. Proof. intros contained_a; unfold RmaxAbsFun. assert (Rabs a <= RmaxAbsFun iv)%R by (apply contained_leq_maxAbs; auto). eapply Rle_trans. apply Rle_abs. auto. Qed. Lemma contained_leq_maxAbs_neg_val a iv: contained a iv -> (- a <= RmaxAbsFun (iv))%R. Proof. intros contained_a; unfold RmaxAbsFun. assert (Rabs a <= RmaxAbsFun iv)%R by (apply contained_leq_maxAbs; auto). eapply Rle_trans. apply Rle_abs. rewrite Rabs_Ropp. auto. Qed. Lemma distance_gives_iv a b e iv: contained a iv -> (Rabs (a - b) <= e)%R -> contained b (widenInterval iv e). Proof. `````` Heiko Becker committed Jun 29, 2017 327 `````` intros contained_a abs_le; simpl in *. `````` Heiko Becker committed Sep 07, 2016 328 329 `````` destruct contained_a as [lo_a a_hi]. rewrite Rabs_minus_sym in abs_le. `````` Heiko Becker committed Oct 04, 2016 330 `````` unfold Rabs in abs_le. `````` Heiko Becker committed Jan 05, 2017 331 `````` destruct Rcase_abs in abs_le; try lra. `````` Heiko Becker committed Feb 06, 2017 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 ``````Qed. Lemma minAbs_positive_iv_is_lo a b: (0 < a)%R -> (a <= b)%R -> RminAbsFun (a,b) = a. Proof. intros; unfold RminAbsFun; simpl. assert (0 < b)%R by lra. assert (Rabs a = a)%R as Rabs_pos_a by (apply Rabs_right; lra). assert (Rabs b = b)%R as Rabs_pos_b by (apply Rabs_right; lra). rewrite Rabs_pos_a, Rabs_pos_b. rewrite Rmin_left; lra. Qed. Lemma minAbs_negative_iv_is_hi a b: (b < 0)%R -> (a <= b)%R -> (RminAbsFun (a,b) = - b)%R. Proof. intros; unfold RminAbsFun; simpl. assert (Rabs a = - a)%R as Rabs_neg_a by (apply Rabs_left; lra). assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra). rewrite Rabs_neg_a, Rabs_neg_b. rewrite Rmin_right; lra. `````` Nikita Zyuzin committed Oct 23, 2017 357 ``Qed.``