collections.v 28.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2 3 4 5
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
collections. *)
6
From stdpp Require Export base tactics orders.
7
From stdpp Require Import sets.
8

9 10 11
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
   x, x  X  x  Y.

12
(** * Basic theorems *)
13 14
Section simple_collection.
  Context `{SimpleCollection A C}.
15 16
  Implicit Types x y : A.
  Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18
  Lemma elem_of_empty x : x    False.
19
  Proof. split. apply not_elem_of_empty. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22 23
  Lemma elem_of_union_l x X Y : x  X  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.
  Lemma elem_of_union_r x X Y : x  Y  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.
24 25 26
  Global Instance: EmptySpec C.
  Proof. firstorder auto. Qed.
  Global Instance: JoinSemiLattice C.
27
  Proof. firstorder auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29
  Global Instance: AntiSymm () (@collection_subseteq A C _).
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
31
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32 33
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. firstorder. Qed.
34 35
  Lemma elem_of_equiv_alt X Y :
    X  Y  ( x, x  X  x  Y)  ( x, x  Y  x  X).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  Proof. firstorder. Qed.
37 38
  Lemma elem_of_equiv_empty X : X     x, x  X.
  Proof. firstorder. Qed.
39 40 41 42 43 44
  Lemma collection_positive_l X Y : X  Y    X  .
  Proof.
    rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
  Qed.
  Lemma collection_positive_l_alt X Y : X    X  Y  .
  Proof. eauto using collection_positive_l. Qed.
45 46 47 48
  Lemma elem_of_singleton_1 x y : x  {[y]}  x = y.
  Proof. by rewrite elem_of_singleton. Qed.
  Lemma elem_of_singleton_2 x y : x = y  x  {[y]}.
  Proof. by rewrite elem_of_singleton. Qed.
49 50 51
  Lemma elem_of_subseteq_singleton x X : x  X  {[ x ]}  X.
  Proof.
    split.
52 53
    - intros ??. rewrite elem_of_singleton. by intros ->.
    - intros Ex. by apply (Ex x), elem_of_singleton.
54
  Qed.
55
  Global Instance singleton_proper : Proper ((=) ==> ()) (singleton (B:=C)).
56
  Proof. by repeat intro; subst. Qed.
57 58
  Global Instance elem_of_proper :
    Proper ((=) ==> () ==> iff) (() : A  C  Prop) | 5.
59
  Proof. intros ???; subst. firstorder. Qed.
60
  Lemma elem_of_union_list Xs x : x   Xs   X, X  Xs  x  X.
61 62
  Proof.
    split.
63
    - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
64
      setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
65
    - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
66
      intros. apply elem_of_union_r; auto.
67
  Qed.
68
  Lemma non_empty_singleton x : ({[ x ]} : C)  .
69 70 71 72 73 74
  Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
  Lemma not_elem_of_singleton x y : x  {[ y ]}  x  y.
  Proof. by rewrite elem_of_singleton. Qed.
  Lemma not_elem_of_union x X Y : x  X  Y  x  X  x  Y.
  Proof. rewrite elem_of_union. tauto. Qed.

75 76 77 78 79 80 81 82 83
  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.
    Lemma elem_of_equiv_alt_L X Y :
      X = Y  ( x, x  X  x  Y)  ( x, x  Y  x  X).
    Proof. unfold_leibniz. apply elem_of_equiv_alt. Qed.
    Lemma elem_of_equiv_empty_L X : X =    x, x  X.
    Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
84 85 86 87
    Lemma collection_positive_l_L X Y : X  Y =   X = .
    Proof. unfold_leibniz. apply collection_positive_l. Qed.
    Lemma collection_positive_l_alt_L X Y : X    X  Y  .
    Proof. unfold_leibniz. apply collection_positive_l_alt. Qed.
88 89 90 91 92 93 94 95 96 97 98 99
    Lemma non_empty_singleton_L x : {[ x ]}  .
    Proof. unfold_leibniz. apply non_empty_singleton. Qed.
  End leibniz.

  Section dec.
    Context `{ X Y : C, Decision (X  Y)}.
    Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
    Proof.
      refine (cast_if (decide_rel () {[ x ]} X));
        by rewrite elem_of_subseteq_singleton.
    Defined.
  End dec.
