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 159
  intros E. destruct (size_pos_elem_of X); auto with lia.
  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
      epose proof (union_minimal (C:=C)); epose proof (singleton_minimal (C:=C)); eauto using minimal_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
264
    - exists x'; split; [set_solver|].
265
      epose proof (union_minimal (C:=C)); epose proof (singleton_minimal_not_above (C:=C)); eauto. }
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 ??; 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.