collections.v 20.1 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
2 3 4 5 6 7
(* 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. *)
Require Export base tactics orders.

8
(** * Basic theorems *)
9 10
Section simple_collection.
  Context `{SimpleCollection A C}.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
  Lemma elem_of_empty x : x    False.
13
  Proof. split. apply not_elem_of_empty. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18
  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.

19
  Global Instance collection_subseteq: SubsetEq C := λ X Y,
20
     x, x  X  x  Y.
21
  Global Instance: BoundedJoinSemiLattice C.
22
  Proof. firstorder auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24

  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
25
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. firstorder. Qed.
28 29
  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
30
  Proof. firstorder. Qed.
31 32 33
  Lemma elem_of_equiv_empty X : X     x, x  X.
  Proof. firstorder. Qed.

34 35 36 37 38 39
  Lemma elem_of_subseteq_singleton x X : x  X  {[ x ]}  X.
  Proof.
    split.
    * intros ??. rewrite elem_of_singleton. intro. by subst.
    * intros Ex. by apply (Ex x), elem_of_singleton.
  Qed.
40
  Global Instance singleton_proper : Proper ((=) ==> ()) singleton.
41
  Proof. repeat intro. by subst. Qed.
42
  Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) () | 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
  Proof. intros ???. subst. firstorder. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
  Lemma elem_of_union_list (Xs : list C) (x : A) :
46
    x   Xs   X, X  Xs  x  X.
47 48 49 50
  Proof.
    split.
    * induction Xs; simpl; intros HXs.
      + by apply elem_of_empty in HXs.
51 52 53
      + setoid_rewrite elem_of_cons.
        apply elem_of_union in HXs. naive_solver.
    * intros [X []]. induction 1; simpl.
54
      + by apply elem_of_union_l.
55
      + intros. apply elem_of_union_r; auto.
56 57 58 59 60 61 62 63 64 65
  Qed.

  Lemma non_empty_singleton x : {[ x ]}  .
  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.

66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
  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.
    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.
89 90
End simple_collection.

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
(** * 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
  | ?x  {[ ?y ]} =>
    apply elem_of_singleton in H; try first [subst y | subst x]
  | _  _  _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
    destruct H as [H1|H2]; [go H1 | go H2]
  | _  _  _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H;
    destruct H as [H1 H2]; go H1; go H2
  | _  _  _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
    destruct H as [H1 H2]; go H1; go H2
  | ?x  _ <$> _ =>
    let H1 := fresh in apply elem_of_fmap in H;
    destruct H as [? [? H1]]; try (subst x); go H1
  | _  _ = _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_bind in H;
    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 _ = _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_join in H;
    destruct H as [? [H1 H2]]; go H1; go H2
  | _ => idtac
  end in go H.
Tactic Notation "decompose_elem_of" :=
  repeat_on_hyps (fun H => decompose_elem_of H).

125 126
Ltac decompose_empty := repeat
  match goal with
127 128 129 130
  | H :    |- _ => clear H
  | H :  =  |- _ => clear H
  | H :   _ |- _ => symmetry in H
  | H :  = _ |- _ => symmetry in H
131 132 133
  | H : _  _   |- _ => apply empty_union in H; destruct H
  | H : _  _   |- _ => apply non_empty_union in H; destruct H
  | H : {[ _ ]}   |- _ => destruct (non_empty_singleton _ H)
134 135 136
  | 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)
137 138
  end.

139 140 141 142
(** 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]. *)
143 144 145 146
Ltac unfold_elem_of :=
  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
147
    | context [ _  _ ] => setoid_rewrite subset_spec in H
148
    | context [ _   ] => setoid_rewrite elem_of_equiv_empty in H
149
    | context [ _  _ ] => setoid_rewrite elem_of_equiv_alt in H
150 151
    | context [ _ =  ] => setoid_rewrite elem_of_equiv_empty_L in H
    | context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H
152 153 154 155 156
    | context [ _   ] => setoid_rewrite elem_of_empty in H
    | context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
    | context [ _  _  _ ] => setoid_rewrite elem_of_union in H
    | context [ _  _  _ ] => setoid_rewrite elem_of_intersection in H
    | context [ _  _  _ ] => setoid_rewrite elem_of_difference in H
157 158 159 160
    | 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
161 162
    end);
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
Robbert Krebbers's avatar
Robbert Krebbers committed
164
  | |- context [ _  _ ] => setoid_rewrite subset_spec
165
  | |- context [ _   ] => setoid_rewrite elem_of_equiv_empty
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
167 168
  | |- context [ _ =  ] => setoid_rewrite elem_of_equiv_empty_L
  | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L
169
  | |- context [ _   ] => setoid_rewrite elem_of_empty
170
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
171 172 173
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
174 175 176 177
  | |- 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
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179
  end.

180 181 182
(** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
generally powerful enough. This tactic either fails or proves the goal. *)
183
Tactic Notation "solve_elem_of" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  simpl in *;
185
  decompose_empty;
186 187 188 189 190 191 192 193 194
  unfold_elem_of;
  solve [intuition (simplify_equality; tac)].
Tactic Notation "solve_elem_of" := solve_elem_of auto.

(** For goals with quantifiers we could use the above tactic but with
[firstorder] instead of [intuition] as finishing tactic. However, [firstorder]
fails or loops on very small goals generated by [solve_elem_of] already. We
use the [naive_solver] tactic as a substitute. This tactic either fails or
proves the goal. *)
195
Tactic Notation "esolve_elem_of" tactic3(tac) :=
196
  simpl in *;
197
  decompose_empty;
198 199 200
  unfold_elem_of;
  naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.
201 202
 
(** * More theorems *)
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206
Section collection.
  Context `{Collection A C}.

  Global Instance: LowerBoundedLattice C.