100 101
End simple_collection.

102
Definition of_option `{Singleton A C, Empty C} (x : option A) : C :=
103
  match x with None =>  | Some a => {[ a ]} end.
104 105
Fixpoint of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
  match l with [] =>  | x :: l => {[ x ]}  of_list l end.
106

107 108 109 110 111 112 113 114 115 116
Section of_option_list.
  Context `{SimpleCollection A C}.
  Lemma elem_of_of_option (x : A) o : x  of_option o  o = Some x.
  Proof.
    destruct o; simpl;
      rewrite ?elem_of_empty, ?elem_of_singleton; naive_solver.
  Qed.
  Lemma elem_of_of_list (x : A) l : x  of_list l  x  l.
  Proof.
    split.
117
    - induction l; simpl; [by rewrite elem_of_empty|].
Robbert Krebbers's avatar
Robbert Krebbers committed
118
      rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
119
    - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
120 121
  Qed.
End of_option_list.
122 123 124

Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
  λ P dec A x, match dec with left H => x H | _ =>  end.
125 126 127 128 129 130 131 132 133

Section collection_monad_base.
  Context `{CollectionMonad M}.
  Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
    x  guard P; X  P  x  X.
  Proof.
    unfold mguard, collection_guard; simpl; case_match;
      rewrite ?elem_of_empty; naive_solver.
  Qed.
134 135 136
  Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
    P  x  X  x  guard P; X.
  Proof. by rewrite elem_of_guard. Qed.
137 138 139 140 141 142 143 144 145 146 147 148
  Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X    ¬P  X  .
  Proof.
    rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
    destruct (decide P); naive_solver.
  Qed.
  Lemma bind_empty {A B} (f : A  M B) X :
    X = f    X     x, x  X  f x  .
  Proof.
    setoid_rewrite elem_of_equiv_empty; setoid_rewrite elem_of_bind.
    naive_solver.
  Qed.
End collection_monad_base.
149

150 151 152 153 154 155 156
(** * Tactics *)
(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
Tactic Notation "decompose_elem_of" hyp(H) :=
  let rec go H :=
  lazymatch type of H with
  | _   => apply elem_of_empty in H; destruct H
157 158 159
  | _   => clear H
  | _  {[ _ | _ ]} => rewrite elem_of_mkSet in H
  | ¬_  {[ _ | _ ]} => rewrite not_elem_of_mkSet in H
160 161
  | ?x  {[ ?y ]} =>
    apply elem_of_singleton in H; try first [subst y | subst x]
162 163
  | ?x  {[ ?y ]} =>
    apply not_elem_of_singleton in H
164
  | _  _  _ =>
165 166 167 168
    apply elem_of_union in H; destruct H as [H|H]; [go H|go H]
  | _  _  _ =>
    let H1 := fresh H in let H2 := fresh H in apply not_elem_of_union in H;
    destruct H as [H1 H2]; go H1; go H2
169
  | _  _  _ =>
170
    let H1 := fresh H in let H2 := fresh H in apply elem_of_intersection in H;
171 172
    destruct H as [H1 H2]; go H1; go H2
  | _  _  _ =>
173
    let H1 := fresh H in let H2 := fresh H in apply elem_of_difference in H;
174 175
    destruct H as [H1 H2]; go H1; go H2
  | ?x  _ <$> _ =>
176
    apply elem_of_fmap in H; destruct H as [? [? H]]; try (subst x); go H
177
  | _  _ = _ =>
178
    let H1 := fresh H in let H2 := fresh H in apply elem_of_bind in H;
179 180 181 182
    destruct H as [? [H1 H2]]; go H1; go H2
  | ?x  mret ?y =>
    apply elem_of_ret in H; try first [subst y | subst x]
  | _  mjoin _ = _ =>
183
    let H1 := fresh H in let H2 := fresh H in apply elem_of_join in H;
184
    destruct H as [? [H1 H2]]; go H1; go H2
185
  | _  guard _; _ =>
186
    let H1 := fresh H in let H2 := fresh H in apply elem_of_guard in H;
187 188
    destruct H as [H1 H2]; go H2
  | _  of_option _ => apply elem_of_of_option in H
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  | _  of_list _ => apply elem_of_of_list in H
190 191 192 193 194
  | _ => idtac
  end in go H.
Tactic Notation "decompose_elem_of" :=
  repeat_on_hyps (fun H => decompose_elem_of H).

195 196
Ltac decompose_empty := repeat
  match goal with
197 198 199 200
  | H :    |- _ => clear H
  | H :  =  |- _ => clear H
  | H :   _ |- _ => symmetry in H
  | H :  = _ |- _ => symmetry in H
201 202 203
  | H : _  _   |- _ => apply empty_union in H; destruct H
  | H : _  _   |- _ => apply non_empty_union in H; destruct H
  | H : {[ _ ]}   |- _ => destruct (non_empty_singleton _ H)
204 205 206
  | H : _  _ =  |- _ => apply empty_union_L in H; destruct H
  | H : _  _   |- _ => apply non_empty_union_L in H; destruct H
  | H : {[ _ ]} =  |- _ => destruct (non_empty_singleton_L _ H)
207
  | H : guard _ ; _   |- _ => apply guard_empty in H; destruct H
208 209
  end.

210 211 212 213
(** The first pass of our collection tactic consists of eliminating all
occurrences of [(∪)], [(∩)], [(∖)], [(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)],
by rewriting these into logically equivalent propositions. For example we
rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *)
214
Ltac set_unfold :=
215 216 217
  repeat_on_hyps (fun H =>
    repeat match type of H with
    | context [ _  _ ] => setoid_rewrite elem_of_subseteq in H
Robbert Krebbers's avatar
Robbert Krebbers committed
218
    | context [ _  _ ] => setoid_rewrite subset_spec in H
219
    | context [ _   ] => setoid_rewrite elem_of_equiv_empty in H
220
    | context [ _  _ ] => setoid_rewrite elem_of_equiv_alt in H
221 222
    | context [ _ =  ] => setoid_rewrite elem_of_equiv_empty_L in H
    | context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H
223
    | context [ _   ] => setoid_rewrite elem_of_empty in H
224
    | context [ _   ] => setoid_rewrite elem_of_all in H
225
    | context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
226
    | context [ _  {[_| _ ]} ] => setoid_rewrite elem_of_mkSet in H; simpl in H
227 228 229
    | context [ _  _  _ ] => setoid_rewrite elem_of_union in H
    | context [ _  _  _ ] => setoid_rewrite elem_of_intersection in H
    | context [ _  _  _ ] => setoid_rewrite elem_of_difference in H
230 231 232 233
    | context [ _  _ <$> _ ] => setoid_rewrite elem_of_fmap in H
    | context [ _  mret _ ] => setoid_rewrite elem_of_ret in H
    | context [ _  _ = _ ] => setoid_rewrite elem_of_bind in H
    | context [ _  mjoin _ ] => setoid_rewrite elem_of_join in H
234
    | context [ _  guard _; _ ] => setoid_rewrite elem_of_guard in H
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236
    | context [ _  of_option _ ] => setoid_rewrite elem_of_of_option in H
    | context [ _  of_list _ ] => setoid_rewrite elem_of_of_list in H
237 238
    end);
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
239
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
Robbert Krebbers's avatar
Robbert Krebbers committed
240
  | |- context [ _  _ ] => setoid_rewrite subset_spec
241
  | |- context [ _   ] => setoid_rewrite elem_of_equiv_empty
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
243 244
  | |- context [ _ =  ] => setoid_rewrite elem_of_equiv_empty_L
  | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L
245
  | |- context [ _   ] => setoid_rewrite elem_of_empty
246
  | |- context [ _   ] => setoid_rewrite elem_of_all
247
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
248
  | |- context [ _  {[ _ | _ ]} ] => setoid_rewrite elem_of_mkSet; simpl
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
252 253 254 255
  | |- context [ _  _ <$> _ ] => setoid_rewrite elem_of_fmap
  | |- context [ _  mret _ ] => setoid_rewrite elem_of_ret
  | |- context [ _  _ = _ ] => setoid_rewrite elem_of_bind
  | |- context [ _  mjoin _ ] => setoid_rewrite elem_of_join
256
  | |- context [ _  guard _; _ ] => setoid_rewrite elem_of_guard
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
  | |- context [ _  of_option _ ] => setoid_rewrite elem_of_of_option
  | |- context [ _  of_list _ ] => setoid_rewrite elem_of_of_list
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
  end.

261
(** Since [firstorder] fails or loops on very small goals generated by
262
[set_solver] already. We use the [naive_solver] tactic as a substitute.
263
This tactic either fails or proves the goal. *)
264
Tactic Notation "set_solver" "by" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  setoid_subst;
266
  decompose_empty;
267
  set_unfold;
268
  naive_solver tac.
269 270 271 272 273
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.
274
Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
275
Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
276

277
(** * More theorems *)
Robbert Krebbers's avatar
Robbert Krebbers committed
278 279
Section collection.
  Context `{Collection A C}.
