fin_sets.v 16.1 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
(** Operations *)
11
Instance set_size `{Elements A C} : Size C := length  elements.
12

13
Definition set_fold `{Elements A C} {B}
14
  (f : A  B  B) (b : B) : C  B := foldr f b  elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

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

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

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
  fresh  elements.
Typeclasses Opaque set_filter.

(** We generalize the [fresh] operation on sets to generate lists of fresh
elements w.r.t. a set [X]. *)
Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
    (n : nat) (X : C) : list A :=
  match n with
  | 0 => []
  | S n => let x := fresh X in x :: fresh_list n ({[ x ]}  X)
  end.
Instance: Params (@fresh_list) 6 := {}.

(** The following inductive predicate classifies that a list of elements is
in fact fresh w.r.t. a set [X]. *)
Inductive Forall_fresh `{ElemOf A C} (X : C) : list A  Prop :=
  | Forall_fresh_nil : Forall_fresh X []
  | Forall_fresh_cons x xs :
     x  xs  x  X  Forall_fresh X xs  Forall_fresh X (x :: xs).

(** Properties **)
48 49
Section fin_set.
Context `{FinSet A C}.
50
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
Lemma fin_set_finite X : set_finite X.
53
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
54

Robbert Krebbers's avatar
Robbert Krebbers committed
55
Instance elem_of_dec_slow : RelDecision (@{C}) | 100.
56
Proof.
57
  refine (λ x X, cast_if (decide_rel () x (elements X)));
58 59 60 61
    by rewrite <-(elem_of_elements _).
Defined.

(** * The [elements] operation *)
62 63 64 65
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.

66
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
Proof.
  intros ?? E. apply NoDup_Permutation.
69 70 71
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Qed.
73

74 75 76 77 78
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
79 80 81 82 83 84 85 86 87 88 89
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.

90 91 92 93 94 95 96 97 98
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.
99
Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
100 101
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
102
    elements_union_singleton, elements_empty by set_solver.
103
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
105
Proof.
106
  intros; apply NoDup_submseteq; eauto using NoDup_elements.
107 108 109
  intros x. rewrite !elem_of_elements; auto.
Qed.

110
(** * The [size] operation *)
111
Global Instance set_size_proper: Proper (() ==> (=)) (@size C _).
112
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
113

114
Lemma size_empty : size ( : C) = 0.
115
Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
116
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof.
118 119
  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
120
Qed.
121
Lemma size_empty_iff (X : C) : size X = 0  X  .
122
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
123 124
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
125

126
Lemma set_choose_or_empty X : ( x, x  X)  X  .
127
Proof.
128
  destruct (elements X) as [|x l] eqn:HX; [right|left].
129 130
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
131
Qed.
132 133 134 135
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.
136
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
137
Proof.
138
  intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|].
139
  contradict Hsz. rewrite HX, size_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Qed.
141

142
Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
143
Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed.
144 145
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
146
  unfold size, set_size. simpl. rewrite <-!elem_of_elements.
147 148 149
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
150
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
152 153
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
154
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
155
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Qed.
157

158
Lemma size_union X Y : X ## Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Proof.
160
  intros. unfold size, set_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  apply Permutation_length, NoDup_Permutation.
162 163
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
164
    intros x; rewrite !elem_of_elements; set_solver.
165
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
168
Proof.
169 170 171
  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
172
Qed.
173

Robbert Krebbers's avatar
Robbert Krebbers committed
174
Lemma subseteq_size X Y : X  Y  size X  size Y.
175
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
Proof.
178
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181
  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
182
Qed.
183 184

(** * Induction principles *)
185
Lemma set_wf : wf (@{C}).
186
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
187
Lemma set_ind (P : C  Prop) :
188
  Proper (() ==> iff) P 
189
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  intros ? Hemp Hadd. apply well_founded_induction with ().
192 193
  { apply set_wf. }
  intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
