sets.v 50.2 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 sets. Most
4
importantly, it implements some tactics to automatically solve goals involving
5
sets. *)
6
From stdpp Require Export orders list.
7 8
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
   everywhere makes for lots of extra ssumptions. *)
9

10 11
(* Higher precedence to make sure these instances are not used for other types
with an [ElemOf] instance, such as lists. *)
12
Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
13
   x, x  X  x  Y.
14
Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
15
   x, x  X  x  Y.
16
Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
17
   x, x  X  x  Y  False.
18
Typeclasses Opaque set_equiv set_subseteq set_disjoint.
19

20 21
(** * Setoids *)
Section setoids_simple.
22
  Context `{SemiSet A C}.
Robbert Krebbers's avatar
Robbert Krebbers committed
23

24
  Global Instance set_equiv_equivalence : Equivalence (@{C}).
25
  Proof.
26 27 28 29
    split.
    - done.
    - intros X Y ? x. by symmetry.
    - intros X Y Z ?? x; by trans (x  Y).
30
  Qed.
31
  Global Instance singleton_proper : Proper ((=) ==> (@{C})) singleton.
32
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  Global Instance elem_of_proper : Proper ((=) ==> () ==> iff) (@{C}) | 5.
34
  Proof. by intros x ? <- X Y. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  Global Instance disjoint_proper: Proper (() ==> () ==> iff) (##@{C}).
36
  Proof.
37
    intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
38
  Qed.
39
  Global Instance union_proper : Proper (() ==> () ==> (@{C})) union.
40
  Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed.
41
  Global Instance union_list_proper: Proper (() ==> (@{C})) union_list.
42
  Proof. by induction 1; simpl; try apply union_proper. Qed.
43
  Global Instance subseteq_proper : Proper ((@{C}) ==> (@{C}) ==> iff) ().
44 45 46 47 48 49
  Proof.
    intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
  Qed.
End setoids_simple.

Section setoids.
50
  Context `{Set_ A C}.
51

52 53
  (** * Setoids *)
  Global Instance intersection_proper :
54
    Proper (() ==> () ==> (@{C})) intersection.
55
  Proof.
56
    intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
57
  Qed.
58
  Global Instance difference_proper :
59
     Proper (() ==> () ==> (@{C})) difference.
60
  Proof.
61
    intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
62
  Qed.
63
End setoids.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

65
Section setoids_monad.
66
  Context `{MonadSet M}.
67

68
  Global Instance set_fmap_proper {A B} :
69
    Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
70
  Proof.
71 72
    intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_fmap. f_equiv; intros z.
    by rewrite HX, Hf.
73
  Qed.
74
  Global Instance set_bind_proper {A B} :
75
    Proper (pointwise_relation _ () ==> () ==> ()) (@mbind M _ A B).
76 77
  Proof.
    intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_bind. f_equiv; intros z.
78
    by rewrite HX, (Hf z).
79
  Qed.
80
  Global Instance set_join_proper {A} :
81 82 83 84 85
    Proper (() ==> ()) (@mjoin M _ A).
  Proof.
    intros X1 X2 HX x. rewrite !elem_of_join. f_equiv; intros z. by rewrite HX.
  Qed.
End setoids_monad.
86

87 88 89 90 91
(** * Tactics *)
(** The tactic [set_unfold] transforms all occurrences of [(∪)], [(∩)], [(∖)],
[(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)] into logically equivalent propositions
involving just [∈]. For example, [A → x ∈ X ∪ ∅] becomes [A → x ∈ X ∨ False].

92 93 94
This transformation is implemented using type classes instead of setoid
rewriting to ensure that we traverse each term at most once and to be able to
deal with occurences of the set operations under binders. *)
95
Class SetUnfold (P Q : Prop) := { set_unfold : P  Q }.
96
Arguments set_unfold _ _ {_} : assert.
97 98
Hint Mode SetUnfold + - : typeclass_instances.

99 100 101 102 103 104 105 106 107 108 109 110 111 112
(** The class [SetUnfoldElemOf] is a more specialized version of [SetUnfold]
for propositions of the shape [x ∈ X] to improve performance. *)
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
  { set_unfold_elem_of : x  X  Q }.
Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.

Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
  SetUnfoldElemOf x X (x  X) | 1000.
Proof. done. Qed.
Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
  SetUnfoldElemOf x X Q  SetUnfold (x  X) Q.
Proof. by destruct 1; constructor. Qed.

113 114 115
Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.

116
Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
Definition set_unfold_1 `{SetUnfold P Q} : P  Q := proj1 (set_unfold P Q).
Definition set_unfold_2 `{SetUnfold P Q} : Q  P := proj2 (set_unfold P Q).

Lemma set_unfold_impl P Q P' Q' :
  SetUnfold P P'  SetUnfold Q Q'  SetUnfold (P  Q) (P'  Q').
Proof. constructor. by rewrite (set_unfold P P'), (set_unfold Q Q'). Qed.
Lemma set_unfold_and P Q P' Q' :
  SetUnfold P P'  SetUnfold Q Q'  SetUnfold (P  Q) (P'  Q').
Proof. constructor. by rewrite (set_unfold P P'), (set_unfold Q Q'). Qed.
Lemma set_unfold_or P Q P' Q' :
  SetUnfold P P'  SetUnfold Q Q'  SetUnfold (P  Q) (P'  Q').
Proof. constructor. by rewrite (set_unfold P P'), (set_unfold Q Q'). Qed.
Lemma set_unfold_iff P Q P' Q' :
  SetUnfold P P'  SetUnfold Q Q'  SetUnfold (P  Q) (P'  Q').
Proof. constructor. by rewrite (set_unfold P P'), (set_unfold Q Q'). Qed.
Lemma set_unfold_not P P' : SetUnfold P P'  SetUnfold (¬P) (¬P').
Proof. constructor. by rewrite (set_unfold P P'). Qed.
Lemma set_unfold_forall {A} (P P' : A  Prop) :
  ( x, SetUnfold (P x) (P' x))  SetUnfold ( x, P x) ( x, P' x).
Proof. constructor. naive_solver. Qed.
Lemma set_unfold_exist {A} (P P' : A  Prop) :
  ( x, SetUnfold (P x) (P' x))  SetUnfold ( x, P x) ( x, P' x).
Proof. constructor. naive_solver. Qed.

(* Avoid too eager application of the above instances (and thus too eager
unfolding of type class transparent definitions). *)
Hint Extern 0 (SetUnfold (_  _) _) =>
  class_apply set_unfold_impl : typeclass_instances.
Hint Extern 0 (SetUnfold (_  _) _) =>
  class_apply set_unfold_and : typeclass_instances.
Hint Extern 0 (SetUnfold (_  _) _) =>
  class_apply set_unfold_or : typeclass_instances.
Hint Extern 0 (SetUnfold (_  _) _) =>
  class_apply set_unfold_iff : typeclass_instances.
Hint Extern 0 (SetUnfold (¬ _) _) =>
  class_apply set_unfold_not : typeclass_instances.
Hint Extern 1 (SetUnfold ( _, _) _) =>
  class_apply set_unfold_forall : typeclass_instances.
Hint Extern 0 (SetUnfold ( _, _) _) =>
  class_apply set_unfold_exist : typeclass_instances.

Section set_unfold_simple.
159
  Context `{SemiSet A C}.
