1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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
59
60
61
62
63
64
65
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
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
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
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
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Definitions and theorems about semi-open integer intervals *)
Require Import Coqlib.
Require Import Zwf.
Require Coq.Program.Wf.
Require Recdef.
Definition interv : Type := (Z * Z)%type.
(** * Membership *)
Definition In (x: Z) (i: interv) : Prop := fst i <= x < snd i.
Lemma In_dec:
forall x i, {In x i} + {~In x i}.
Proof.
unfold In; intros.
case (zle (fst i) x); intros.
case (zlt x (snd i)); intros.
left; auto.
right; intuition.
right; intuition.
Qed.
Lemma notin_range:
forall x i,
x < fst i \/ x >= snd i -> ~In x i.
Proof.
unfold In; intros; omega.
Qed.
Lemma range_notin:
forall x i,
~In x i -> fst i < snd i -> x < fst i \/ x >= snd i.
Proof.
unfold In; intros; omega.
Qed.
(** * Emptyness *)
Definition empty (i: interv) : Prop := fst i >= snd i.
Lemma empty_dec:
forall i, {empty i} + {~empty i}.
Proof.
unfold empty; intros.
case (zle (snd i) (fst i)); intros.
left; omega.
right; omega.
Qed.
Lemma is_notempty:
forall i, fst i < snd i -> ~empty i.
Proof.
unfold empty; intros; omega.
Qed.
Lemma empty_notin:
forall x i, empty i -> ~In x i.
Proof.
unfold empty, In; intros. omega.
Qed.
Lemma in_notempty:
forall x i, In x i -> ~empty i.
Proof.
unfold empty, In; intros. omega.
Qed.
(** * Disjointness *)
Definition disjoint (i j: interv) : Prop :=
forall x, In x i -> ~In x j.
Lemma disjoint_sym:
forall i j, disjoint i j -> disjoint j i.
Proof.
unfold disjoint; intros; red; intros. elim (H x); auto.
Qed.
Lemma empty_disjoint_r:
forall i j, empty j -> disjoint i j.
Proof.
unfold disjoint; intros. apply empty_notin; auto.
Qed.
Lemma empty_disjoint_l:
forall i j, empty i -> disjoint i j.
Proof.
intros. apply disjoint_sym. apply empty_disjoint_r; auto.
Qed.
Lemma disjoint_range:
forall i j,
snd i <= fst j \/ snd j <= fst i -> disjoint i j.
Proof.
unfold disjoint, In; intros. omega.
Qed.
Lemma range_disjoint:
forall i j,
disjoint i j ->
empty i \/ empty j \/ snd i <= fst j \/ snd j <= fst i.
Proof.
unfold disjoint, empty; intros.
destruct (zlt (fst i) (snd i)); auto.
destruct (zlt (fst j) (snd j)); auto.
right; right.
destruct (zlt (fst i) (fst j)).
(* Case 1: i starts to the left of j. *)
destruct (zle (snd i) (fst j)).
(* Case 1.1: i ends to the left of j, OK *)
auto.
(* Case 1.2: i ends to the right of j's start, not disjoint. *)
elim (H (fst j)). red; omega. red; omega.
(* Case 2: j starts to the left of i *)
destruct (zle (snd j) (fst i)).
(* Case 2.1: j ends to the left of i, OK *)
auto.
(* Case 2.2: j ends to the right of i's start, not disjoint. *)
elim (H (fst i)). red; omega. red; omega.
Qed.
Lemma range_disjoint':
forall i j,
disjoint i j -> fst i < snd i -> fst j < snd j ->
snd i <= fst j \/ snd j <= fst i.
Proof.
intros. exploit range_disjoint; eauto. unfold empty; intuition omega.
Qed.
Lemma disjoint_dec:
forall i j, {disjoint i j} + {~disjoint i j}.
Proof.
intros.
destruct (empty_dec i). left; apply empty_disjoint_l; auto.
destruct (empty_dec j). left; apply empty_disjoint_r; auto.
destruct (zle (snd i) (fst j)). left; apply disjoint_range; auto.
destruct (zle (snd j) (fst i)). left; apply disjoint_range; auto.
right; red; intro. exploit range_disjoint; eauto. intuition.
Qed.
(** * Shifting an interval by some amount *)
Definition shift (i: interv) (delta: Z) : interv := (fst i + delta, snd i + delta).
Lemma in_shift:
forall x i delta,
In x i -> In (x + delta) (shift i delta).
Proof.
unfold shift, In; intros. simpl. omega.
Qed.
Lemma in_shift_inv:
forall x i delta,
In x (shift i delta) -> In (x - delta) i.
Proof.
unfold shift, In; simpl; intros. omega.
Qed.
(** * Enumerating the elements of an interval *)
Section ELEMENTS.
Variable lo: Z.
Function elements_rec (hi: Z) {wf (Zwf lo) hi} : list Z :=
if zlt lo hi then (hi-1) :: elements_rec (hi-1) else nil.
Proof.
intros. red. omega.
apply Zwf_well_founded.
Qed.
Lemma In_elements_rec:
forall hi x,
List.In x (elements_rec hi) <-> lo <= x < hi.
Proof.
intros. functional induction (elements_rec hi).
simpl; split; intros.
destruct H. clear IHl. omega. rewrite IHl in H. clear IHl. omega.
destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. omega.
simpl; intuition.
Qed.
End ELEMENTS.
Definition elements (i: interv) : list Z :=
elements_rec (fst i) (snd i).
Lemma in_elements:
forall x i,
In x i -> List.In x (elements i).
Proof.
intros. unfold elements. rewrite In_elements_rec. auto.
Qed.
Lemma elements_in:
forall x i,
List.In x (elements i) -> In x i.
Proof.
unfold elements; intros.
rewrite In_elements_rec in H. auto.
Qed.
(** * Checking properties on all elements of an interval *)
Section FORALL.
Variables P Q: Z -> Prop.
Variable f: forall (x: Z), {P x} + {Q x}.
Variable lo: Z.
Program Fixpoint forall_rec (hi: Z) {wf (Zwf lo) hi}:
{forall x, lo <= x < hi -> P x}
+ {exists x, lo <= x < hi /\ Q x} :=
if zlt lo hi then
match f (hi - 1) with
| left _ =>
match forall_rec (hi - 1) with
| left _ => left _ _
| right _ => right _ _
end
| right _ => right _ _
end
else
left _ _
.
Next Obligation.
red. omega.
Qed.
Next Obligation.
assert (x = hi - 1 \/ x < hi - 1) by omega.
destruct H2. congruence. auto.
Qed.
Next Obligation.
exists wildcard'0; split; auto. omega.
Qed.
Next Obligation.
exists (hi - 1); split; auto. omega.
Qed.
Next Obligation.
omegaContradiction.
Defined.
End FORALL.
Definition forall_dec
(P Q: Z -> Prop) (f: forall (x: Z), {P x} + {Q x}) (i: interv) :
{forall x, In x i -> P x} + {exists x, In x i /\ Q x} :=
forall_rec P Q f (fst i) (snd i).
(** * Folding a function over all elements of an interval *)
Section FOLD.
Variable A: Type.
Variable f: Z -> A -> A.
Variable lo: Z.
Variable a: A.
Function fold_rec (hi: Z) {wf (Zwf lo) hi} : A :=
if zlt lo hi then f (hi - 1) (fold_rec (hi - 1)) else a.
Proof.
intros. red. omega.
apply Zwf_well_founded.
Qed.
Lemma fold_rec_elements:
forall hi, fold_rec hi = List.fold_right f a (elements_rec lo hi).
Proof.
intros. functional induction (fold_rec hi).
rewrite elements_rec_equation. rewrite zlt_true; auto.
simpl. congruence.
rewrite elements_rec_equation. rewrite zlt_false; auto.
Qed.
End FOLD.
Definition fold {A: Type} (f: Z -> A -> A) (a: A) (i: interv) : A :=
fold_rec A f (fst i) a (snd i).
Lemma fold_elements:
forall (A: Type) (f: Z -> A -> A) a i,
fold f a i = List.fold_right f a (elements i).
Proof.
intros. unfold fold, elements. apply fold_rec_elements.
Qed.
(** Hints *)
Hint Resolve
notin_range range_notin
is_notempty empty_notin in_notempty
disjoint_sym empty_disjoint_r empty_disjoint_l
disjoint_range
in_shift in_shift_inv
in_elements elements_in : intv.
|
