sets.v 48.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.

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285 286 287 288 289 290
    SetUnfold (l  k) ( x, P x  Q x).
  Proof.
    constructor; unfold subseteq, list_subseteq.
    apply forall_proper; naive_solver.
  Qed.
End set_unfold_list.

291 292 293
Ltac set_unfold :=
  let rec unfold_hyps :=
    try match goal with
294 295 296 297 298 299 300
    | 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
301 302 303
    end in
  apply set_unfold_2; unfold_hyps; csimpl in *.

304 305
(** Since [firstorder] already fails or loops on very small goals generated by
[set_solver], we use the [naive_solver] tactic as a substitute. *)
306
Tactic Notation "set_solver" "by" tactic3(tac) :=
307
  try fast_done;
308 309 310 311 312 313 314 315 316 317 318 319 320
  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.

321 322 323 324
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.

325

326 327 328
(** * Sets with [∪], [∅] and [{[_]}] *)
Section semi_set.
  Context `{SemiSet A C}.
329 330 331 332 333 334 335
  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.
336
  Lemma set_equiv_spec X Y : X  Y  X  Y  Y  X.
337 338 339
  Proof. set_solver. Qed.

  (** Subset relation *)
340
  Global Instance set_subseteq_antisymm: AntiSymm () (@{C}).
341 342
  Proof. intros ??. set_solver. Qed.

343
  Global Instance set_subseteq_preorder: PreOrder (@{C}).
344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365
  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 *)
366 367
  Lemma union_subseteq X Y Z : X  Y  Z  X  Z  Y  Z.
  Proof. set_solver. Qed.
368 369 370 371 372 373
  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.
374
  Lemma union_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
375
  Proof. set_solver. Qed.
376
  Lemma union_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
377
  Proof. set_solver. Qed.
378
  Lemma union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
379 380
  Proof. set_solver. Qed.

381
  Global Instance union_idemp : IdemP (@{C}) ().
382
  Proof. intros X. set_solver. Qed.
383
  Global Instance union_empty_l : LeftId (@{C})  ().
384
  Proof. intros X. set_solver. Qed.
385
  Global Instance union_empty_r : RightId (@{C})  ().
386
  Proof. intros X. set_solver. Qed.
387
  Global Instance union_comm : Comm (@{C}) ().
388
  Proof. intros X Y. set_solver. Qed.
389
  Global Instance union_assoc : Assoc (@{C}) ().
390 391 392 393 394
  Proof. intros X Y Z. set_solver. Qed.

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

395
  Lemma union_cancel_l X Y Z : Z ## X  Z ## Y  Z  X  Z  Y  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
  Proof. set_solver. Qed.
397
  Lemma union_cancel_r X Y Z : X ## Z  Y ## Z  X  Z  Y  Z  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
398 399
  Proof. set_solver. Qed.

400
  (** Empty *)
Robbert Krebbers's avatar
Robbert Krebbers committed
401 402
  Lemma empty_subseteq X :   X.
  Proof. set_solver. Qed.
403 404
  Lemma elem_of_equiv_empty X : X     x, x  X.
  Proof. set_solver. Qed.
405
  Lemma elem_of_empty x : x  ( : C)  False.
406 407 408 409 410 411 412 413 414 415 416
  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 *)
417
  Lemma elem_of_singleton_1 x y : x  ({[y]} : C)  x = y.
418
  Proof. by rewrite elem_of_singleton. Qed.
419
  Lemma elem_of_singleton_2 x y : x = y  x  ({[y]} : C).
420 421 422 423 424
  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.
425
  Lemma not_elem_of_singleton x y : x  ({[ y ]} : C)  x  y.
426 427 428
  Proof. by rewrite elem_of_singleton. Qed.

  (** Disjointness *)
429
  Lemma elem_of_disjoint X Y : X ## Y   x, x  X  x  Y  False.
430 431
  Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
432
  Global Instance disjoint_sym : Symmetric (##@{C}).
433
  Proof. intros X Y. set_solver. Qed.
434
  Lemma disjoint_empty_l Y :  ## Y.
435
  Proof. set_solver. Qed.
436
  Lemma disjoint_empty_r X : X ## .
437
  Proof. set_solver. Qed.
438
  Lemma disjoint_singleton_l x Y : {[ x ]} ## Y  x  Y.
439
  Proof. set_solver. Qed.
440
  Lemma disjoint_singleton_r y X : X ## {[ y ]}  y  X.
441
  Proof. set_solver. Qed.
442
  Lemma disjoint_union_l X1 X2 Y : X1  X2 ## Y  X1 ## Y  X2 ## Y.
443
  Proof. set_solver. Qed.
444
  Lemma disjoint_union_r X Y1 Y2 : X ## Y1  Y2  X ## Y1  X ## Y2.
445 446 447 448
  Proof. set_solver. Qed.

  (** Big unions *)
  Lemma elem_of_union_list Xs x : x   Xs   X, X  Xs  x  X.
449 450
  Proof.
    split.
451 452
    - 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
453
    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
454
      intros. apply elem_of_union_r; auto.
455
  Qed.
456

457 458 459 460 461 462 463
  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.
464
  Proof.
465 466
    induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id  _)|].
    by rewrite IH, (assoc _).
467
  Qed.
468
  Lemma union_list_reverse Xs :  (reverse Xs)   Xs.
469
  Proof.
470 471 472
    induction Xs as [|X Xs IH]; simpl; [done |].
    by rewrite reverse_cons, union_list_app,
      union_list_singleton, (comm _), IH.
473
  Qed.
474 475
  Lemma union_list_mono Xs Ys : Xs * Ys   Xs   Ys.
  Proof. induction 1; simpl; auto using union_mono. Qed.
476
  Lemma empty_union_list Xs :  Xs    Forall ( ) Xs.
477
  Proof.
478 479 480
    split.
    - induction Xs; simpl; rewrite ?empty_union; intuition.
    - induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
481
  Qed.
482

483 484 485 486 487
  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.
488 489
    Lemma set_equiv_spec_L X Y : X = Y  X  Y  Y  X.
    Proof. unfold_leibniz. apply set_equiv_spec. Qed.
490 491

    (** Subset relation *)
492
    Global Instance set_subseteq_partialorder : PartialOrder (@{C}).
493 494 495 496 497 498 499 500 501 502
    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 *)
503
    Global Instance union_idemp_L : IdemP (=@{C}) ().
504
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
505
    Global Instance union_empty_l_L : LeftId (=@{C})  ().
506
    Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
507
    Global Instance union_empty_r_L : RightId (=@{C})  ().
508
    Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
509
    Global Instance union_comm_L : Comm (=@{C}) ().
510
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
511
    Global Instance union_assoc_L : Assoc (=@{C}) ().
512 513 514 515 516
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.

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

517
    Lemma union_cancel_l_L X Y Z : Z ## X  Z ## Y  Z  X = Z  Y  X = Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
    Proof. unfold_leibniz. apply union_cancel_l. Qed.
519
    Lemma union_cancel_r_L X Y Z : X ## Z  Y ## Z  X  Z = Y  Z  X = Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
520 521
    Proof. unfold_leibniz. apply union_cancel_r. Qed.

522 523 524 525 526 527 528 529 530 531 532 533 534
    (** 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 *)
535
    Lemma non_empty_singleton_L x : {[ x ]}  ( : C).
536 537 538 539 540 541 542 543 544 545 546 547 548 549
    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.
    Lemma empty_union_list_L Xs :  Xs =   Forall (= ) Xs.
    Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
  End leibniz.

  Section dec.
550
    Context `{!RelDecision (@{C})}.
