IntervalArithQ.v 12.8 KB
Newer Older
1
(**
2
3
  Formalization of rational valued interval arithmetic
  Used in soundness proofs and computations of range validator.
4
**)
Heiko Becker's avatar
Heiko Becker committed
5
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz.
6
Require Import Coq.ZArith.ZArith.
7
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps.
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
(**
  Define validity of an intv, 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 intv, it must lie between the lower and upper bound.
**)
Definition valid (iv:intv) :Prop :=
  (ivlo iv <= ivhi iv)%Q.

Definition contained (x:Q) (iv:intv) :=
  (ivlo iv <= x <= ivhi iv)%Q.

Lemma contained_implies_valid (x:Q) (iv:intv) :
  contained x iv ->
  valid iv.
Proof.
  unfold contained, valid; intros inIv; apply (Qle_trans _ x _); destruct inIv; auto.
Qed.

(**
  Subset definition; when an intv is a subintv of another
**)
Definition isSupersetIntv (iv1:intv) (iv2:intv) :=
29
  andb (Qleb (ivlo iv2) (ivlo iv1)) (Qleb (ivhi iv1) (ivhi iv2)).
30
31
32
33
34

Definition pointIntv (x:Q) := mkIntv x x.

Lemma contained_implies_subset (x:Q) (iv:intv):
  contained x iv ->
35
  isSupersetIntv (pointIntv x) iv = true.
36
37
Proof.
  intros containedIv.
38
39
40
41
42
43
44
45
46
  unfold contained, isSupersetIntv, pointIntv in *; destruct containedIv.
  apply Is_true_eq_true. apply andb_prop_intro.
  split.
  - apply Qle_bool_iff in H.
    unfold Qleb; simpl in *.
    rewrite H; unfold Is_true; auto.
  - apply Qle_bool_iff in H0.
    unfold Qleb; simpl in *.
    rewrite H0. unfold Is_true; auto.
47
48
Qed.

49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Definition isEqIntv (iv1:intv) (iv2:intv) :=
  (ivlo iv1 == ivlo iv2) /\ (ivhi iv1 == ivhi iv2).

Lemma supIntvAntisym (iv1:intv) (iv2:intv) :
  isSupersetIntv iv1 iv2 = true ->
  isSupersetIntv iv2 iv1 = true ->
  isEqIntv iv1 iv2.
Proof.
  intros incl12 incl21.
  unfold isSupersetIntv in *.
  apply andb_true_iff in incl12.
  apply andb_true_iff in incl21.
  destruct incl12 as [incl12_low incl12_hi].
  destruct incl21 as [incl21_low incl21_hi].
  apply Qle_bool_iff in incl12_low.
  apply Qle_bool_iff in incl12_hi.
  apply Qle_bool_iff in incl21_low.
  apply Qle_bool_iff in incl21_hi.
  split.
  - apply (Qle_antisym (ivlo iv1) (ivlo iv2)); auto.
  - apply (Qle_antisym (ivhi iv1) (ivhi iv2)); auto.
Qed.

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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
(**
  Definition of validity conditions for intv operations, Addition, Subtraction, Multiplication and Division
 **)
Definition validIntvAdd (iv1:intv) (iv2:intv) (iv3:intv) :=
  forall a b, contained a iv1 -> contained b iv2 ->
         contained (a + b) iv3.

Definition validIntvSub (iv1:intv) (iv2:intv) (iv3:intv) :=
  forall a b, contained a iv1 -> contained b iv2 ->
         contained (a - b) iv3.

Definition validIntvMult (iv1:intv) (iv2:intv) (iv3:intv) :=
  forall a b, contained a iv1 -> contained b iv2 ->
         contained (a * b) iv3.

Definition validIntvDiv (iv1:intv) (iv2:intv) (iv3:intv) :=
  forall a b, contained a iv1 -> contained b iv2 ->
         contained (a / b) iv3.

Lemma validPointIntv (a:Q) :
  contained a (pointIntv a).
Proof.
  unfold contained; split; simpl; apply Qle_refl; auto.
Qed.

(**
  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:Q) (b:Q) (c:Q) (d:Q) := Qmin a (Qmin b (Qmin c d)).