280
  Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
281

282
  Global Instance: Lattice C.
283
  Proof. split. apply _. firstorder auto. set_solver. Qed.
284 285
  Global Instance difference_proper :
     Proper (() ==> () ==> ()) (@difference C _).
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287 288 289
  Proof.
    intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
    by rewrite !elem_of_difference, HX, HY.
  Qed.
290
  Lemma non_empty_inhabited x X : x  X  X  .
291
  Proof. set_solver. Qed.
292
  Lemma intersection_singletons x : ({[x]} : C)  {[x]}  {[x]}.
293
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
  Lemma difference_twice X Y : (X  Y)  Y  X  Y.
295
  Proof. set_solver. Qed.
296
  Lemma subseteq_empty_difference X Y : X  Y  X  Y  .
297
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  Lemma difference_diag X : X  X  .
299
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  Lemma difference_union_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
301
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Lemma difference_union_distr_r X Y Z : Z  (X  Y)  (Z  X)  (Z  Y).
303
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
  Lemma difference_intersection_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
305
  Proof. set_solver. Qed.
306
  Lemma disjoint_union_difference X Y : X  Y    (X  Y)  X  Y.
307
  Proof. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
308

309 310 311 312 313 314
  Section leibniz.
    Context `{!LeibnizEquiv C}.
    Lemma intersection_singletons_L x : {[x]}  {[x]} = {[x]}.
    Proof. unfold_leibniz. apply intersection_singletons. Qed.
    Lemma difference_twice_L X Y : (X  Y)  Y = X  Y.
    Proof. unfold_leibniz. apply difference_twice. Qed.
315 316
    Lemma subseteq_empty_difference_L X Y : X  Y  X  Y = .
    Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
317 318 319 320
    Lemma difference_diag_L X : X  X = .
    Proof. unfold_leibniz. apply difference_diag. Qed.
    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
321 322
    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.
323 324 325
    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.
326 327
    Lemma disjoint_union_difference_L X Y : X  Y =   (X  Y)  X = Y.
    Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
328 329 330
  End leibniz.

  Section dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
    Context `{ (x : A) (X : C), Decision (x  X)}.
