fin_collections.v 9.31 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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
7
8
From Coq Require Import Permutation.
From stdpp Require Import relations listset.
From stdpp Require Export numbers collections.
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
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)).

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

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

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 *)
32
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
Proof.
  intros ?? E. apply NoDup_Permutation.
35
36
37
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
Qed.
39

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

56
57
58
59
60
61
62
63
64
65
66
67
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]}),
68
    elements_union_singleton, elements_empty by set_solver.
69
70
71
72
73
74
75
Qed.
Lemma elements_contains X Y : X  Y  elements X `contains` elements Y.
Proof.
  intros; apply NoDup_contains; auto using NoDup_elements.
  intros x. rewrite !elem_of_elements; auto.
Qed.

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

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

92
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
93
Proof.
94
  destruct (elements X) as [|x l] eqn:HX; [right|left].
95
96
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
97
Qed.
98
99
100
101
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.
102
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
103
Proof.
104
105
  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
106
Qed.
107
108
109
110
111
112
113
114
115

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
140
Lemma subseteq_size X Y : X  Y  size X  size Y.
141
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Proof.
144
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
147
  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
148
Qed.
149
150

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

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

191
(** * Minimal elements *)
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
Lemma minimal_exists `{!StrictOrder R,  x y, Decision (R x y)} (X : C) :
  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.
Lemma minimal_exists_L
    `{!LeibnizEquiv C, !StrictOrder R,  x y, Decision (R x y)} (X : C) :
  X     x, x  X  minimal R x X.
Proof. unfold_leibniz. apply minimal_exists. Qed.

213
214
215
216
217
218
219
220
(** * Filter *)
Lemma elem_of_filter (P : A  Prop) `{! x, Decision (P x)} 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.

221
(** * Decision procedures *)
222
223
Global Instance set_Forall_dec `(P : A  Prop)
  `{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
224
225
Proof.
  refine (cast_if (decide (Forall P (elements X))));
226
    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
227
      by rewrite <-Forall_forall).
228
Defined.
229
230
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
231
232
Proof.
  refine (cast_if (decide (Exists P (elements X))));
233
    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
234
      by rewrite <-Exists_exists).
235
Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
End fin_collection.