IntervalArith.v 12.9 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 Aug 18, 2016 6 ``````Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps. `````` 7 8 9 10 11 12 13 14 15 16 ``````(** 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. **) Definition valid (intv:interval) :Prop := (IVlo intv <= IVhi intv)%R. Definition contained (x:R) (intv:interval) := (IVlo intv <= x <= IVhi intv)%R. `````` Heiko Becker committed Aug 17, 2016 17 ``````Lemma contained_implies_valid (x:R) (intv:interval) : `````` 18 19 20 21 22 23 24 25 `````` contained x intv -> valid intv. Proof. unfold contained, valid; intros inIntv; apply (Rle_trans _ x _); destruct inIntv; auto. Qed. (** Subset definition; when an interval is a subinterval of another `````` Heiko Becker committed Aug 10, 2016 26 ``````**) `````` 27 28 29 30 31 ``````Definition isSupersetInterval (iv1:interval) (iv2:interval) := (IVlo iv2 <= IVlo iv1)%R /\ (IVhi iv1 <= IVhi iv2)%R. Definition pointInterval (x:R) := mkInterval x x. `````` Heiko Becker committed Aug 17, 2016 32 ``````Lemma contained_implies_subset (x:R) (intv:interval): `````` 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 `````` contained x intv -> isSupersetInterval (pointInterval x) intv. Proof. intros containedIntv. unfold contained, isSupersetInterval, pointInterval in *; destruct containedIntv; split; auto. Qed. (** Definition of validity conditions for interval operations, Addition, Subtraction, Multiplication and Division **) Definition validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) := forall a b, contained a iv1 -> contained b iv2 -> contained (a + b) iv3. Definition validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) := forall a b, contained a iv1 -> contained b iv2 -> contained (a - b) iv3. Definition validIntervalMult (iv1:interval) (iv2:interval) (iv3:interval) := forall a b, contained a iv1 -> contained b iv2 -> contained (a * b) iv3. Definition validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) := forall a b, contained a iv1 -> contained b iv2 -> contained (a / b) iv3. `````` Heiko Becker committed Aug 09, 2016 59 ``````Lemma validPointInterval (a:R) : `````` Heiko Becker committed Aug 10, 2016 60 `````` contained a (pointInterval a). `````` Heiko Becker committed Aug 09, 2016 61 62 63 64 ``````Proof. unfold contained; split; simpl; apply Req_le; auto. Qed. `````` 65 66 67 68 69 70 71 72 73 74 75 ``````(** 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 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 106 107 108 109 110 111 112 113 114 115 ``````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. `````` 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 ``````(** Asbtract interval update function, parametric by actual operator applied. **) Definition absIntvUpd (op:R->R->R) (I1:interval) (I2:interval) := ( min4 (op (IVlo I1) (IVlo I2)) (op (IVlo I1) (IVhi I2)) (op (IVhi I1) (IVlo I2)) (op (IVhi I1) (IVhi I2)), max4 (op (IVlo I1) (IVlo I2)) (op (IVlo I1) (IVhi I2)) (op (IVhi I1) (IVlo I2)) (op (IVhi I1) (IVhi I2)) ). Definition widenInterval (Iv:interval) (v:R) := mkInterval (IVlo Iv - v) (IVhi Iv + v). Definition negateInterval (intv:interval) := mkInterval (- IVhi intv) (- IVlo intv). `````` Heiko Becker committed Aug 17, 2016 135 ``````Lemma interval_negation_valid (intv:interval) (a:R) : `````` 136 137 138 139 140 141 `````` contained a intv-> contained (- a) (negateInterval intv). Proof. unfold contained; destruct intv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi]. split; apply Ropp_ge_le_contravar; apply Rle_ge; auto. Qed. `````` Heiko Becker committed Aug 17, 2016 142 143 ``````Definition invertInterval (intv:interval) := mkInterval (/ IVhi intv) (/ IVlo intv). `````` Heiko Becker committed Oct 04, 2016 144 145 146 147 148 149 150 151 152 153 154 155 156 157 ``````Lemma interval_inversion_valid (iv:interval) (a:R) : (IVhi iv < 0 \/ 0 < IVlo iv -> contained a iv -> contained (/ a) (invertInterval iv))%R. Proof. unfold contained; destruct iv as [ivlo ivhi]; simpl; 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 158 `````` + repeat rewrite Ropp_inv_permute; try lra. `````` Heiko Becker committed Oct 04, 2016 159 160 161 162 163 164 165 166 `````` 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. `````` 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 ``````Definition addInterval (iv1:interval) (iv2:interval) := absIntvUpd Rplus iv1 iv2. Lemma additionIsValid iv1 iv2: validIntervalAdd iv1 iv2 (addInterval iv1 iv2). Proof. unfold validIntervalAdd. intros a b. unfold contained, addInterval, absIntvUpd, min4, max4. 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 Sep 07, 2016 190 ``````Definition subtractInterval (I1:interval) (I2:interval) := `````` 191 192 193 `````` addInterval I1 (negateInterval I2). Corollary subtractionIsValid iv1 iv2: `````` Heiko Becker committed Sep 07, 2016 194 `````` validIntervalSub iv1 iv2 (subtractInterval iv1 iv2). `````` 195 ``````Proof. `````` Heiko Becker committed Sep 07, 2016 196 `````` unfold subtractInterval. `````` 197 198 `````` intros a b. intros contained_1 contained_I2. `````` Heiko Becker committed Aug 15, 2016 199 `````` rewrite Rsub_eq_Ropp_Rplus. `````` 200 `````` apply additionIsValid; auto. `````` Heiko Becker committed Aug 17, 2016 201 `````` apply interval_negation_valid; auto. `````` 202 203 204 205 206 ``````Qed. Definition multInterval (iv1:interval) (iv2:interval) := absIntvUpd Rmult iv1 iv2. `````` Heiko Becker committed Aug 10, 2016 207 208 209 210 211 ``````(** 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 Aug 17, 2016 212 ``````Lemma interval_multiplication_valid (I1:interval) (I2:interval) (a:R) (b:R) : `````` Heiko Becker committed Aug 10, 2016 213 214 215 `````` contained a I1 -> contained b I2 -> contained (a * b) (multInterval I1 I2). `````` 216 ``````Proof. `````` Heiko Becker committed Aug 10, 2016 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 274 275 276 277 278 279 280 281 282 `````` unfold contained, multInterval, absIntvUpd, IVlo, IVhi. destruct I1 as [ivlo1 ivhi1]; destruct I2 as [ivlo2 ivhi2]; simpl. 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. `````` 283 284 ``````Qed. `````` Heiko Becker committed Aug 17, 2016 285 286 287 ``````Definition divideInterval (I1:interval) (I2:interval) := multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))). `````` Heiko Becker committed Oct 04, 2016 288 289 290 291 292 293 294 295 296 297 ``````Corollary divisionIsValid a b I1 I2: (IVhi I2 < 0 \/ 0 < IVlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideInterval I1 I2))%R. 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 18, 2016 298 ``````(** Define the maxAbs function on R and prove some minor properties of it. **) `````` Heiko Becker committed Sep 07, 2016 299 300 ``````Definition RmaxAbsFun (iv:interval) := Rmax (Rabs (fst iv)) (Rabs (snd iv)). `````` Heiko Becker committed Sep 05, 2016 301 `````` `````` Heiko Becker committed Sep 07, 2016 302 303 304 ``````Lemma contained_leq_maxAbs a iv: contained a iv -> (Rabs a <= RmaxAbsFun iv)%R. `````` Heiko Becker committed Sep 05, 2016 305 306 307 308 309 310 311 ``````Proof. intros contained_a. unfold RmaxAbsFun. unfold contained in contained_a; simpl in contained_a; destruct contained_a. eapply RmaxAbs; auto. Qed. `````` Heiko Becker committed Sep 07, 2016 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 ``````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 Rabs_error_bounded_maxAbs a b eps iv: `````` Heiko Becker committed Sep 05, 2016 336 `````` (Rabs (a - b) <= eps)%R -> `````` Heiko Becker committed Sep 07, 2016 337 338 `````` contained a iv -> (Rabs b <= Rabs (RmaxAbsFun iv + eps))%R. `````` Heiko Becker committed Sep 05, 2016 339 340 ``````Proof. intros Rabs_le_eps contained_a. `````` Heiko Becker committed Sep 07, 2016 341 `````` pose proof (contained_leq_maxAbs _ _ contained_a). `````` Heiko Becker committed Sep 05, 2016 342 343 344 345 `````` rewrite Rabs_minus_sym in Rabs_le_eps. assert (Rabs b - Rabs a <= eps)%R. - eapply Rle_trans; [apply Rabs_triang_inv | auto]. - assert (Rabs b <= Rabs a + eps)%R by lra. `````` Heiko Becker committed Sep 07, 2016 346 `````` assert (Rabs a + eps <= RmaxAbsFun iv + eps)%R by (apply Rplus_le_compat_r; auto). `````` Heiko Becker committed Sep 05, 2016 347 348 349 `````` eapply Rle_trans; eauto. eapply Rle_trans; eauto. apply Rle_abs. `````` Heiko Becker committed Sep 07, 2016 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 ``````Qed. Lemma lowerbound_iv a ivlo ivhi: contained a (ivlo, ivhi) -> (a >= Rmin (ivlo) (ivhi))%R. Proof. intros contained_a. unfold contained in contained_a; destruct contained_a. assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto). apply Rle_ge. eapply Rle_trans. apply Rmin_l. auto. Qed. Lemma distance_gives_iv a b e iv: contained a iv -> (Rabs (a - b) <= e)%R -> contained b (widenInterval iv e). Proof. intros contained_a abs_le; unfold contained in *; simpl in *. destruct contained_a as [lo_a a_hi]. rewrite Rabs_minus_sym in abs_le. `````` Heiko Becker committed Oct 04, 2016 373 `````` unfold Rabs in abs_le. `````` Heiko Becker committed Oct 05, 2016 374 375 376 377 `````` destruct Rcase_abs in abs_le. - rewrite Ropp_minus_distr in abs_le. split; lra. - lra. `````` Heiko Becker committed Sep 07, 2016 378 ``Qed.``