332
    Lemma not_elem_of_intersection x X Y : x  X  Y  x  X  x  Y.
333
    Proof. rewrite elem_of_intersection. destruct (decide (x  X)); tauto. Qed.
334
    Lemma not_elem_of_difference x X Y : x  X  Y  x  X  x  Y.
335
    Proof. rewrite elem_of_difference. destruct (decide (x  Y)); tauto. Qed.
336 337
    Lemma union_difference X Y : X  Y  Y  X  Y  X.
    Proof.
338 339
      split; intros x; rewrite !elem_of_union, elem_of_difference; [|intuition].
      destruct (decide (x  X)); intuition.
340 341 342 343
    Qed.
    Lemma non_empty_difference X Y : X  Y  Y  X  .
    Proof.
      intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
344
      destruct (decide (x  X)); set_solver.
345
    Qed.
346
    Lemma empty_difference_subseteq X Y : X  Y    X  Y.
347
    Proof. intros ? x ?; apply dec_stable; set_solver. Qed.
348 349 350 351 352
    Context `{!LeibnizEquiv C}.
    Lemma union_difference_L X Y : X  Y  Y = X  Y  X.
    Proof. unfold_leibniz. apply union_difference. Qed.
    Lemma non_empty_difference_L X Y : X  Y  Y  X  .
    Proof. unfold_leibniz. apply non_empty_difference. Qed.
353 354
    Lemma empty_difference_subseteq_L X Y : X  Y =   X  Y.
    Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
355 356 357 358 359 360
  End dec.
End collection.

Section collection_ops.
  Context `{CollectionOps A C}.