207 208 209 210 211 212
  Proof.
    split.
    * apply _.
    * firstorder auto.
    * solve_elem_of.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227

  Lemma intersection_singletons x : {[x]}  {[x]}  {[x]}.
  Proof. esolve_elem_of. Qed.
  Lemma difference_twice X Y : (X  Y)  Y  X  Y.
  Proof. esolve_elem_of. Qed.

  Lemma empty_difference X Y : X  Y  X  Y  .
  Proof. esolve_elem_of. Qed.
  Lemma difference_diag X : X  X  .
  Proof. esolve_elem_of. Qed.
  Lemma difference_union_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
  Proof. esolve_elem_of. Qed.
  Lemma difference_intersection_distr_l X Y Z : (X  Y)  Z  X  Z  Y  Z.
  Proof. esolve_elem_of. Qed.

228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283
  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.

    Lemma empty_difference_L X Y : X  Y  X  Y = .
    Proof. unfold_leibniz. apply empty_difference. Qed.
    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.
    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.
  End leibniz.

  Section dec.
    Context `{ X Y : C, Decision (X  Y)}.

    Lemma not_elem_of_intersection x X Y : x  X  Y  x  X  x  Y.
    Proof.
      rewrite elem_of_intersection.
      destruct (decide (x  X)); tauto.
    Qed.
    Lemma not_elem_of_difference x X Y : x  X  Y  x  X  x  Y.
    Proof.
      rewrite elem_of_difference.
      destruct (decide (x  Y)); tauto.
    Qed.
    Lemma union_difference X Y : X  Y  Y  X  Y  X.
    Proof.
      split; intros x; rewrite !elem_of_union, elem_of_difference.
      * destruct (decide (x  X)); intuition.
      * intuition.
    Qed.
    Lemma non_empty_difference X Y : X  Y  Y  X  .
    Proof.
      intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
      destruct (decide (x  X)); esolve_elem_of.
    Qed.

    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.
  End dec.
End collection.

Section collection_ops.
  Context `{CollectionOps A C}.

Robbert Krebbers's avatar
Robbert Krebbers committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
  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.
    * revert x. induction Xs; simpl; intros x HXs.
      + eexists [], x. intuition.
      + rewrite elem_of_intersection_with in HXs.
        destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
        destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
        eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
    * intros (xs & y & Hxs & ? & Hx). revert x Hx.
      induction Hxs; intros; simplify_option_equality; [done |].
      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.
    intros HY HXs Hf.
    induction Xs; simplify_option_equality; [done |].
    intros x Hx. rewrite elem_of_intersection_with in Hx.
    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
  Qed.
311
End collection_ops.
Robbert Krebbers's avatar
Robbert Krebbers committed
312

