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 :
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 :
281
    SetUnfoldElemOf x X Q  SetUnfoldElemOf x (filter P X) (P x  Q).
282
  Proof.
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) :
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.