fin_sets.v 17.1 KB
Newer Older
1
(** This file collects definitions and theorems on finite sets. Most
2
importantly, it implements a fold and size function and some useful induction
3
principles on finite sets . *)
4
From stdpp Require Import relations.
5
From stdpp Require Export numbers sets.
6
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
(** Operations *)
9
Instance set_size `{Elements A C} : Size C := length  elements.
10

11
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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 **)
46
47
Section fin_set.
Context `{FinSet A C}.
48
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

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

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

(** * The [elements] operation *)
60
Global Instance set_unfold_elements X x P :
61
62
  SetUnfoldElemOf x X P  SetUnfoldElemOf x (elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed.
63

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

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

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

116
(** * The [size] operation *)
117
Global Instance set_size_proper: Proper (() ==> (=)) (@size C _).
118
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
119

120
Lemma size_empty : size ( : C) = 0.
121
Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
122
Lemma size_empty_inv (X : C) : size X = 0  X  .
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof.
124
125
  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
126
Qed.
127
Lemma size_empty_iff (X : C) : size X = 0  X  .
128
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
131

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Lemma subseteq_size X Y : X  Y  size X  size Y.
181
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Lemma subset_size X Y : X  Y  size X < size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Proof.
184
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
  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
188
Qed.
189
190

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

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

Dan Frumin's avatar
Dan Frumin committed
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
Lemma set_fold_empty {B} (f : A  B  B) (b : B) :
  set_fold f b ( : C) = b.
Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
Lemma set_fold_singleton {B} (f : A  B  B) (b : B) (a : A) :
  set_fold f b ({[a]} : C) = f a b.
Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
Lemma set_fold_disj_union (f : A  A  A) (b : A) X Y :
  Comm (=) f 
  Assoc (=) f 
  X ## Y 
  set_fold f b (X  Y) = set_fold f (set_fold f b X) Y.
Proof.
  intros Hcomm Hassoc Hdisj. unfold set_fold; simpl.
  by rewrite elements_disj_union, <- foldr_app, (comm (++)).
Qed.

252
(** * Minimal elements *)
253
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
  X     x, x  X  minimal R x X.
Proof.
256
  pattern X; apply set_ind; clear X.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
259
  intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
Robbert Krebbers's avatar
Robbert Krebbers committed
260
261
262
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
263
      eapply union_minimal; [eapply singleton_minimal|by eapply minimal_weaken].
Robbert Krebbers's avatar
Robbert Krebbers committed
264
    - exists x'; split; [set_solver|].
265
      by eapply union_minimal; [apply singleton_minimal_not_above|]. }
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
269
270
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  X     x, x  X  minimal R x X.
272
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273

274
(** * Filter *)
275
276
277
278
279
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.
280
281
    unfold filter, set_filter.
    by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
282
283
  Qed.
  Global Instance set_unfold_filter X Q :
284
    SetUnfoldElemOf x X Q  SetUnfoldElemOf x (filter P X) (P x  Q).
285
  Proof.
286
    intros x ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
  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.
310

311
312
(** * Map *)
Section map.
313
  Context `{Set_ B D}.
314
315

  Lemma elem_of_map (f : A  B) (X : C) y :
316
    y  set_map (D:=D) f X   x, y = f x  x  X.
317
  Proof.
318
    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
319
320
321
    by setoid_rewrite elem_of_elements.
  Qed.
  Global Instance set_unfold_map (f : A  B) (X : C) (P : A  Prop) :
322
323
    ( y, SetUnfoldElemOf y X (P y)) 
    SetUnfoldElemOf x (set_map (D:=D) f X) ( y, x = f y  P y).
324
325
  Proof. constructor. rewrite elem_of_map; naive_solver. Qed.

326
327
  Global Instance set_map_proper :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
328
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
329
330
  Global Instance set_map_mono :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (set_map (C:=C) (D:=D)).
331
332
333
  Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.

  Lemma elem_of_map_1 (f : A  B) (X : C) (y : B) :
334
    y  set_map (D:=D) f X   x, y = f x  x  X.
335
336
  Proof. set_solver. Qed.
  Lemma elem_of_map_2 (f : A  B) (X : C) (x : A) :
337
    x  X  f x  set_map (D:=D) f X.
338
339
  Proof. set_solver. Qed.
  Lemma elem_of_map_2_alt (f : A  B) (X : C) (x : A) (y : B) :
340
    x  X  y = f x  y  set_map (D:=D) f X.
341
342
343
  Proof. set_solver. Qed.
End map.

344
(** * Decision procedures *)
345
346
347
348
349
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.

350
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
351
352
  {set_Forall P X} + {set_Exists Q X}.
Proof.
353
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
354
355
356
357
358
   [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.
359
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
360
361
362
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
363
364
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
365
366
367
368
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
369
Proof.
370
371
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
372
Defined.
373
374
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
375
Proof.
376
377
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
378
Defined.
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395

(** 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.
396
397
398
399
400
401

Section infinite.
  Context `{Infinite A}.

  (** Properties about the [fresh] operation on finite sets *)
  Global Instance fresh_proper: Proper ((@{C}) ==> (=)) fresh.
402
  Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449

  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.
450
End fin_set.