Definition max4 (a:Q) (b:Q) (c:Q) (d:Q) := Qmax a (Qmax b (Qmax c d)).

Ltac Qmin_l := intros; apply Q.min_le_iff; left; apply Qle_refl.
Ltac Qmin_r := intros; apply Q.min_le_iff; right; apply Qle_refl.

Lemma min4_correct (a b c d:Q) :
  (let m := min4 a b c d in
   m <= a /\ m <= b /\ m <= c /\ m <= d)%Q.
Proof.
  intros m.
  repeat split; unfold m, min4.
  - Qmin_l.
  - assert (forall c,  Qmin b c <= b)%Q by Qmin_l.
    apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto.
    Qmin_r.

  - assert (Qmin c d <= c)%Q by Qmin_l.
    assert (Qmin b (Qmin c d) <= c)%Q.
    + apply (Qle_trans _ (Qmin c d) _); auto. Qmin_r.
    + apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto. Qmin_r.
  - assert (Qmin c d <= d)%Q by Qmin_r.
    assert (Qmin b (Qmin c d) <= d)%Q.
    + apply (Qle_trans _ (Qmin c d) _); auto. Qmin_r.
    + apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto. Qmin_r.
Qed.

Ltac Qmax_l := intros; apply Q.max_le_iff; left; apply Qle_refl.
Ltac Qmax_r := intros; apply Q.max_le_iff; right; apply Qle_refl.

Lemma max4_correct (a b c d:Q) :
  (let m := max4 a b c d in
   a <= m /\ b <= m /\ c <= m /\ d <= m)%Q.
Proof.
  intros m.
  repeat split; unfold m, max4.
  - Qmax_l.
  - assert (forall c,  b <= Qmax b c)%Q by Qmax_l.
    apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto.
    Qmax_r.
  - assert (c <= Qmax c d)%Q by Qmax_l.
    assert (c <= Qmax b (Qmax c d))%Q.
    + apply (Qle_trans _ (Qmax c d) _); auto. Qmax_r.
    + apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto. Qmax_r.
  - assert (d <= Qmax c d)%Q by Qmax_r.
    assert (d <= Qmax b (Qmax c d))%Q.
    + apply (Qle_trans _ (Qmax c d) _); auto. Qmax_r.
    + apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto. Qmax_r.
Qed.

(**
 Asbtract intv update function, parametric by actual operator applied.
**)
Definition absIvUpd (op:Q->Q->Q) (I1:intv) (I2:intv) :=
  (
    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 widenIntv (Iv:intv) (v:Q) := mkIntv (ivlo Iv - v) (ivhi Iv + v).

Definition negateIntv (iv:intv) := mkIntv (- ivhi iv) (- ivlo iv).

Lemma intv_negation_valid (iv:intv) (a:Q) :
  contained a iv-> contained (- a) (negateIntv iv).
Proof.
  unfold contained; destruct iv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi].
  split; apply Qopp_le_compat; auto.
Qed.

Definition invertIntv (iv:intv) := mkIntv (/ ivhi iv) (/ ivlo iv).

Heiko Becker's avatar
Heiko Becker committed
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
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
(*
Lemma zero_not_contained_cases (iv:intv) :
  ivlo iv <= ivhi iv -> ~ contained 0 iv -> ivhi iv < 0 \/ 0 < ivlo iv.
Proof.
  unfold contained; destruct iv as [lo hi]; simpl; intros.
  hnf in H0; rewrite Decidable.not_and_iff in H0.
  case_eq (lo ?= 0); case_eq (hi ?= 0); intros.
  - exfalso.
    rewrite <- Qeq_alt in H1, H2.
    apply H0; [rewrite H2; auto | rewrite H1; auto]; apply Qle_refl.
  - rewrite <- Qlt_alt in H1.
    rewrite <- Qeq_alt in H2.
    rewrite H2 in H.
    exfalso.
    apply Qle_not_lt in H; auto.
  - rewrite <- Qgt_alt in H1.
    rewrite <- Qeq_alt in H2.
 *)
Lemma Qinv_Qopp_compat (a:Q) :
  / - a = - / a.
