IntervalArith.v 12.9 KB
Newer Older
1
2
(**
  Formalization of real valued interval arithmetic
3
  Used in soundness proofs for error bound validator.
4
**)
5
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Heiko Becker's avatar
Heiko Becker committed
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.

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
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.

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.

59
Lemma validPointInterval (a:R) :
60
  contained a (pointInterval a).
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)).

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).

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.

142
143
Definition invertInterval (intv:interval) := mkInterval (/ IVhi intv) (/ IVlo intv).

Heiko Becker's avatar
Heiko Becker committed
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.
158
    + repeat rewrite Ropp_inv_permute; try lra.
Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
190
Definition subtractInterval (I1:interval) (I2:interval) :=
191
192
193
  addInterval I1 (negateInterval I2).

Corollary subtractionIsValid iv1 iv2:
Heiko Becker's avatar
Heiko Becker committed
194
  validIntervalSub iv1 iv2 (subtractInterval iv1 iv2).
195
Proof.
Heiko Becker's avatar
Heiko Becker committed
196
  unfold subtractInterval.
197
198
  intros a b.
  intros contained_1 contained_I2.
Heiko Becker's avatar
Heiko Becker committed
199
  rewrite Rsub_eq_Ropp_Rplus.
200
  apply additionIsValid; auto.
201
  apply interval_negation_valid; auto.
202
203
204
205
206
Qed.

Definition multInterval (iv1:interval) (iv2:interval) :=
  absIntvUpd Rmult iv1 iv2.

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
**)
212
Lemma interval_multiplication_valid (I1:interval) (I2:interval) (a:R) (b:R) :
213
214
215
  contained a I1 ->
  contained b I2 ->
  contained (a * b) (multInterval I1 I2).
216
Proof.
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.

285
286
287
Definition divideInterval (I1:interval) (I2:interval) :=
  multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))).

Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
298
(** Define the maxAbs function on R and prove some minor properties of it. **)
Heiko Becker's avatar
Heiko Becker committed
299
300
Definition RmaxAbsFun (iv:interval) :=
  Rmax (Rabs (fst iv)) (Rabs (snd iv)).
301

Heiko Becker's avatar
Heiko Becker committed
302
303
304
Lemma contained_leq_maxAbs a iv:
  contained a iv ->
  (Rabs a <= RmaxAbsFun iv)%R.
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's avatar
Heiko Becker committed
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:
336
  (Rabs (a - b) <= eps)%R ->
Heiko Becker's avatar
Heiko Becker committed
337
338
  contained a iv ->
  (Rabs b <= Rabs (RmaxAbsFun iv + eps))%R.
339
340
Proof.
  intros Rabs_le_eps contained_a.
Heiko Becker's avatar
Heiko Becker committed
341
  pose proof (contained_leq_maxAbs _ _ contained_a).
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's avatar
Heiko Becker committed
346
    assert (Rabs a + eps <= RmaxAbsFun iv + eps)%R by (apply Rplus_le_compat_r; auto).
347
348
349
    eapply Rle_trans; eauto.
    eapply Rle_trans; eauto.
    apply Rle_abs.
Heiko Becker's avatar
Heiko Becker committed
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's avatar
Heiko Becker committed
373
  unfold Rabs in abs_le.
374
375
376
377
   destruct Rcase_abs in abs_le.
   - rewrite Ropp_minus_distr in abs_le.
     split; lra.
   - lra.
Heiko Becker's avatar
Heiko Becker committed
378
Qed.