194 195
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
196
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Qed.
198
Lemma set_ind_L `{!LeibnizEquiv C} (P : C  Prop) :
199
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
200
Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
201

202 203
(** * 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
204
  Proper ((=) ==> () ==> iff) P 
205
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
206
   X, P (set_fold f b X) X.
Robbert Krebbers's avatar
Robbert Krebbers committed
207 208
Proof.
  intros ? Hemp Hadd.
209
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
210 211
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  induction 1 as [|x l ?? IH]; simpl.
213
  - intros X HX. setoid_rewrite elem_of_nil in HX.
214
    rewrite equiv_empty. done. set_solver.
215
  - intros X HX. setoid_rewrite elem_of_cons in HX.
216 217
    rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
Qed.
219
Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
220
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
221
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
222
  Proper (() ==> R) (set_fold f b : C  B).
223
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
224

225
(** * Minimal elements *)
226
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
227 228
  X     x, x  X  minimal R x X.
Proof.
229
  pattern X; apply set_ind; clear X.
230 231
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
232
  intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
233 234 235
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
236
      eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken.
237
    - exists x'; split; [set_solver|].
238
      eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). }
239 240 241
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
242 243
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
244
  X     x, x  X  minimal R x X.
245
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
246

247
(** * Filter *)
248 249 250 251 252
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.
253 254
    unfold filter, set_filter.
    by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
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
  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.
283

284 285
(** * Map *)
Section map.
286
  Context `{Set_ B D}.
287 288

  Lemma elem_of_map (f : A  B) (X : C) y :
289
    y  set_map (D:=D) f X   x, y = f x  x  X.
290
  Proof.
291
    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
292 293 294 295
    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)) 
296
    SetUnfold (x  set_map (D:=D) f X) ( y, x = f y  P y).
297 298
  Proof. constructor. rewrite elem_of_map; naive_solver. Qed.

299 300
  Global Instance set_map_proper :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
301
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
302 303
  Global Instance set_map_mono :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
304 305 306
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.

  Lemma elem_of_map_1 (f : A  B) (X : C) (y : B) :
307
    y  set_map (D:=D) f X   x, y = f x  x  X.
308 309
  Proof. set_solver. Qed.
  Lemma elem_of_map_2 (f : A  B) (X : C) (x : A) :
310
    x  X  f x  set_map (D:=D) f X.
311 312
  Proof. set_solver. Qed.
  Lemma elem_of_map_2_alt (f : A  B) (X : C) (x : A) (y : B) :
313
    x  X  y = f x  y  set_map (D:=D) f X.
314 315 316
  Proof. set_solver. Qed.
End map.

317
(** * Decision procedures *)
318 319 320 321 322
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.

323
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
324 325
  {set_Forall P X} + {set_Exists Q X}.
Proof.
326
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
327 328 329 330 331
   [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.
332
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
333 334 335
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
336 337
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
338 339 340 341
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
342
Proof.
343 344
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
345
Defined.
346 347
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
348
Proof.
349 350
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
351
Defined.
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368

(** 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.
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422

Section infinite.
  Context `{Infinite A}.

  (** Properties about the [fresh] operation on finite sets *)
  Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
  Proof. unfold fresh, set_fresh. solve_proper. Qed.

  Lemma is_fresh X : fresh X  X.
  Proof.
    unfold fresh, set_fresh. rewrite <-elem_of_elements. apply infinite_is_fresh.
  Qed.
  Lemma exist_fresh X :  x, x  X.
  Proof. exists (fresh X). apply is_fresh. Qed.

  (** Properties about the [fresh_list] operation on finite sets *)
  Global Instance fresh_list_proper n : Proper ((@{C}) ==> (=)) (fresh_list n).
  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.

  Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs  NoDup xs.
  Proof. induction 1; by constructor. Qed.
  Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs  x  xs  x  X.
  Proof.
    intros HX; revert x; rewrite <-Forall_forall. by induction HX; constructor.
  Qed.
  Lemma Forall_fresh_alt X xs :
    Forall_fresh X xs  NoDup xs   x, x  xs  x  X.
  Proof.
    split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of.
    rewrite <-Forall_forall.
    intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
  Qed.
  Lemma Forall_fresh_subseteq X Y xs :
    Forall_fresh X xs  Y  X  Forall_fresh Y xs.
  Proof. rewrite !Forall_fresh_alt; set_solver. Qed.

  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.
  Lemma fresh_list_is_fresh n X x : x  fresh_list n X  x  X.
  Proof.
    revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
    apply IH in Hin; set_solver.
  Qed.
  Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
  Proof.
    revert X. induction n; simpl; constructor; auto.
    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
  Qed.
  Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
  Proof.
    rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh.
  Qed.
End infinite.
423
End fin_set.