Proof.
  unfold Qinv.
  case_eq (Qnum a); intros; unfold Qopp; rewrite H; simpl; auto.
Qed.

Lemma intv_inversion_valid (iv:intv) (a:Q) :
  ivhi iv < 0 \/ 0 < ivlo iv -> contained a iv -> contained (/ a) (invertIntv iv).
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) by (eapply Qle_trans; eauto);
      split.
  - assert (- / a <= - / ivhi).
    + assert (0 < - ivhi) by lra.
      repeat rewrite <- Qinv_Qopp_compat.
      eapply Qle_shift_inv_l; try auto.
      assert (- ivhi <= - a) by lra.
      apply (Qmult_le_r _ 1 (- a)); try lra.
      rewrite Qmult_1_l.
      setoid_rewrite Qmult_comm at 1.
      rewrite Qmult_assoc.
      rewrite Qmult_inv_r; lra.
    + apply Qopp_le_compat in H0;
        repeat rewrite Qopp_involutive in H0; auto.
  - assert (- / ivlo <= - / a).
    +  repeat rewrite <- Qinv_Qopp_compat.
       eapply Qle_shift_inv_l; try lra.
       apply (Qmult_le_r _ _ (- ivlo)); try lra.
       rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
    + apply Qopp_le_compat in H0.
      repeat rewrite Qopp_involutive in H0; auto.
  - apply Qle_shift_inv_l; try lra.
    apply (Qmult_le_r _ _ (ivhi)); try lra.
    rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
  - apply Qle_shift_inv_l; try lra.
    apply (Qmult_le_r _ _ a); try lra.
    rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra.
Qed.

242
243
244
Definition addIntv (iv1:intv) (iv2:intv) :=
  absIvUpd Qplus iv1 iv2.

Heiko Becker's avatar
Heiko Becker committed
245
Lemma interval_addition_valid iv1 iv2:
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
  validIntvAdd iv1 iv2 (addIntv iv1 iv2).
Proof.
  unfold validIntvAdd.
  intros a b.
  unfold contained, addIntv, absIvUpd, 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)%Q as lower_bound by (apply Qplus_le_compat; auto).
    apply (Qle_trans _ (fst iv1 + fst iv2) _); [Qmin_l | auto].
  (** Upper Bound **)
  - assert (a + b <= snd iv1 + snd iv2)%Q as upper_bound by (apply Qplus_le_compat; auto).
    apply (Qle_trans _ (snd iv1 + snd iv2) _); [ auto | ].
    apply (Qle_trans _ (Qmax (fst iv1 + snd iv2) (Qmax (snd iv1 + fst iv2) (snd iv1 + snd iv2))) _);
      [ | Qmax_r].
    apply (Qle_trans _ (Qmax (snd iv1 + fst iv2) (snd iv1 + snd iv2)) _ ); [ | Qmax_r].
    apply (Qle_trans _ (snd iv1 + snd iv2) _); [ apply Qle_refl; auto | Qmax_r].
Qed.

265
Definition subtractIntv (I1:intv) (I2:intv) :=
266
267
  addIntv I1 (negateIntv I2).

Heiko Becker's avatar
Heiko Becker committed
268
Corollary interval_subtraction_valid iv1 iv2:
269
  validIntvSub iv1 iv2 (subtractIntv iv1 iv2).
270
Proof.
271
  unfold subtractIntv.
272
273
274
  intros a b.
  intros contained_1 contained_I2.
  rewrite Qsub_eq_Qopp_Qplus.
Heiko Becker's avatar
Heiko Becker committed
275
  apply interval_addition_valid; auto.
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
  apply intv_negation_valid; auto.
Qed.

Definition multIntv (iv1:intv) (iv2:intv) :=
  absIvUpd Qmult iv1 iv2.

(**
  Prove validity of multiplication for the intv lattice.
  Prove is structurally the same as the proof done Jourdan et al. in Verasco, in FloatIntvsForward.v
  TODO: Credit
 **)
Lemma intv_multiplication_valid (I1:intv) (I2:intv) (a:Q) (b:Q) :
  contained a I1 ->
  contained b I2 ->
  contained (a * b) (multIntv I1 I2).
