fin_sets.v 13.2 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
(** This file collects definitions and theorems on finite sets. Most
4
importantly, it implements a fold and size function and some useful induction
5
principles on finite sets . *)
6
From stdpp Require Import relations.
7
From stdpp Require Export numbers sets.
8
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10 11
Instance set_size `{Elements A C} : Size C := length  elements.
Definition set_fold `{Elements A C} {B}
12
  (f : A  B  B) (b : B) : C  B := foldr f b  elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

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

19
Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
20
    (f : A  B) (X : C) : D :=
21 22
  list_to_set (f <$> elements X).
Typeclasses Opaque set_map.
23

24 25
Section fin_set.
Context `{FinSet A C}.
26
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28
Lemma fin_set_finite X : set_finite X.
29
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
30

Robbert Krebbers's avatar
Robbert Krebbers committed
31
Instance elem_of_dec_slow : RelDecision (@{C}) | 100.
32
Proof.
33
  refine (λ x X, cast_if (decide_rel () x (elements X)));
34 35 36 37
    by rewrite <-(elem_of_elements _).
Defined.

(** * The [elements] operation *)
38 39 40 41
Global Instance set_unfold_elements X x P :
  SetUnfold (x  X) P  SetUnfold (x  elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold (x  X) P). Qed.

42
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
Proof.
  intros ?? E. apply NoDup_Permutation.
45 46 47
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Qed.
49

50 51 52 53 54
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
55 56 57 58 59 60 61 62 63 64 65
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.

66 67 68 69 70 71 72 73 74
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.
75
Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
76 77
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
78
    elements_union_singleton, elements_empty by set_solver.
79
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
81
Proof.
82
  intros; apply NoDup_submseteq; eauto using NoDup_elements.
83 84 85
  intros x. rewrite !elem_of_elements; auto.
Qed.

86
(** * The [size] operation *)
87
Global Instance set_size_proper: Proper (() ==> (=)) (@size C _).
88
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
89

90
Lemma size_empty : size ( : C) = 0.
91
Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
92
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof.
94 95
  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
96
Qed.
97
Lemma size_empty_iff (X : C) : size X = 0  X  .
98
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
101

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

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

134
Lemma size_union X Y : X ## Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
136
  intros. unfold size, set_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
  apply Permutation_length, NoDup_Permutation.
138 139
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
140
    intros x; rewrite !elem_of_elements; set_solver.
141
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
144
Proof.
145 146 147
  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
148
Qed.
149

Robbert Krebbers's avatar
Robbert Krebbers committed
150
Lemma subseteq_size X Y : X  Y  size X  size Y.
151
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof.
154
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
  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
158
Qed.
159 160

(** * Induction principles *)
161
Lemma set_wf : wf (@{C}).
162
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
163
Lemma set_ind (P : C  Prop) :
164
  Proper (() ==> iff) P 
165
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  intros ? Hemp Hadd. apply well_founded_induction with ().
168 169
  { apply set_wf. }
  intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
170 171
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
172
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Qed.
174
Lemma set_ind_L `{!LeibnizEquiv C} (P : C  Prop) :
175
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
176
Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
177

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

201
(** * Minimal elements *)
202
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204
  X     x, x  X  minimal R x X.
Proof.
205
  pattern X; apply set_ind; clear X.
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
208
  intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210 211
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
212
      eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
    - exists x'; split; [set_solver|].
214
      eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). }
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
218 219
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  X     x, x  X  minimal R x X.
221
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
222

223
(** * Filter *)
224 225 226 227 228
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.
229 230
    unfold filter, set_filter.
    by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
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
  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.
259

260 261
(** * Map *)
Section map.
262
  Context `{Set_ B D}.
263 264

  Lemma elem_of_map (f : A  B) (X : C) y :
265
    y  set_map (D:=D) f X   x, y = f x  x  X.
266
  Proof.
267
    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
268 269 270 271
    by setoid_rewrite elem_of_elements.
  Qed.
  Global Instance set_unfold_map (f : A  B) (X : C) (P : A  Prop) :
    ( y, SetUnfold (y  X) (P y)) 
272
    SetUnfold (x  set_map (D:=D) f X) ( y, x = f y  P y).
273 274
  Proof. constructor. rewrite elem_of_map; naive_solver. Qed.

275 276
  Global Instance set_map_proper :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
277
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
278 279
  Global Instance set_map_mono :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
280 281 282
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.

  Lemma elem_of_map_1 (f : A  B) (X : C) (y : B) :
283
    y  set_map (D:=D) f X   x, y = f x  x  X.
284 285
  Proof. set_solver. Qed.
  Lemma elem_of_map_2 (f : A  B) (X : C) (x : A) :
286
    x  X  f x  set_map (D:=D) f X.
287 288
  Proof. set_solver. Qed.
  Lemma elem_of_map_2_alt (f : A  B) (X : C) (x : A) (y : B) :
289
    x  X  y = f x  y  set_map (D:=D) f X.
290 291 292
  Proof. set_solver. Qed.
End map.

293
(** * Decision procedures *)
294 295 296 297 298
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.

299
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
300 301
  {set_Forall P X} + {set_Exists Q X}.
Proof.
302
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
303 304 305 306 307
   [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.
308
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
309 310 311
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
312 313
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
314 315 316 317
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
318
Proof.
319 320
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
321
Defined.
322 323
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
324
Proof.
325 326
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
327
Defined.
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344

(** Alternative versions of finite and infinite predicates *)
Lemma pred_finite_set (P : A  Prop) :
  pred_finite P  ( X : C,  x, P x  x  X).
Proof.
  split.
  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
  - intros [X Hfin]. exists (elements X). set_solver.
Qed.

Lemma pred_infinite_set (P : A  Prop) :
  pred_infinite P  ( X : C,  x, P x  x  X).
Proof.
  split.
  - intros Hinf X. destruct (Hinf (elements X)). set_solver.
  - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver.
Qed.
345
End fin_set.