Robbert Krebbers's avatar
Robbert Krebbers committed
361 362 363 364 365
  Lemma elem_of_intersection_with_list (f : A  A  option A) Xs Y x :
    x  intersection_with_list f Y Xs   xs y,
      Forall2 () xs Xs  y  Y  foldr (λ x, (= f x)) (Some y) xs = Some x.
  Proof.
    split.
366
    - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
367 368
      rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
      destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
369
      eexists (x1 :: xs), y. intuition (simplify_option_eq; auto).
370
    - intros (xs & y & Hxs & ? & Hx). revert x Hx.
371
      induction Hxs; intros; simplify_option_eq; [done |].
Robbert Krebbers's avatar
Robbert Krebbers committed
372 373 374 375 376 377 378 379 380
      rewrite elem_of_intersection_with. naive_solver.
  Qed.

  Lemma intersection_with_list_ind (P Q : A  Prop) f Xs Y :
    ( y, y  Y  P y) 
    Forall (λ X,  x, x  X  Q x) Xs 
    ( x y z, Q x  P y  f x y = Some z  P z) 
     x, x  intersection_with_list f Y Xs  P x.
  Proof.
381
    intros HY HXs Hf. induction Xs; simplify_option_eq; [done |].
Robbert Krebbers's avatar
Robbert Krebbers committed
382 383 384
    intros x Hx. rewrite elem_of_intersection_with in Hx.
    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
  Qed.
385
End collection_ops.
Robbert Krebbers's avatar
Robbert Krebbers committed
386

387
(** * Sets without duplicates up to an equivalence *)
388
Section NoDup.
389
  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
Robbert Krebbers's avatar
Robbert Krebbers committed
390 391

  Definition elem_of_upto (x : A) (X : B) :=  y, y  X  R x y.
392
  Definition set_NoDup (X : B) :=  x y, x  X  y  X  R x y  x = y.
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394

  Global Instance: Proper (() ==> iff) (elem_of_upto x).
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
396 397 398
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
399 400
    - rewrite <-E1, <-E2; intuition.
    - rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
  Qed.
402
  Global Instance: Proper (() ==> iff) set_NoDup.
Robbert Krebbers's avatar
Robbert Krebbers committed
403 404 405
  Proof. firstorder. Qed.

  Lemma elem_of_upto_elem_of x X : x  X  elem_of_upto x X.
406
  Proof. unfold elem_of_upto. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
408
  Proof. unfold elem_of_upto. set_solver. Qed.
409
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
410
  Proof. unfold elem_of_upto. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411

412 413
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
414
  Proof. unfold elem_of_upto. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
