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

Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
107
108
109
110
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.

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

114
Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
115
116
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
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.
157
  Context `{SemiSet A C}.
158
159
160
  Implicit Types x y : A.
  Implicit Types X Y : C.

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

  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) :
Robbert Krebbers's avatar
Robbert Krebbers committed
211
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold ( = X) ( x, ¬P x) | 5.
212
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed.
213
  Global Instance set_unfold_equiv_empty_r_L (P : A  Prop) X :
Robbert Krebbers's avatar
Robbert Krebbers committed
214
    ( x, SetUnfoldElemOf x X (P x))  SetUnfold (X = ) ( x, ¬P x) | 5.
215
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed.
216
  Global Instance set_unfold_equiv_L (P Q : A  Prop) X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
217
    ( x, SetUnfoldElemOf x X (P x))  ( x, SetUnfoldElemOf x Y (Q x)) 
218
    SetUnfold (X = Y) ( x, P x  Q x) | 10.
219
  Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed.
220
221
222
End set_unfold_simple.

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

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

Section set_unfold_monad.
244
  Context `{MonadSet M}.
245

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

Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
266
267
Section set_unfold_list.
  Context {A : Type}.
  Implicit Types x : A.
  Implicit Types l : list A.

Robbert Krebbers's avatar
Robbert Krebbers committed
268
  Global Instance set_unfold_nil x : SetUnfoldElemOf x [] False.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
  Proof. constructor; apply elem_of_nil. Qed.
  Global Instance set_unfold_cons x y l P :
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
    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
273
  Global Instance set_unfold_app x l k P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
    SetUnfoldElemOf x l P  SetUnfoldElemOf x k Q 
    SetUnfoldElemOf x (l ++ k) (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
276
277
  Proof.
    intros ??; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
    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
279
280
  Qed.
  Global Instance set_unfold_included l k (P Q : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
281
    ( x, SetUnfoldElemOf x l (P x))  ( x, SetUnfoldElemOf x k (Q x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
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.
End set_unfold_list.

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

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

319
320
321
322
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.
Hint Extern 1000 (_  _) => set_solver : set_solver.

323

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

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

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

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

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

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

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

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

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

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

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

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

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

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

515
    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
516
    Proof. unfold_leibniz. apply union_cancel_l. Qed.
517
    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
518
519
    Proof. unfold_leibniz. apply union_cancel_r. Qed.

520
521
522
523
524
525
526
527
528
529
530
531
532
    (** 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 *)
533
    Lemma non_empty_singleton_L x : {[ x ]}  ( : C).
534
535
536
537
538
539
540
541
542
543
544
545
546
547
    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.
548
    Context `{!RelDecision (@{C})}.
549
    Lemma set_subseteq_inv X Y : X  Y  X  Y  X  Y.
550
    Proof. destruct (decide (X  Y)); [by right|left;set_solver]. Qed.
551
    Lemma set_not_subset_inv X Y : X  Y  X  Y  X  Y.
552
553
554
555
556
557
558
559
    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}.
560
561
562
563
    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.
564
565
566
567
568
    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.
569
End semi_set.
570
571


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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
593
  Lemma intersection_mono_l X Y1 Y2 : Y1  Y2  X  Y1  X  Y2.
594
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
  Lemma intersection_mono_r X1 X2 Y : X1  X2  X1  Y  X2  Y.
596
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
597
  Lemma intersection_mono X1 X2 Y1 Y2 :
598
    X1  X2  Y1  Y2  X1  Y1  X2  Y2.
599
  Proof. set_solver. Qed.
600

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

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

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

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

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

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

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

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

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

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

    (** Difference *)
693
694
    Lemma difference_twice_L X Y : (X  Y)  Y = X  Y.
    Proof. unfold_leibniz. apply difference_twice. Qed.
695
696
    Lemma subseteq_empty_difference_L X Y : X  Y  X  Y = .
    Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
697
698
    Lemma difference_diag_L X : X  X = .
    Proof. unfold_leibniz. apply difference_diag. Qed.
699
700
    Lemma difference_empty_L X : X   = X.
    Proof. unfold_leibniz. apply difference_empty. Qed.
701
702
    Lemma difference_union_distr_l_L X Y Z : (X  Y)  Z = X  Z  Y  Z.
    Proof.