551
    Lemma set_subseteq_inv X Y : X  Y  X  Y  X  Y.
552
    Proof. destruct (decide (X  Y)); [by right|left;set_solver]. Qed.
553
    Lemma set_not_subset_inv X Y : X  Y  X  Y  X  Y.
554 555 556 557 558 559 560 561
    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.
    Lemma non_empty_union_list Xs :  Xs    Exists ( ) Xs.
    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.

    Context `{!LeibnizEquiv C}.
562 563 564 565
    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.
566 567 568 569 570
    Lemma non_empty_union_L X Y : X  Y    X    Y  .
    Proof. unfold_leibniz. apply non_empty_union. Qed.
    Lemma non_empty_union_list_L Xs :  Xs    Exists ( ) Xs.
    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
  End dec.
571
End semi_set.
572 573


574 575 576
(** * Sets with [∪], [∩], [∖], [∅] and [{[_]}] *)
Section set.
  Context `{Set_ A C}.
577
  Implicit Types x y : A.
578
  Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
579

580 581 582 583 584 585 586 587 588 589 590 591 592 593 594
  (** 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.

595
  Lemma intersection_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
596
  Proof. set_solver. Qed.
597
  Lemma intersection_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
598
  Proof. set_solver. Qed.
599
  Lemma intersection_mono X1 X2 Y1 Y2 :
600
    X1  X2  Y1  Y2  X1  Y1  X2  Y2.
601
  Proof. set_solver. Qed.
602

603
  Global Instance intersection_idemp : IdemP (@{C}) ().
604
  Proof. intros X; set_solver. Qed.
605
  Global Instance intersection_comm : Comm (@{C}) ().
606
  Proof. intros X Y; set_solver. Qed.
607
  Global Instance intersection_assoc : Assoc (@{C}) ().
608
  Proof. intros X Y Z; set_solver. Qed.
609
  Global Instance intersection_empty_l : LeftAbsorb (@{C})  ().
610
  Proof. intros X; set_solver. Qed.
611
  Global Instance intersection_empty_r: RightAbsorb (@{C})  ().
612 613
  Proof. intros X; set_solver. Qed.

614
  Lemma intersection_singletons x : ({[x]} : C)  {[x]}  {[x]}.
615
  Proof. set_solver. Qed.
616 617 618 619 620 621 622 623 624 625 626

  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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
627
  Lemma difference_twice X Y : (X  Y)  Y  X  Y.
628
  Proof. set_solver. Qed.
629
  Lemma subseteq_empty_difference X Y : X  Y  X  Y  .
630
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
  Lemma difference_diag X : X  X  .
632
  Proof. set_solver. Qed.
633 634
  Lemma difference_empty X : X    X.
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
  Lemma difference_union_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
636
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  Lemma difference_union_distr_r X Y Z : Z  (X  Y)  (Z  X)  (Z  Y).
638
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
  Lemma difference_intersection_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
640
  Proof. set_solver. Qed.
641
  Lemma difference_disjoint X Y : X ## Y  X  Y  X.
642
  Proof. set_solver. Qed.
643 644
  Lemma subset_difference_elem_of {x: A} {s: C} (inx: x  s): s  {[ x ]}  s.
  Proof. set_solver. Qed.
645 646
  Lemma difference_difference X Y Z : (X  Y)  Z  X  (Y  Z).
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
647

648
  Lemma difference_mono X1 X2 Y1 Y2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
649 650
    X1  X2  Y2  Y1  X1  Y1  X2  Y2.
  Proof. set_solver. Qed.
651
  Lemma difference_mono_l X Y1 Y2 : Y2  Y1  X  Y1  X  Y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
  Proof. set_solver. Qed.
653
  Lemma difference_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
654 655
  Proof. set_solver. Qed.

656
  (** Disjointness *)
657
  Lemma disjoint_intersection X Y : X ## Y  X  Y  .
658 659
  Proof. set_solver. Qed.

660 661
  Section leibniz.
    Context `{!LeibnizEquiv C}.
662 663 664 665 666 667 668 669 670

    (** 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.

671
    Global Instance intersection_idemp_L : IdemP (=@{C}) ().
672
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
673
    Global Instance intersection_comm_L : Comm (=@{C}) ().
674
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
675
    Global Instance intersection_assoc_L : Assoc (=@{C}) ().
676
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
677
    Global Instance intersection_empty_l_L: LeftAbsorb (=@{C})  ().
678
    Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
679
    Global Instance intersection_empty_r_L: RightAbsorb (=@{C})  ().
680 681
    Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.

682
    Lemma intersection_singletons_L x : {[x]}  {[x]} = ({[x]} : C).
683
    Proof. unfold_leibniz. apply intersection_singletons. Qed.
684 685 686 687 688

    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
689
    Lemma intersection_union_l_L X Y Z : X  (Y  Z) = (X  Y)  (X  Z).
690
    Proof. unfold_leibniz; apply intersection_union_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
691
    Lemma intersection_union_r_L X Y Z : (X  Y)  Z = (X  Z)  (Y  Z).
692 693 694
    Proof. unfold_leibniz; apply intersection_union_r. Qed.

    (** Difference *)
695 696
    Lemma difference_twice_L X Y : (X  Y)  Y = X  Y.
    Proof. unfold_leibniz. apply difference_twice. Qed.
697 698
    Lemma subseteq_empty_difference_L X Y : X  Y  X  Y = .
    Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
699 700
    Lemma difference_diag_L X : X  X = .
    Proof. unfold_leibniz. apply difference_diag. Qed.
701 702
    Lemma difference_empty_L X : X   = X.
    Proof. unfold_leibniz. apply difference_empty. Qed.
703 704
    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
705 706
    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.
707 708 709
    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.
710
    Lemma difference_disjoint_L X Y : X ## Y  X  Y = X.
711
    Proof. unfold_leibniz. apply difference_disjoint. Qed.
712 713
    Lemma difference_difference_L X Y Z : (X  Y)  Z = X  (Y  Z).
    Proof. unfold_leibniz. apply difference_difference. Qed.
714 715

    (** Disjointness *)
716
    Lemma disjoint_intersection_L X Y : X ## Y  X  Y = .
717
    Proof. unfold_leibniz. apply disjoint_intersection. Qed.
718 719 720
  End leibniz.

  Section dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
721
    Context `{!RelDecision (@{C})}.
722
    Lemma not_elem_of_intersection x X Y : x  X  Y  x  X  x  Y.
723
    Proof. rewrite elem_of_intersection. destruct (decide (x  X)); tauto. Qed.
724
    Lemma not_elem_of_difference x X Y : x  X  Y  x  X  x  Y.
725
    Proof. rewrite elem_of_difference. destruct (decide (x  Y)); tauto. Qed.
726 727
    Lemma union_difference X Y : X  Y  Y  X  Y  X.
    Proof.
728
      intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
729
      destruct (decide (x  X)); intuition.
730
    Qed.
731 732 733 734 735
    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.
736
    Lemma subseteq_disjoint_union X Y : X  Y   Z, Y  X  Z  X ## Z.
737 738 739 740
    Proof.
      split; [|set_solver].
      exists (Y  X); split; [auto using union_difference|set_solver].
    Qed.
741
    Lemma non_empty_difference X Y : X  Y  Y  X  .
742
    Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed.
743
    Lemma empty_difference_subseteq X Y : X  Y    X  Y.
744
    Proof. set_solver. Qed.
Dan Frumin's avatar