416
  Proof. unfold elem_of_upto. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417

418
  Lemma set_NoDup_empty: set_NoDup .
419
  Proof. unfold set_NoDup. set_solver. Qed.
420 421
  Lemma set_NoDup_add x X :
    ¬elem_of_upto x X  set_NoDup X  set_NoDup ({[ x ]}  X).
422
  Proof. unfold set_NoDup, elem_of_upto. set_solver. Qed.
423 424
  Lemma set_NoDup_inv_add x X :
    x  X  set_NoDup ({[ x ]}  X)  ¬elem_of_upto x X.
425 426
  Proof.
    intros Hin Hnodup [y [??]].
427
    rewrite (Hnodup x y) in Hin; set_solver.
428
  Qed.
429
  Lemma set_NoDup_inv_union_l X Y : set_NoDup (X  Y)  set_NoDup X.
430
  Proof. unfold set_NoDup. set_solver. Qed.
431
  Lemma set_NoDup_inv_union_r X Y : set_NoDup (X  Y)  set_NoDup Y.
432
  Proof. unfold set_NoDup. set_solver. Qed.
433
End NoDup.
Robbert Krebbers's avatar
Robbert Krebbers committed
434

435
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
436
Section quantifiers.
437
  Context `{SimpleCollection A B} (P : A  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
438

439 440 441 442
  Definition set_Forall X :=  x, x  X  P x.
  Definition set_Exists X :=  x, x  X  P x.

  Lemma set_Forall_empty : set_Forall .
443
  Proof. unfold set_Forall. set_solver. Qed.
444
  Lemma set_Forall_singleton x : set_Forall {[ x ]}  P x.
445
  Proof. unfold set_Forall. set_solver. Qed.
446
  Lemma set_Forall_union X Y : set_Forall X  set_Forall Y  set_Forall (X  Y).
447
  Proof. unfold set_Forall. set_solver. Qed.
448
  Lemma set_Forall_union_inv_1 X Y : set_Forall (X  Y)  set_Forall X.
449
  Proof. unfold set_Forall. set_solver. Qed.
450
  Lemma set_Forall_union_inv_2 X Y : set_Forall (X  Y)  set_Forall Y.
451
  Proof. unfold set_Forall. set_solver. Qed.
452 453

  Lemma set_Exists_empty : ¬set_Exists .
454
  Proof. unfold set_Exists. set_solver. Qed.
455
  Lemma set_Exists_singleton x : set_Exists {[ x ]}  P x.
456
  Proof. unfold set_Exists. set_solver. Qed.
457
  Lemma set_Exists_union_1 X Y : set_Exists X  set_Exists (X  Y).
458
  Proof. unfold set_Exists. set_solver. Qed.
459
  Lemma set_Exists_union_2 X Y : set_Exists Y  set_Exists (X  Y).
460
  Proof. unfold set_Exists. set_solver. Qed.
461 462
  Lemma set_Exists_union_inv X Y :
    set_Exists (X  Y)  set_Exists X  set_Exists Y.
463
  Proof. unfold set_Exists. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
464 465
End quantifiers.

466
Section more_quantifiers.
467
  Context `{SimpleCollection A B}.
468

469 470 471 472 473 474
  Lemma set_Forall_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
    set_Forall P X  set_Forall Q X.
  Proof. unfold set_Forall. naive_solver. Qed.
  Lemma set_Exists_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
    set_Exists P X  set_Exists Q X.
  Proof. unfold set_Exists. naive_solver. Qed.
475 476
End more_quantifiers.

477 478 479
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
480 481 482 483 484 485 486 487 488 489
Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
    (n : nat) (X : C) : list A :=
  match n with
  | 0 => []
  | S n => let x := fresh X in x :: fresh_list n ({[ x ]}  X)
  end.