160 161 162
  Implicit Types x y : A.
  Implicit Types X Y : C.

163
  Global Instance set_unfold_empty x : SetUnfoldElemOf x ( : C) False.
164
  Proof. constructor. split. apply not_elem_of_empty. done. Qed.
165
  Global Instance set_unfold_singleton x y : SetUnfoldElemOf x ({[ y ]} : C) (x = y).
166 167
  Proof. constructor; apply elem_of_singleton. Qed.
  Global Instance set_unfold_union x X Y P Q :
168 169
    SetUnfoldElemOf x X P  SetUnfoldElemOf x Y Q 
    SetUnfoldElemOf x (X  Y) (P  Q).
170 171
  Proof.
    intros ??; constructor.
172 173
    by rewrite elem_of_union,
      (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
174 175 176 177
  Qed.
  Global Instance set_unfold_equiv_same X : SetUnfold (X  X) True | 1.
  Proof. done. Qed.
  Global Instance set_unfold_equiv_empty_l X (P : A  Prop) :
178
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold (  X) ( x, ¬P x) | 5.
179
  Proof.
180
    intros ?; constructor. unfold equiv, set_equiv.
181
    pose proof (not_elem_of_empty (C:=C)); naive_solver.
182
  Qed.
183
  Global Instance set_unfold_equiv_empty_r (P : A  Prop) X :
184
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold (X  ) ( x, ¬P x) | 5.
185
  Proof.
186
    intros ?; constructor. unfold equiv, set_equiv.
187
    pose proof (not_elem_of_empty (C:=C)); naive_solver.
188
  Qed.
189
  Global Instance set_unfold_equiv (P Q : A  Prop) X :
190
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
191
    SetUnfold (X  Y) ( x, P x  Q x) | 10.
192
  Proof. constructor. apply forall_proper; naive_solver. Qed.
193
  Global Instance set_unfold_subseteq (P Q : A  Prop) X Y :
194
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
195
    SetUnfold (X  Y) ( x, P x  Q x).
196
  Proof. constructor. apply forall_proper; naive_solver. Qed.
197
  Global Instance set_unfold_subset (P Q : A  Prop) X :
198
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
199
    SetUnfold (X  Y) (( x, P x  Q x)  ¬∀ x, Q x  P x).
200
  Proof.
201 202
    constructor. unfold strict.
    repeat f_equiv; apply forall_proper; naive_solver.
203
  Qed.
204
  Global Instance set_unfold_disjoint (P Q : A  Prop) X Y :
205
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
206
    SetUnfold (X ## Y) ( x, P x  Q x  False).
207
  Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
208 209 210 211 212

  Context `{!LeibnizEquiv C}.
  Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
  Proof. done. Qed.
  Global Instance set_unfold_equiv_empty_l_L X (P : A  Prop) :
213
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold ( = X) ( x, ¬P x) | 5.
214
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed.
215
  Global Instance set_unfold_equiv_empty_r_L (P : A  Prop) X :
216
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold (X = ) ( x, ¬P x) | 5.
217
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed.
218
  Global Instance set_unfold_equiv_L (P Q : A  Prop) X Y :
219
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
220
    SetUnfold (X = Y) ( x, P x  Q x) | 10.
221
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed.
222 223 224
End set_unfold_simple.

Section set_unfold.
225
  Context `{Set_ A C}.
226 227 228 229
  Implicit Types x y : A.
  Implicit Types X Y : C.

  Global Instance set_unfold_intersection x X Y P Q :
230 231
    SetUnfoldElemOf x X P  SetUnfoldElemOf x Y Q 
    SetUnfoldElemOf x (X  Y) (P  Q).
232
  Proof.
233
    intros ??; constructor. rewrite elem_of_intersection.
234
    by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
235 236
  Qed.
  Global Instance set_unfold_difference x X Y P Q :
237 238
    SetUnfoldElemOf x X P  SetUnfoldElemOf x Y Q 
    SetUnfoldElemOf x (X  Y) (P  ¬Q).
239
  Proof.
240
    intros ??; constructor. rewrite elem_of_difference.
241
    by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
242 243 244 245
  Qed.
End set_unfold.

Section set_unfold_monad.
246
  Context `{MonadSet M}.
247

248
  Global Instance set_unfold_ret {A} (x y : A) :
249
    SetUnfoldElemOf x (mret (M:=M) y) (x = y).
250
  Proof. constructor; apply elem_of_ret. Qed.
251
  Global Instance set_unfold_bind {A B} (f : A  M B) X (P Q : A  Prop) :
252 253
    ( y, SetUnfoldElemOf y X (P y))  ( y, SetUnfoldElemOf x (f y) (Q y)) 
    SetUnfoldElemOf x (X = f) ( y, Q y  P y).
254
  Proof. constructor. rewrite elem_of_bind; naive_solver. Qed.
255
  Global Instance set_unfold_fmap {A B} (f : A  B) (X : M A) (P : A  Prop) :
256 257
    ( y, SetUnfoldElemOf y X (P y)) 
    SetUnfoldElemOf x (f <$> X) ( y, x = f y  P y).
258
  Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed.
259
  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A  Prop) :
260 261
    ( Y, SetUnfoldElemOf Y X (P Y)) 
    SetUnfoldElemOf x (mjoin X) ( Y, x  Y  P Y).
262 263 264
  Proof. constructor. rewrite elem_of_join; naive_solver. Qed.
End set_unfold_monad.

265 266 267 268 269
Section set_unfold_list.
  Context {A : Type}.
  Implicit Types x : A.
  Implicit Types l : list A.

270
  Global Instance set_unfold_nil x : SetUnfoldElemOf x [] False.
271 272
  Proof. constructor; apply elem_of_nil. Qed.
  Global Instance set_unfold_cons x y l P :
273 274
    SetUnfoldElemOf x l P  SetUnfoldElemOf x (y :: l) (x = y  P).
  Proof. constructor. by rewrite elem_of_cons, (set_unfold_elem_of x l P). Qed.
275
  Global Instance set_unfold_app x l k P Q :
276 277
    SetUnfoldElemOf x l P  SetUnfoldElemOf x k Q 
    SetUnfoldElemOf x (l ++ k) (P  Q).
278 279
  Proof.
    intros ??; constructor.
280
    by rewrite elem_of_app, (set_unfold_elem_of x l P), (set_unfold_elem_of x k Q).
281 282
  Qed.
  Global Instance set_unfold_included l k (P Q : A  Prop) :
283
    ( x, SetUnfoldElemOf x l (P x))  ( x, SetUnfoldElemOf x k (Q x)) 
284 285 286 287 288
    SetUnfold (l  k) ( x, P x  Q x).
  Proof.
    constructor; unfold subseteq, list_subseteq.
    apply forall_proper; naive_solver.
  Qed.
289 290 291 292 293 294 295 296 297 298 299 300

  Global Instance set_unfold_reverse x l P :
    SetUnfoldElemOf x l P  SetUnfoldElemOf x (reverse l) P.
  Proof. constructor. by rewrite elem_of_reverse, (set_unfold_elem_of x l P). Qed.

  Global Instance set_unfold_list_fmap {B} (f : A  B) l P :
    ( y, SetUnfoldElemOf y l (P y)) 
    SetUnfoldElemOf x (f <$> l) ( y, x = f y  P y).
  Proof.
    constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
    by rewrite (set_unfold_elem_of y l (P y)).
  Qed.
301 302
End set_unfold_list.

303 304 305
Ltac set_unfold :=
  let rec unfold_hyps :=
    try match goal with
306 307 308 309 310 311 312
    | H : ?P |- _ =>
       lazymatch type of P with
       | Prop =>
         apply set_unfold_1 in H; revert H;
         first [unfold_hyps; intros H | intros H; fail 1]
       | _ => fail
       end
313 314 315
    end in
  apply set_unfold_2; unfold_hyps; csimpl in *.

316 317
(** Since [firstorder] already fails or loops on very small goals generated by
[set_solver], we use the [naive_solver] tactic as a substitute. *)
318
Tactic Notation "set_solver" "by" tactic3(tac) :=
319
  try fast_done;
320 321 322 323 324 325 326 327 328 329 330 331 332
  intros; setoid_subst;
  set_unfold;
  intros; setoid_subst;
  try match goal with |- _  _ => apply dec_stable end;
  naive_solver tac.
Tactic Notation "set_solver" "-" hyp_list(Hs) "by" tactic3(tac) :=
  clear Hs; set_solver by tac.
Tactic Notation "set_solver" "+" hyp_list(Hs) "by" tactic3(tac) :=
  clear -Hs; set_solver by tac.
Tactic Notation "set_solver" := set_solver by idtac.
Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.

333 334 335 336
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.

337

338 339 340
(** * Sets with [∪], [∅] and [{[_]}] *)
Section semi_set.
  Context `{SemiSet A C}.
341 342 343 344 345 346 347
  Implicit Types x y : A.
  Implicit Types X Y : C.
  Implicit Types Xs Ys : list C.

  (** Equality *)
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. set_solver. Qed.
348
  Lemma set_equiv_spec X Y : X  Y  X  Y  Y  X.
349 350 351
  Proof. set_solver. Qed.

  (** Subset relation *)
352
  Global Instance set_subseteq_antisymm: AntiSymm () (@{C}).
353 354
  Proof. intros ??. set_solver. Qed.

355
  Global Instance set_subseteq_preorder: PreOrder (@{C}).
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
  Proof. split. by intros ??. intros ???; set_solver. Qed.

  Lemma subseteq_union X Y : X  Y  X  Y  Y.
  Proof. set_solver. Qed.
  Lemma subseteq_union_1 X Y : X  Y  X  Y  Y.
  Proof. by rewrite subseteq_union. Qed.
  Lemma subseteq_union_2 X Y : X  Y  Y  X  Y.
  Proof. by rewrite subseteq_union. Qed.

  Lemma union_subseteq_l X Y : X  X  Y.
  Proof. set_solver. Qed.
  Lemma union_subseteq_r X Y : Y  X  Y.
  Proof. set_solver. Qed.
  Lemma union_least X Y Z : X  Z  Y  Z  X  Y  Z.
  Proof. set_solver. Qed.

  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
  Proof. done. Qed.
  Lemma elem_of_subset X Y : X  Y  ( x, x  X  x  Y)  ¬( x, x  Y  x  X).
  Proof. set_solver. Qed.

  (** Union *)
378 379
  Lemma union_subseteq X Y Z : X  Y  Z  X  Z  Y  Z.
  Proof. set_solver. Qed.
380 381 382 383 384 385
  Lemma not_elem_of_union x X Y : x  X  Y  x  X  x  Y.
  Proof. set_solver. Qed.
  Lemma elem_of_union_l x X Y : x  X  x  X  Y.
  Proof. set_solver. Qed.
  Lemma elem_of_union_r x X Y : x  Y  x  X  Y.
  Proof. set_solver. Qed.
386
  Lemma union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
387
  Proof. set_solver. Qed.
388
  Lemma union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
389
  Proof. set_solver. Qed.
390
  Lemma union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
391 392
  Proof. set_solver. Qed.

393
  Global Instance union_idemp : IdemP (@{C}) ().
394
  Proof. intros X. set_solver. Qed.
395
  Global Instance union_empty_l : LeftId (@{C})  ().
396
  Proof. intros X. set_solver. Qed.
397
  Global Instance union_empty_r : RightId (@{C})  ().
398
  Proof. intros X. set_solver. Qed.
399
  Global Instance union_comm : Comm (@{C}) ().
400
  Proof. intros X Y. set_solver. Qed.
401
  Global Instance union_assoc : Assoc (@{C}) ().
402 403 404 405 406
  Proof. intros X Y Z. set_solver. Qed.

  Lemma empty_union X Y : X  Y    X    Y  .
  Proof. set_solver. Qed.

407
  Lemma union_cancel_l X Y Z : Z ## X  Z ## Y  Z  X  Z  Y  X  Y.
408
  Proof. set_solver. Qed.
409
  Lemma union_cancel_r X Y Z : X ## Z  Y ## Z  X  Z  Y  Z  X  Y.
410 411
  Proof. set_solver. Qed.

412
  (** Empty *)
Robbert Krebbers's avatar
Robbert Krebbers committed
413 414
  Lemma empty_subseteq X :   X.
  Proof. set_solver. Qed.
415 416
  Lemma elem_of_equiv_empty X : X     x, x  X.
  Proof. set_solver. Qed.
417
  Lemma elem_of_empty x : x  ( : C)  False.
418 419 420 421 422 423 424 425 426 427 428
  Proof. set_solver. Qed.
  Lemma equiv_empty X : X    X  .
  Proof. set_solver. Qed.
  Lemma union_positive_l X Y : X  Y    X  .
  Proof. set_solver. Qed.
  Lemma union_positive_l_alt X Y : X    X  Y  .
  Proof. set_solver. Qed.
  Lemma non_empty_inhabited x X : x  X  X  .
  Proof. set_solver. Qed.

  (** Singleton *)
429
  Lemma elem_of_singleton_1 x y : x  ({[y]} : C)  x = y.
430
  Proof. by rewrite elem_of_singleton. Qed.
431
  Lemma elem_of_singleton_2 x y : x = y  x  ({[y]} : C).
432 433 434 435 436
  Proof. by rewrite elem_of_singleton. Qed.
  Lemma elem_of_subseteq_singleton x X : x  X  {[ x ]}  X.
  Proof. set_solver. Qed.
  Lemma non_empty_singleton x : ({[ x ]} : C)  .
  Proof. set_solver. Qed.
437
  Lemma not_elem_of_singleton x y : x  ({[ y ]} : C)  x  y.
438 439 440
  Proof. by rewrite elem_of_singleton. Qed.

  (** Disjointness *)
441
  Lemma elem_of_disjoint X Y : X ## Y   x, x  X  x  Y  False.
442 443
  Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
444
  Global Instance disjoint_sym : Symmetric (##@{C}).
445
  Proof. intros X Y. set_solver. Qed.
446
  Lemma disjoint_empty_l Y :  ## Y.
447
  Proof. set_solver. Qed.
448
  Lemma disjoint_empty_r X : X ## .
449
  Proof. set_solver. Qed.
450
  Lemma disjoint_singleton_l x Y : {[ x ]} ## Y  x  Y.
451
  Proof. set_solver. Qed.
452
  Lemma disjoint_singleton_r y X : X ## {[ y ]}  y  X.
453
  Proof. set_solver. Qed.
454
  Lemma disjoint_union_l X1 X2 Y : X1  X2 ## Y  X1 ## Y  X2 ## Y.
455
  Proof. set_solver. Qed.
456
  Lemma disjoint_union_r X Y1 Y2 : X ## Y1  Y2  X ## Y1  X ## Y2.
457 458 459 460
  Proof. set_solver. Qed.

  (** Big unions *)
  Lemma elem_of_union_list Xs x : x   Xs   X, X  Xs  x  X.
461 462
  Proof.
    split.
463 464
    - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
      setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
Ralf Jung's avatar
Ralf Jung committed
465
    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
466
      intros. apply elem_of_union_r; auto.
467
  Qed.
468

469 470 471 472 473 474 475
  Lemma union_list_nil :  @nil C = .
  Proof. done. Qed.
  Lemma union_list_cons X Xs :  (X :: Xs) = X   Xs.
  Proof. done. Qed.
  Lemma union_list_singleton X :  [X]  X.
  Proof. simpl. by rewrite (right_id  _). Qed.
  Lemma union_list_app Xs1 Xs2 :  (Xs1 ++ Xs2)   Xs1   Xs2.
476
  Proof.
477 478
    induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id  _)|].
    by rewrite IH, (assoc _).
479
  Qed.
480
  Lemma union_list_reverse Xs :  (reverse Xs)   Xs.
481
  Proof.
482 483 484
    induction Xs as [|X Xs IH]; simpl; [done |].
    by rewrite reverse_cons, union_list_app,
      union_list_singleton, (comm _), IH.
485
  Qed.
486 487
  Lemma union_list_mono Xs Ys : Xs * Ys   Xs   Ys.
  Proof. induction 1; simpl; auto using union_mono. Qed.
488
  Lemma empty_union_list Xs :  Xs    Forall (. ) Xs.
489
  Proof.
490 491 492
    split.
    - induction Xs; simpl; rewrite ?empty_union; intuition.
    - induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
493
  Qed.
494

495 496 497 498 499
  Section leibniz.
    Context `{!LeibnizEquiv C}.

    Lemma elem_of_equiv_L X Y : X = Y   x, x  X  x  Y.
    Proof. unfold_leibniz. apply elem_of_equiv. Qed.
500 501
    Lemma set_equiv_spec_L X Y : X = Y  X  Y  Y  X.
    Proof. unfold_leibniz. apply set_equiv_spec. Qed.
502 503

    (** Subset relation *)
504
    Global Instance set_subseteq_partialorder : PartialOrder (@{C}).
505 506 507 508 509 510 511 512 513 514
    Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.

    Lemma subseteq_union_L X Y : X  Y  X  Y = Y.
    Proof. unfold_leibniz. apply subseteq_union. Qed.
    Lemma subseteq_union_1_L X Y : X  Y  X  Y = Y.
    Proof. unfold_leibniz. apply subseteq_union_1. Qed.
    Lemma subseteq_union_2_L X Y : X  Y = Y  X  Y.
    Proof. unfold_leibniz. apply subseteq_union_2. Qed.

    (** Union *)
515
    Global Instance union_idemp_L : IdemP (=@{C}) ().
516
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
517
    Global Instance union_empty_l_L : LeftId (=@{C})  ().
518
    Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
519
    Global Instance union_empty_r_L : RightId (=@{C})  ().
520
    Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
521
    Global Instance union_comm_L : Comm (=@{C}) ().
522
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
523
    Global Instance union_assoc_L : Assoc (=@{C}) ().
524 525 526 527 528
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.

    Lemma empty_union_L X Y : X  Y =   X =   Y = .
    Proof. unfold_leibniz. apply empty_union. Qed.

529
    Lemma union_cancel_l_L X Y Z : Z ## X  Z ## Y  Z  X = Z  Y  X = Y.
530
    Proof. unfold_leibniz. apply union_cancel_l. Qed.
531
    Lemma union_cancel_r_L X Y Z : X ## Z  Y ## Z  X  Z = Y  Z  X = Y.
532 533
    Proof. unfold_leibniz. apply union_cancel_r. Qed.

534 535 536 537 538 539 540 541 542 543 544 545 546
    (** Empty *)
    Lemma elem_of_equiv_empty_L X : X =    x, x  X.
    Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
    Lemma equiv_empty_L X : X    X = .
    Proof. unfold_leibniz. apply equiv_empty. Qed.
    Lemma union_positive_l_L X Y : X  Y =   X = .
    Proof. unfold_leibniz. apply union_positive_l. Qed.
    Lemma union_positive_l_alt_L X Y : X    X  Y  .
    Proof. unfold_leibniz. apply union_positive_l_alt. Qed.
    Lemma non_empty_inhabited_L x X : x  X  X  .
    Proof. unfold_leibniz. apply non_empty_inhabited. Qed.

    (** Singleton *)
547
    Lemma non_empty_singleton_L x : {[ x ]}  ( : C).
548 549 550 551 552 553 554 555 556
    Proof. unfold_leibniz. apply non_empty_singleton. Qed.

    (** Big unions *)
    Lemma union_list_singleton_L X :  [X] = X.
    Proof. unfold_leibniz. apply union_list_singleton. Qed.
    Lemma union_list_app_L Xs1 Xs2 :  (Xs1 ++ Xs2) =  Xs1   Xs2.
    Proof. unfold_leibniz. apply union_list_app. Qed.
    Lemma union_list_reverse_L Xs :  (reverse Xs) =  Xs.
    Proof. unfold_leibniz. apply union_list_reverse. Qed.
557
    Lemma empty_union_list_L Xs :  Xs =   Forall (.= ) Xs.
558 559 560 561
    Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
  End leibniz.

  Section dec.
562
    Context `{!RelDecision (@{C})}.
563
    Lemma set_subseteq_inv X Y : X  Y  X  Y  X  Y.
564
    Proof. destruct (decide (X  Y)); [by right|left;set_solver]. Qed.
565
    Lemma set_not_subset_inv X Y : X  Y  X  Y  X  Y.
566 567 568 569
    Proof. destruct (decide (X  Y)); [by right|left;set_solver]. Qed.

    Lemma non_empty_union X Y : X  Y    X    Y  .
    Proof. rewrite empty_union. destruct (decide (X  )); intuition. Qed.
570
    Lemma non_empty_union_list Xs :  Xs    Exists (. ) Xs.
571 572 573
    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.

    Context `{!LeibnizEquiv C}.
574 575 576 577
    Lemma set_subseteq_inv_L X Y : X  Y  X  Y  X = Y.
    Proof. unfold_leibniz. apply set_subseteq_inv. Qed.
    Lemma set_not_subset_inv_L X Y : X  Y  X  Y  X = Y.
    Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
578 579
    Lemma non_empty_union_L X Y : X  Y    X    Y  .
    Proof. unfold_leibniz. apply non_empty_union. Qed.
580
    Lemma non_empty_union_list_L Xs :  Xs    Exists (. ) Xs.
581 582
    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
  End dec.
583
End semi_set.
584 585


586 587 588
(** * Sets with [∪], [∩], [∖], [∅] and [{[_]}] *)
Section set.
  Context `{Set_ A C}.
589
  Implicit Types x y : A.
590
  Implicit Types X Y : C.
591

592 593 594 595 596 597 598 599 600 601 602 603 604 605 606
  (** Intersection *)
  Lemma subseteq_intersection X Y : X  Y  X  Y  X.
  Proof. set_solver. Qed. 
  Lemma subseteq_intersection_1 X Y : X  Y  X  Y  X.
  Proof. apply subseteq_intersection. Qed.
  Lemma subseteq_intersection_2 X Y : X  Y  X  X  Y.
  Proof. apply subseteq_intersection. Qed.

  Lemma intersection_subseteq_l X Y : X  Y  X.
  Proof. set_solver. Qed.
  Lemma intersection_subseteq_r X Y : X  Y  Y.
  Proof. set_solver. Qed.
  Lemma intersection_greatest X Y Z : Z  X  Z  Y  Z  X  Y.
  Proof. set_solver. Qed.

607
  Lemma intersection_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
608
  Proof. set_solver. Qed.
609
  Lemma intersection_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
610
  Proof. set_solver. Qed.
611
  Lemma intersection_mono X1 X2 Y1 Y2 :
612
    X1  X2  Y1  Y2  X1  Y1  X2  Y2.
613
  Proof. set_solver. Qed.
614

615
  Global Instance intersection_idemp : IdemP (@{C}) ().
616
  Proof. intros X; set_solver. Qed.
617
  Global Instance intersection_comm : Comm (@{C}) ().
618
  Proof. intros X Y; set_solver. Qed.
619
  Global Instance intersection_assoc : Assoc (@{C}) ().
620
  Proof. intros X Y Z; set_solver. Qed.
621
  Global Instance intersection_empty_l : LeftAbsorb (@{C})  ().
622
  Proof. intros X; set_solver. Qed.
623
  Global Instance intersection_empty_r: RightAbsorb (@{C})  ().
624 625
  Proof. intros X; set_solver. Qed.

626
  Lemma intersection_singletons x : ({[x]} : C)  {[x]}  {[x]}.
627
  Proof. set_solver. Qed.
628 629 630 631 632 633 634 635 636 637 638

  Lemma union_intersection_l X Y Z : X  (Y  Z)  (X  Y)  (X  Z).
  Proof. set_solver. Qed.
  Lemma union_intersection_r X Y Z : (X  Y)  Z  (X  Z)  (Y  Z).
  Proof. set_solver. Qed.
  Lemma intersection_union_l X Y Z : X  (Y  Z)  (X  Y)  (X  Z).
  Proof. set_solver. Qed.
  Lemma intersection_union_r X Y Z : (X  Y)  Z  (X  Z)  (Y  Z).
  Proof. set_solver. Qed.

  (** Difference *)
639
  Lemma difference_twice X Y : (X  Y)  Y  X  Y.
640
  Proof. set_solver. Qed.
641
  Lemma subseteq_empty_difference X Y : X  Y  X  Y  .
642
  Proof. set_solver. Qed.
643
  Lemma difference_diag X : X  X  .
644
  Proof. set_solver. Qed.
645 646
  Lemma difference_empty X : X    X.
  Proof. set_solver. Qed.
647
  Lemma difference_union_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
648
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
  Lemma difference_union_distr_r X Y Z : Z  (X  Y)  (Z  X)  (Z  Y).
650
  Proof. set_solver. Qed.
651
  Lemma difference_intersection_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
652
  Proof. set_solver. Qed.
653
  Lemma difference_disjoint X Y : X ## Y  X  Y  X.
654
  Proof. set_solver. Qed.
655 656
  Lemma subset_difference_elem_of {x: A} {s: C} (inx: x  s): s  {[ x ]}  s.
  Proof. set_solver. Qed.
657 658
  Lemma difference_difference X Y Z : (X  Y)  Z  X  (Y  Z).
  Proof. set_solver. Qed.
659

660
  Lemma difference_mono X1 X2 Y1 Y2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
661 662
    X1  X2  Y2  Y1  X1  Y1  X2  Y2.
  Proof. set_solver. Qed.
663
  Lemma difference_mono_l X Y1 Y2 : Y2  Y1  X  Y1  X  Y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
664
  Proof. set_solver. Qed.
665
  Lemma difference_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
666 667
  Proof. set_solver. Qed.

668 669 670 671 672 673
  Lemma subseteq_difference_r X Y1 Y2 :
    X ## Y2  X  Y1  X  Y1  Y2.
  Proof. set_solver. Qed.
  Lemma subseteq_difference_l X1 X2 Y : X1  Y  X1  X2  Y.
  Proof. set_solver. Qed.

674
  (** Disjointness *)
675
  Lemma disjoint_intersection X Y : X ## Y  X  Y  .
676
  Proof. set_solver. Qed.
677
  Lemma disjoint_difference_l1 X1 X2 Y : Y  X2  X1  X2 ## Y.
678
  Proof. set_solver. Qed.
679 680 681 682 683
  Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y  X1  X2 ## Y.
  Proof. set_solver. Qed.
  Lemma disjoint_difference_r1 X Y1 Y2 : X  Y2  X ## Y1  Y2.
  Proof. set_solver. Qed.
  Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1  X ## Y1  Y2.
684
  Proof. set_solver. Qed.
685

686 687
  Section leibniz.
    Context `{!LeibnizEquiv C}.
688 689 690 691 692 693 694 695 696

    (** Intersection *)
    Lemma subseteq_intersection_L X Y : X  Y  X  Y = X.
    Proof. unfold_leibniz. apply subseteq_intersection. Qed.
    Lemma subseteq_intersection_1_L X Y : X  Y  X  Y = X.
    Proof. unfold_leibniz. apply subseteq_intersection_1. Qed.
    Lemma subseteq_intersection_2_L X Y : X  Y = X  X  Y.
    Proof. unfold_leibniz. apply subseteq_intersection_2. Qed.

697
    Global Instance intersection_idemp_L : IdemP (=@{C}) ().
698
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
699
    Global Instance intersection_comm_L : Comm (=@{C}) ().
700
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
701
    Global Instance intersection_assoc_L : Assoc (=@{C}) ().
702
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
703
    Global Instance intersection_empty_l_L: LeftAbsorb (=@{C})  ().
704
    Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
705
    Global Instance intersection_empty_r_L: RightAbsorb (=@{C})  ().
706 707
    Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.

708
    Lemma intersection_singletons_L x : {[x]}  {[x]} = ({[x]} : C).
709
    Proof. unfold_leibniz. apply intersection_singletons. Qed.
710 711 712 713 714

    Lemma union_intersection_l_L X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
    Proof. unfold_leibniz; apply union_intersection_l. Qed.
    Lemma union_intersection_r_L X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
    Proof. unfold_leibniz; apply union_intersection_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
    Lemma intersection_union_l_L X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
716
    Proof. unfold_leibniz; apply intersection_union_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
717
    Lemma intersection_union_r_L X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
718 719 720
    Proof. unfold_leibniz; apply intersection_union_r. Qed.

    (** Difference *)
721 722
    Lemma difference_twice_L X Y : (X  Y)  Y = X  Y.
    Proof. unfold_leibniz. apply difference_twice. Qed.
723 724
    Lemma subseteq_empty_difference_L X Y : X  Y  X  Y = .
    Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
725 726
    Lemma difference_diag_L X : X  X = .
    Proof. unfold_leibniz. apply difference_diag. Qed.
727 728
    Lemma difference_empty_L X : X   = X.
    Proof. unfold_leibniz. apply difference_empty. Qed.
729 730
    Lemma difference_union_distr_l_L X Y Z : (X  Y)  Z = X  Z  Y  Z.
    Proof. unfold_leibniz. apply difference_union_distr_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
731 732
    Lemma difference_union_distr_r_L X Y Z : Z  (X  Y) = (Z  X)  (Z  Y).
    Proof. unfold_leibniz. apply difference_union_distr_r. Qed.
733 734 735
    Lemma difference_intersection_distr_l_L X Y Z :
      (X  Y)  Z = X  Z  Y  Z.
    Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
736
    Lemma difference_disjoint_L X Y : X ## Y  X  Y = X.
737
    Proof. unfold_leibniz. apply difference_disjoint. Qed.
738 739
    Lemma difference_difference_L X Y Z : (X  Y)  Z = X  (Y  Z).
    Proof. unfold_leibniz. apply difference_difference. Qed.
740 741

    (** Disjointness *)
742
    Lemma disjoint_intersection_L X Y : X ## Y  X  Y = .
743
    Proof. unfold_leibniz. apply disjoint_intersection. Qed.
744 745 746
  End leibniz.

  Section dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
747
    Context `{!RelDecision (@{C})}.
748
    Lemma not_elem_of_intersection x X Y : x  X  Y  x  X  x  Y.
749
    Proof. rewrite elem_of_intersection. destruct (decide (x  X)); tauto. Qed.
750
    Lemma not_elem_of_difference x X Y : x  X  Y  x  X  x  Y.
751
    Proof. rewrite elem_of_difference. destruct (decide (x  Y)); tauto. Qed.
752 753
    Lemma union_difference X Y : X  Y  Y  X  Y  X.
    Proof.
754
      intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
755
      destruct (decide (x  X)); intuition.
756
    Qed.
757 758 759 760 761
    Lemma difference_union X Y : X  Y  Y  X  Y.
    Proof.
      intros x. rewrite !elem_of_union; rewrite elem_of_difference.
      split; [ | destruct (decide (x  Y)) ]; intuition.
    Qed.
762
    Lemma subseteq_disjoint_union X Y : X  Y   Z, Y  X  Z  X ## Z.
763 764 765 766
    Proof.
      split; [|set_solver].
      exists (Y  X); split; [auto using union_difference|set_solver].
    Qed.
767
    Lemma non_empty_difference X Y : X  Y  Y  X  .
768
    Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed.
769
    Lemma empty_difference_subseteq X Y : X  Y    X  Y.
770
    Proof. set_solver. Qed.
771 772 773 774
    Lemma singleton_union_difference X Y x :
      {[x]}  (X  Y)  ({[x]}  X)  (Y  {[x]}).
    Proof.
      intro y; split; intros Hy; [ set_solver | ].
775
      destruct (decide (y  ({[x]} : C))); set_solver.
776
    Qed.
777

778 779 780
    Context `{!LeibnizEquiv C}.
    Lemma union_difference_L X Y : X  Y  Y = X  Y  X.
    Proof. unfold_leibniz. apply union_difference. Qed.
781 782
    Lemma difference_union_L X Y : X  Y  Y = X  Y.
    Proof. unfold_leibniz. apply difference_union. Qed.
783 784
    Lemma non_empty_difference_L X Y : X  Y  Y  X  .
    Proof. unfold_leibniz. apply non_empty_difference. Qed.
785 786
    Lemma empty_difference_subseteq_L X Y : X  Y =   X  Y.
    Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
787
    Lemma subseteq_disjoint_union_L X Y : X  Y   Z, Y = X  Z  X ## Z.
788
    Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed.
789 790 791
    Lemma singleton_union_difference_L X Y x :
      {[x]}  (X  Y) = ({[x]}  X)  (Y  {[x]}).
    Proof. unfold_leibniz. apply singleton_union_difference. Qed.
792
  End dec.
793
End set.
794

795 796

(** * Conversion of option and list *)
797 798
Section option_and_list_to_set.
  Context `{SemiSet A C}.
799 800
  Implicit Types l : list A.

801
  Lemma elem_of_option_to_set (x : A) mx: x  option_to_set (C:=C) mx  mx = Some x.
802
  Proof. destruct mx; set_solver. Qed.
803 804
  Lemma not_elem_of_option_to_set (x : A) mx: x  option_to_set (C:=C) mx  mx  Some x.
  Proof. by rewrite elem_of_option_to_set. Qed.
805

806
  Lemma elem_of_list_to_set (x : A) l : x  list_to_set (C:=C) l  x  l.
807 808 809 810 811 812
  Proof.
    split.
    - induction l; simpl; [by rewrite elem_of_empty|].
      rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
    - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
  Qed.
813 814
  Lemma not_elem_of_list_to_set (x : A) l : x  list_to_set (C:=C) l  x  l.
  Proof. by rewrite elem_of_list_to_set. Qed.
815

816
  Global Instance set_unfold_option_to_set (mx : option A) x :
817
    SetUnfoldElemOf x (option_to_set (C:=C) mx) (mx = Some x).
818 819
  Proof. constructor; apply elem_of_option_to_set. Qed.
  Global Instance set_unfold_list_to_set (l : list A) x P :
820
    SetUnfoldElemOf x l P  SetUnfoldElemOf x (list_to_set (C:=C) l) P.
821
  Proof. constructor. by rewrite elem_of_list_to_set, (set_unfold (x  l) P). Qed.
822

823
  Lemma list_to_set_nil : list_to_set [] =@{C} .
824
  Proof. done. Qed.
825
  Lemma list_to_set_cons x l : list_to_set (x :: l) =@{C} {[ x ]}  list_to_set l.
826
  Proof. done. Qed.
827
  Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) @{C} list_to_set l1  list_to_set l2.
828
  Proof. set_solver. Qed.
829
  Global Instance list_to_set_perm : Proper ((≡ₚ) ==> ()) (list_to_set (C:=C)).
830
  Proof. induction 1; set_solver. Qed.
Robbert Krebbers's avatar