fin_collections.v 11.3 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
6
From Coq Require Import Permutation.
7
8
From iris.prelude Require Import relations listset.
From iris.prelude Require Export numbers collections.
9
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
13
14

Instance collection_size `{Elements A C} : Size C := length  elements.
Definition collection_fold `{Elements A C} {B}
  (f : A  B  B) (b : B) : C  B := foldr f b  elements.

15
16
17
Instance collection_filter
    `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
  of_list (filter P (elements X)).
18
Typeclasses Opaque collection_filter.
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
Section fin_collection.
Context `{FinCollection A C}.
22
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
23

24
25
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
26
27
28
29
30
31
32
33

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
  refine (cast_if (decide_rel () x (elements X)));
    by rewrite <-(elem_of_elements _).
Defined.

(** * The [elements] operation *)
34
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
Proof.
  intros ?? E. apply NoDup_Permutation.
37
38
39
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Qed.
41

42
43
44
45
46
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
47
48
49
50
51
52
53
54
55
56
57
Lemma elements_empty_inv X : elements X = []  X  .
Proof.
  intros HX; apply elem_of_equiv_empty; intros x.
  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
Qed.
Lemma elements_empty' X : elements X = []  X  .
Proof.
  split; intros HX; [by apply elements_empty_inv|].
  by rewrite <-Permutation_nil, HX, elements_empty.
Qed.

58
59
60
61
62
63
64
65
66
67
68
69
Lemma elements_union_singleton (X : C) x :
  x  X  elements ({[ x ]}  X)  x :: elements X.
Proof.
  intros ?; apply NoDup_Permutation.
  { apply NoDup_elements. }
  { by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
  intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
  by rewrite elem_of_cons, elem_of_elements.
Qed.
Lemma elements_singleton x : elements {[ x ]} = [x].
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
70
    elements_union_singleton, elements_empty by set_solver.
71
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
73
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  intros; apply NoDup_submseteq; auto using NoDup_elements.
75
76
77
  intros x. rewrite !elem_of_elements; auto.
Qed.

78
(** * The [size] operation *)
79
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
81

Robbert Krebbers's avatar
Robbert Krebbers committed
82
Lemma size_empty : size ( : C) = 0.
83
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
Lemma size_empty_inv (X : C) : size X = 0  X  .
Proof.
86
87
  intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
  by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
Qed.
Lemma size_empty_iff (X : C) : size X = 0  X  .
90
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
93

Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
Proof.
  destruct (elements X) as [|x l] eqn:HX; [right|left].
97
98
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
107
108
Qed.
Lemma collection_choose X : X     x, x  X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X     x, x  X.
Proof. unfold_leibniz. apply collection_choose. Qed.
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
Proof.
  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Qed.
109
110
111
112
113
114
115
116
117

Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
121
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Proof.
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
122
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
123
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Qed.
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
Lemma size_union X Y : X  Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  intros. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  apply Permutation_length, NoDup_Permutation.
130
131
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
132
    intros x; rewrite !elem_of_elements; set_solver.
133
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
136
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
Proof.
137
138
139
  rewrite <-size_union by set_solver.
  setoid_replace (Y  X) with ((Y  X)  X) by set_solver.
  rewrite <-union_difference, (comm ()); set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Qed.
141

Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
Lemma subseteq_size X Y : X  Y  size X  size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X  Y  size X < size Y.
Proof.
146
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
149
150
  rewrite size_union_alt, difference_twice.
  cut (size (Y  X)  0); [lia |].
  by apply size_non_empty_iff, non_empty_difference.
Qed.
151
152

(** * Induction principles *)
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
158
159
160
161
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C  Prop) :
  Proper (() ==> iff) P 
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof.
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
162
163
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
164
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Qed.
166
167
168
Lemma collection_ind_L `{!LeibnizEquiv C} (P : C  Prop) :
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
169
170

(** * The [collection_fold] operation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
173
174
175
176
177
178
179
180
Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
   X, P (collection_fold f b X) X.
Proof.
  intros ? Hemp Hadd.
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
  induction 1 as [|x l ?? IH]; simpl.
181
  - intros X HX. setoid_rewrite elem_of_nil in HX.
182
    rewrite equiv_empty. done. set_solver.
183
  - intros X HX. setoid_rewrite elem_of_cons in HX.
184
185
    rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
190
  Proper (() ==> R) (collection_fold f b : C  B).
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
192

193
(** * Minimal elements *)
194
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
  X     x, x  X  minimal R x X.
Proof.
  pattern X; apply collection_ind; clear X.
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
  intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX].
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
      eauto using union_minimal, singleton_minimal, minimal_weaken.
    - exists x'; split; [set_solver|].
      auto using union_minimal, singleton_minimal_not_above. }
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
210
211
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  X     x, x  X  minimal R x X.
213
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
214

215
(** * Filter *)
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
Section filter.
  Context (P : A  Prop) `{! x, Decision (P x)}.

  Lemma elem_of_filter X x : x  filter P X  P x  x  X.
  Proof.
    unfold filter, collection_filter.
    by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
  Qed.
  Global Instance set_unfold_filter X Q :
    SetUnfold (x  X) Q  SetUnfold (x  filter P X) (P x  Q).
  Proof.
    intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x  X) Q).
  Qed.

  Lemma filter_empty : filter P (:C)  .
  Proof. set_solver. Qed.
  Lemma filter_union X Y : filter P (X  Y)  filter P X  filter P Y.
  Proof. set_solver. Qed.
  Lemma filter_singleton x : P x  filter P ({[ x ]} : C)  {[ x ]}.
  Proof. set_solver. Qed.
  Lemma filter_singleton_not x : ¬P x  filter P ({[ x ]} : C)  .
  Proof. set_solver. Qed.

  Section leibniz_equiv.
    Context `{!LeibnizEquiv C}.
    Lemma filter_empty_L : filter P (:C) = .
    Proof. set_solver. Qed.
    Lemma filter_union_L X Y : filter P (X  Y) = filter P X  filter P Y.
    Proof. set_solver. Qed.
    Lemma filter_singleton_L x : P x  filter P ({[ x ]} : C) = {[ x ]}.
    Proof. set_solver. Qed.
    Lemma filter_singleton_not_L x : ¬P x  filter P ({[ x ]} : C) = .
    Proof. set_solver. Qed.
  End leibniz_equiv.
End filter.
251

252
(** * Decision procedures *)
253
254
255
256
257
Lemma set_Forall_elements P X : set_Forall P X  Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
Lemma set_Exists_elements P X : set_Exists P X  Exists P (elements X).
Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed.

258
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
259
260
  {set_Forall P X} + {set_Exists Q X}.
Proof.
261
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
262
263
264
265
266
   [by apply set_Forall_elements|by apply set_Exists_elements].
Defined.

Lemma not_set_Forall_Exists P `{dec :  x, Decision (P x)} X :
  ¬set_Forall P X  set_Exists (not  P) X.
267
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
268
269
270
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
271
272
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
273
274
275
276
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
Proof.
278
279
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
282
283
Defined.
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
Proof.
284
285
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Defined.
End fin_collection.