fin_collections.v 11.3 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
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 stdpp Require Import relations.
7
From stdpp Require Export numbers collections.
8
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10
11
12
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

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

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

23
24
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
25

26
Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100.
27
Proof.
28
  refine (λ x X, cast_if (decide_rel () x (elements X)));
29
30
31
32
    by rewrite <-(elem_of_elements _).
Defined.

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

41
42
43
44
45
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
46
47
48
49
50
51
52
53
54
55
56
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.

57
58
59
60
61
62
63
64
65
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.
66
Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
67
68
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
69
    elements_union_singleton, elements_empty by set_solver.
70
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
72
Proof.
73
  intros; apply NoDup_submseteq; eauto using NoDup_elements.
74
75
76
  intros x. rewrite !elem_of_elements; auto.
Qed.

77
(** * The [size] operation *)
78
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
79
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
80

81
Lemma size_empty : size ( : C) = 0.
82
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
83
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof.
85
86
  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
87
Qed.
88
Lemma size_empty_iff (X : C) : size X = 0  X  .
89
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
92

93
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
94
Proof.
95
  destruct (elements X) as [|x l] eqn:HX; [right|left].
96
97
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
98
Qed.
99
100
101
102
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.
103
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
104
Proof.
105
106
  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Qed.
108

109
Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
110
111
112
113
114
115
116
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.
117
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof.
119
120
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
121
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
122
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Qed.
124

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

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

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

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

192
(** * Minimal elements *)
193
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
196
197
198
199
200
201
202
  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|].
203
      eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
    - exists x'; split; [set_solver|].
205
      eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). }
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
209
210
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  X     x, x  X  minimal R x X.
212
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213

214
(** * Filter *)
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
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.
250

251
(** * Decision procedures *)
252
253
254
255
256
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.

257
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
258
259
  {set_Forall P X} + {set_Exists Q X}.
Proof.
260
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
261
262
263
264
265
   [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.
266
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
267
268
269
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
270
271
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
272
273
274
275
Qed.

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