Inductive Forall_fresh `{ElemOf A C} (X : C) : list A  Prop :=
  | Forall_fresh_nil : Forall_fresh X []
  | Forall_fresh_cons x xs :
     x  xs  x  X  Forall_fresh X xs  Forall_fresh X (x :: xs).
490

491 492
Section fresh.
  Context `{FreshSpec A C}.
493
  Implicit Types X Y : C.
494

495
  Global Instance fresh_proper: Proper (() ==> (=)) (fresh (C:=C)).
496
  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
497 498
  Global Instance fresh_list_proper:
    Proper ((=) ==> () ==> (=)) (fresh_list (C:=C)).
499
  Proof.
500
    intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal/=; [by rewrite E|].
501
    apply IH. by rewrite E.
502
  Qed.
503 504 505 506 507 508 509 510 511 512 513 514 515 516 517

  Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs  NoDup xs.
  Proof. induction 1; by constructor. Qed.
  Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs  x  xs  x  X.
  Proof.
    intros HX; revert x; rewrite <-Forall_forall.
    by induction HX; constructor.
  Qed.
  Lemma Forall_fresh_alt X xs :
    Forall_fresh X xs  NoDup xs   x, x  xs  x  X.
  Proof.
    split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of.
    rewrite <-Forall_forall.
    intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
  Lemma Forall_fresh_subseteq X Y xs :
    Forall_fresh X xs  Y  X  Forall_fresh Y xs.
520
  Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
521

522 523
  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.
524
  Lemma fresh_list_is_fresh n X x : x  fresh_list n X  x  X.
525
  Proof.
526
    revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
527
    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
528
    apply IH in Hin; set_solver.
529
  Qed.
530
  Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
531
  Proof.
532
    revert X. induction n; simpl; constructor; auto.
533
    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
534 535 536 537
  Qed.
  Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
  Proof.
    rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh.
538 539
  Qed.
End fresh.
540

541
(** * Properties of implementations of collections that form a monad *)
542 543 544
Section collection_monad.
  Context `{CollectionMonad M}.

545 546
  Global Instance collection_fmap_mono {A B} :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
547
  Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
548 549
  Global Instance collection_fmap_proper {A B} :
    Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
550
  Proof. intros f g ? X Y [??]; split; set_solver by eauto. Qed.
551 552
  Global Instance collection_bind_mono {A B} :
    Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
553
  Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
554 555
  Global Instance collection_bind_proper {A B} :
    Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
556
  Proof. unfold respectful; intros f g Hfg X Y [??]; split; set_solver. Qed.
557 558
  Global Instance collection_join_mono {A} :
    Proper (() ==> ()) (@mjoin M _ A).
559
  Proof. intros X Y ?; set_solver. Qed.
560 561
  Global Instance collection_join_proper {A} :
    Proper (() ==> ()) (@mjoin M _ A).
562
  Proof. intros X Y [??]; split; set_solver. Qed.
563

564
  Lemma collection_bind_singleton {A B} (f : A  M B) x : {[ x ]} = f  f x.
565
  Proof. set_solver. Qed.
566
  Lemma collection_guard_True {A} `{Decision P} (X : M A) : P  guard P; X  X.
567
  Proof. set_solver. Qed.
568
  Lemma collection_fmap_compose {A B C} (f : A  B) (g : B  C) (X : M A) :
569
    g  f <$> X  g <$> (f <$> X).
570
  Proof. set_solver. Qed.
571 572
  Lemma elem_of_fmap_1 {A B} (f : A  B) (X : M A) (y : B) :
    y  f <$> X   x, y = f x  x  X.
573
  Proof. set_solver. Qed.
574 575
  Lemma elem_of_fmap_2 {A B} (f : A  B) (X : M A) (x : A) :
    x  X  f x  f <$> X.
576
  Proof. set_solver. Qed.
577 578
  Lemma elem_of_fmap_2_alt {A B} (f : A  B) (X : M A) (x : A) (y : B) :
    x  X  y = f x  y  f <$> X.
579
  Proof. set_solver. Qed.
