fin_sets.v 16.9 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
Global Instance set_unfold_elements X x P :
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
  SetUnfoldElemOf x X P  SetUnfoldElemOf x (elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed.
65

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.
Dan Frumin's avatar
Dan Frumin committed
104
105
106
107
108
109
110
111
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
112
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
113
Proof.
114
  intros; apply NoDup_submseteq; eauto using NoDup_elements.
115
116
117
  intros x. rewrite !elem_of_elements; auto.
Qed.

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

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

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

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

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
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.

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

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

308
309
(** * Map *)
Section map.
310
  Context `{Set_ B D}.
311
312

  Lemma elem_of_map (f : A  B) (X : C) y :
313
    y  set_map (D:=D) f X   x, y = f x  x  X.
314
  Proof.
315
    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
316
317
318
    by setoid_rewrite elem_of_elements.
  Qed.
  Global Instance set_unfold_map (f : A  B) (X : C) (P : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
    ( y, SetUnfoldElemOf y X (P y)) 
    SetUnfoldElemOf x (set_map (D:=D) f X) ( y, x = f y  P y).
321
322
  Proof. constructor. rewrite elem_of_map; naive_solver. Qed.

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

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

341
(** * Decision procedures *)
342
343
344
345
346
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.

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

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

(** 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.
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
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446

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