Proof.
  unfold contained, multIntv, absIvUpd, 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 (Qlt_le_dec a 0).
    + apply Qlt_le_weak in q.
      destruct (Qlt_le_dec ivhi2 0).
      * apply Qlt_le_weak in  q0.
305
306
        pose proof (Qmult_le_compat_neg_l q b_leq_hi) as ahi2_leq_ab.
        pose proof (Qmult_le_compat_neg_l q0 a_leq_hi) as hihi_leq_ahi2.
307
308
309
310
311
312
313
314
315
316
317
318
319
        eapply Qle_trans.
        apply leq_hihi. rewrite Qmult_comm.
        eapply Qle_trans. apply hihi_leq_ahi2.
        rewrite Qmult_comm; auto.
      * eapply Qle_trans.
        apply leq_lohi.
        setoid_rewrite Qmult_comm at 1 2.
        pose proof (Qmult_le_compat_r ivlo1 a ivhi2 lo_leq_a q0).
        rewrite Qmult_comm.
        eapply (Qle_trans).
        apply H; auto.
        rewrite Qmult_comm.
        setoid_rewrite Qmult_comm at 1 2.
320
        eapply (Qmult_le_compat_neg_l); auto.
321
322
323
324
325
326
    + destruct (Qlt_le_dec ivlo2 0).
      * eapply Qle_trans.
        apply leq_hilo.
        rewrite Qmult_comm.
        eapply Qle_trans.
        apply Qlt_le_weak in q0.
327
        apply (Qmult_le_compat_neg_l q0 a_leq_hi).
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
        rewrite Qmult_comm.
        setoid_rewrite Qmult_comm at 1 2.
        eapply (Qmult_le_compat_r _ _ a); auto.
      * eapply Qle_trans.
        apply leq_lolo.
        rewrite Qmult_comm.
        apply (Qle_trans _ (ivlo2 * a)).
        setoid_rewrite Qmult_comm at 1 2.
        eapply (Qmult_le_compat_r _ _ ivlo2 ); auto.
        rewrite Qmult_comm.
        setoid_rewrite Qmult_comm at 1 2.
        eapply (Qmult_le_compat_r _ _ a); auto.
  - destruct (Qlt_le_dec a 0).
    + apply Qlt_le_weak in q.
      eapply Qle_trans.
343
      eapply (Qmult_le_compat_neg_l); eauto.
344
345
346
      destruct (Qlt_le_dec ivlo2 0).
      * rewrite Qmult_comm.
        eapply Qle_trans.
347
        eapply (Qmult_le_compat_neg_l); eauto.
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
        apply Qlt_le_weak; auto.
        rewrite Qmult_comm; auto.
      * eapply Qle_trans.
        eapply (Qmult_le_compat_r _ _ ivlo2); auto.
        apply a_leq_hi.
        apply hilo_leq.
    + rewrite Qmult_comm.
      eapply Qle_trans.
      eapply (Qmult_le_compat_r); auto.
      apply b_leq_hi.
      destruct (Qlt_le_dec ivhi2 0).
      * eapply Qle_trans.
        eapply (Qmult_le_compat_neg_l); auto.
        apply Qlt_le_weak; auto.
        apply lo_leq_a.
        rewrite Qmult_comm; auto.
      * eapply Qle_trans.
        rewrite Qmult_comm.
        eapply (Qmult_le_compat_r); auto.
        apply a_leq_hi.
        apply hihi_leq.
Qed.

Definition divideIntv (I1:intv) (I2:intv) :=
Heiko Becker's avatar
Heiko Becker committed
372
373
  multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).

Heiko Becker's avatar
Heiko Becker committed
374
Corollary interval_division_valid a b (I1:intv) (I2:intv) :
Heiko Becker's avatar
Heiko Becker committed
375
376
377
  ivhi I2 < 0 \/ 0 < ivlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideIntv I1 I2).
Proof.
  intros nodiv0 c_a c_b.
378
  pose proof (intv_inversion_valid nodiv0 c_b).
Heiko Becker's avatar
Heiko Becker committed
379
380
381
  unfold divideIntv, Qdiv.
  apply intv_multiplication_valid; auto.
Qed.