580 581 582 583 584

  Lemma elem_of_mapM {A B} (f : A  M B) l k :
    l  mapM f k  Forall2 (λ x y, x  f y) l k.
  Proof.
    split.
585
    - revert l. induction k; set_solver by eauto.
586
    - induction 1; set_solver.
587
  Qed.
588
  Lemma collection_mapM_length {A B} (f : A  M B) l k :
589
    l  mapM f k  length l = length k.
590
  Proof. revert l; induction k; set_solver by eauto. Qed.
591
  Lemma elem_of_mapM_fmap {A B} (f : A  B) (g : B  M A) l k :
592
    Forall (λ x,  y, y  g x  f y = x) l  k  mapM g l  fmap f k = l.
593
  Proof.
594
    intros Hl. revert k. induction Hl; simpl; intros;
595
      decompose_elem_of; f_equal/=; auto.
596 597
  Qed.
  Lemma elem_of_mapM_Forall {A B} (f : A  M B) (P : B  Prop) l k :
598
    l  mapM f k  Forall (λ x,  y, y  f x  P y) k  Forall P l.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
600 601
  Lemma elem_of_mapM_Forall2_l {A B C} (f : A  M B) (P: B  C  Prop) l1 l2 k :
    l1  mapM f k  Forall2 (λ x y,  z, z  f x  P z y) k l2 
Robbert Krebbers's avatar
Robbert Krebbers committed
602 603 604 605 606
    Forall2 P l1 l2.
  Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
    induction Hl1; inversion_clear 1; constructor; auto.
  Qed.
607
End collection_monad.
608 609 610 611 612 613

(** Finite collections *)
Definition set_finite `{ElemOf A B} (X : B) :=  l : list A,  x, x  X  x  l.

Section finite.
  Context `{SimpleCollection A B}.
614 615
  Global Instance set_finite_subseteq :
     Proper (flip () ==> impl) (@set_finite A B _).
616
  Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed.
617 618
  Global Instance set_finite_proper : Proper (() ==> iff) (@set_finite A B _).
  Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed.
619 620 621
  Lemma empty_finite : set_finite .
  Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
  Lemma singleton_finite (x : A) : set_finite {[ x ]}.
Ralf Jung's avatar
Ralf Jung committed
622
  Proof. exists [x]; intros y ->%elem_of_singleton; left. Qed.
623 624 625 626 627 628
  Lemma union_finite X Y : set_finite X  set_finite Y  set_finite (X  Y).
  Proof.
    intros [lX ?] [lY ?]; exists (lX ++ lY); intros x.
    rewrite elem_of_union, elem_of_app; naive_solver.
  Qed.
  Lemma union_finite_inv_l X Y : set_finite (X  Y)  set_finite X.
629
  Proof. intros [l ?]; exists l; set_solver. Qed.
630
  Lemma union_finite_inv_r X Y : set_finite (X  Y)  set_finite Y.
631
  Proof. intros [l ?]; exists l; set_solver. Qed.
632 633 634 635 636
End finite.

Section more_finite.
  Context `{Collection A B}.
  Lemma intersection_finite_l X Y : set_finite X  set_finite (X  Y).
Ralf Jung's avatar
Ralf Jung committed
637
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
638
  Lemma intersection_finite_r X Y : set_finite Y  set_finite (X  Y).
Ralf Jung's avatar
Ralf Jung committed
639
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
640
  Lemma difference_finite X Y : set_finite X  set_finite (X  Y).
Ralf Jung's avatar
Ralf Jung committed
641
  Proof. intros [l ?]; exists l; intros x [??]%elem_of_difference; auto. Qed.
642 643 644 645
  Lemma difference_finite_inv X Y `{ x, Decision (x  Y)} :
    set_finite Y  set_finite (X  Y)  set_finite X.
  Proof.
    intros [l ?] [k ?]; exists (l ++ k).
646
    intros x ?; destruct (decide (x  Y)); rewrite elem_of_app; set_solver.
647
  Qed.
648
End more_finite.