313
(** * Sets without duplicates up to an equivalence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Section no_dup.
315
  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
Robbert Krebbers's avatar
Robbert Krebbers committed
316 317 318 319 320

  Definition elem_of_upto (x : A) (X : B) :=  y, y  X  R x y.
  Definition no_dup (X : B) :=  x y, x  X  y  X  R x y  x = y.

  Global Instance: Proper (() ==> iff) (elem_of_upto x).
Robbert Krebbers's avatar
Robbert Krebbers committed
321
  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323 324
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
325 326
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
327 328 329 330 331
  Qed.
  Global Instance: Proper (() ==> iff) no_dup.
  Proof. firstorder. Qed.

  Lemma elem_of_upto_elem_of x X : x  X  elem_of_upto x X.
332
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
334
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
335
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
336
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
337

338 339
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
340
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
342
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344

  Lemma no_dup_empty: no_dup .
345
  Proof. unfold no_dup. solve_elem_of. Qed.
346
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
347
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
348 349 350
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
351
    rewrite (Hnodup x y) in Hin; solve_elem_of.
352
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
354
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
356
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
357 358
End no_dup.

359
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Section quantifiers.
361
  Context `{SimpleCollection A B} (P : A  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
362 363 364 365 366

  Definition cforall X :=  x, x  X  P x.
  Definition cexists X :=  x, x  X  P x.

  Lemma cforall_empty : cforall .
367
  Proof. unfold cforall. solve_elem_of. Qed.
368
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
369
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
371
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
373
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
374
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
375
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
376 377

  Lemma cexists_empty : ¬cexists .
378
  Proof. unfold cexists. esolve_elem_of. Qed.
379
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
380
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
382
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
384
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
386
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
387 388
End quantifiers.

389 390
Section more_quantifiers.
  Context `{Collection A B}.
391

392
  Lemma cforall_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
393
    cforall P X  cforall Q X.
394
  Proof. unfold cforall. naive_solver. Qed.
395
  Lemma cexists_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
396
    cexists P X  cexists Q X.
397
  Proof. unfold cexists. naive_solver. Qed.
398 399
End more_quantifiers.

400 401 402
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
403
Section fresh.
404
  Context `{FreshSpec A C} .
405

406 407 408 409
  Definition fresh_sig (X : C) : { x : A | x  X } :=
    exist ( X) (fresh X) (is_fresh X).

  Global Instance fresh_proper: Proper (() ==> (=)) fresh.
410
  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
411

412 413 414 415 416 417
  Fixpoint fresh_list (n : nat) (X : C) : list A :=
    match n with
    | 0 => []
    | S n => let x := fresh X in x :: fresh_list n ({[ x ]}  X)
    end.

418 419 420 421
  Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
422 423
    * by rewrite E.
    * apply IHn. by rewrite E.
424 425
  Qed.

426 427 428
  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

429
  Lemma fresh_list_is_fresh n X x : x  fresh_list n X  x  X.
430
  Proof.
431 432 433
    revert X. induction n; intros X; simpl.
    * by rewrite elem_of_nil.
    * rewrite elem_of_cons. intros [?| Hin]; subst.
434
      + apply is_fresh.
435
      + apply IHn in Hin. solve_elem_of.
436 437 438 439 440 441 442
  Qed.

  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
  Proof.
    revert X.
    induction n; simpl; constructor; auto.
    intros Hin. apply fresh_list_is_fresh in Hin.
443
    solve_elem_of.
444 445
  Qed.
End fresh.
446 447 448 449 450 451 452

Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C :=
  match x with
  | None => 
  | Some a => {[ a ]}
  end.

453
(** * Properties of implementations of collections that form a monad *)
454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
Section collection_monad.
  Context `{CollectionMonad M}.

  Global Instance collection_guard: MGuard M := λ P dec A x,
    if dec then x else .

  Global Instance collection_fmap_proper {A B} (f : A  B) :
    Proper (() ==> ()) (fmap f).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_ret_proper {A} :
    Proper ((=) ==> ()) (@mret M _ A).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_bind_proper {A B} (f : A  M B) :
    Proper (() ==> ()) (mbind f).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_join_proper {A} :
    Proper (() ==> ()) (@mjoin M _ A).
  Proof. intros X Y E. esolve_elem_of. Qed.

  Lemma collection_fmap_compose {A B C} (f : A  B) (g : B  C) X :
    g  f <$> X  g <$> (f <$> X).
  Proof. esolve_elem_of. Qed.
  Lemma elem_of_fmap_1 {A B} (f : A  B) (X : M A) (y : B) :
    y  f <$> X   x, y = f x  x  X.
  Proof. esolve_elem_of. Qed.
  Lemma elem_of_fmap_2 {A B} (f : A  B) (X : M A) (x : A) :
    x  X  f x  f <$> X.
  Proof. esolve_elem_of. Qed.
  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.
  Proof. esolve_elem_of. Qed.

  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.
    * revert l. induction k; esolve_elem_of.
    * induction 1; esolve_elem_of.
  Qed.
  Lemma mapM_length {A B} (f : A  M B) l k :
    l  mapM f k  length l = length k.
  Proof. revert l; induction k; esolve_elem_of. Qed.

  Lemma elem_of_mapM_fmap {A B} (f : A  B) (g : B  M A) l k :
    Forall (λ x,  y, y  g x  f y = x) l 
    k  mapM g l  fmap f k = l.
  Proof.
    intros Hl. revert k.
    induction Hl; simpl; intros;
      decompose_elem_of; simpl; f_equal; auto.
  Qed.

  Lemma elem_of_mapM_Forall {A B} (f : A  M B) (P : B  Prop) l k :
    l  mapM f k 
    Forall (λ x,  y, y  f x  P y) k 
    Forall P l.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
511 512
  Lemma elem_of_mapM_Forall2_l {A B C} (f : A  M B)
      (P : B  C  Prop) l1 l2 k :
Robbert Krebbers's avatar
Robbert Krebbers committed
513 514 515 516 517 518 519
    l1  mapM f k 
    Forall2 (λ x y,  z, z  f x  P z y) k l2 
    Forall2 P l1 l2.
  Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
    induction Hl1; inversion_clear 1; constructor; auto.
  Qed.
520
End collection_monad.