collections.v 17.2 KB
Newer Older
1 2 3 4 5 6 7 8
(* Copyright (c) 2012, Robbert Krebbers. *)
(* 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.

(** * 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 34 35 36
  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.
37
  Global Instance singleton_proper : Proper ((=) ==> ()) singleton.
38
  Proof. repeat intro. by subst. Qed.
39
  Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) () | 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  Proof. intros ???. subst. firstorder. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Context `{ X Y : C, Decision (X  Y)}.
64 65 66 67 68 69

  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.
70 71
End simple_collection.

72 73 74 75 76 77 78
Ltac decompose_empty := repeat
  match goal with
  | H : _  _   |- _ => apply empty_union in H; destruct H
  | H : _  _   |- _ => apply non_empty_union in H; destruct H
  | H : {[ _ ]}   |- _ => destruct (non_empty_singleton _ H)
  end.

79 80 81 82 83
(** * Tactics *)
(** The first pass consists of eliminating all occurrences of [(∪)], [(∩)],
[(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into
logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into
[A → x ∈ X ∨ False]. *)
84 85 86 87
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
88
    | context [ _  _ ] => setoid_rewrite subset_spec in H
89 90 91 92 93 94
    | context [ _  _ ] => setoid_rewrite elem_of_equiv_alt in H
    | 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
95 96 97 98
    | 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
99 100
    end);
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  | |- context [ _  _ ] => setoid_rewrite subset_spec
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
104
  | |- context [ _   ] => setoid_rewrite elem_of_empty
105
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
109 110 111 112
  | |- 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
113 114
  end.

115 116 117
(** 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. *)
118
Tactic Notation "solve_elem_of" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  simpl in *;
120 121 122 123 124 125 126 127 128
  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. *)
129
Tactic Notation "esolve_elem_of" tactic3(tac) :=
130 131 132 133 134
  simpl in *;
  unfold_elem_of;
  naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.

135
(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
136
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
137
Tactic Notation "decompose_elem_of" hyp(H) :=
138 139 140
  let rec go H :=
  lazymatch type of H with
  | _   => apply elem_of_empty in H; destruct H
141 142
  | ?x  {[ ?y ]} =>
    apply elem_of_singleton in H; try first [subst y | subst x]
143 144 145 146 147 148 149 150 151
  | _  _  _ =>
    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
152 153 154 155 156 157 158 159 160 161 162
  | ?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
163 164
  | _ => idtac
  end in go H.
165 166
Tactic Notation "decompose_elem_of" :=
  repeat_on_hyps (fun H => decompose_elem_of H).
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
Section collection.
  Context `{Collection A C}.

  Global Instance: LowerBoundedLattice C.
  Proof. split. apply _. firstorder auto. Qed.

  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.

  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.

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

241
(** * Sets without duplicates up to an equivalence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Section no_dup.
243
  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245 246 247 248

  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
249
  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251 252
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
253 254
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256 257 258 259
  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.
260
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
262
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
263
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
264
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
265

266 267
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
268
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
270
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272

  Lemma no_dup_empty: no_dup .
273
  Proof. unfold no_dup. solve_elem_of. Qed.
274
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
275
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
276 277 278
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
279
    rewrite (Hnodup x y) in Hin; solve_elem_of.
280
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
282
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
284
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
End no_dup.

287
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
288
Section quantifiers.
289
  Context `{SimpleCollection A B} (P : A  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
290 291 292 293 294

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

  Lemma cforall_empty : cforall .
295
  Proof. unfold cforall. solve_elem_of. Qed.
296
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
297
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
299
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
301
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
303
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304 305

  Lemma cexists_empty : ¬cexists .
306
  Proof. unfold cexists. esolve_elem_of. Qed.
307
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
308
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
310
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
312
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
314
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
315 316
End quantifiers.

317 318
Section more_quantifiers.
  Context `{Collection A B}.
319

320
  Lemma cforall_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
321
    cforall P X  cforall Q X.
322
  Proof. unfold cforall. naive_solver. Qed.
323
  Lemma cexists_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
324
    cexists P X  cexists Q X.
325
  Proof. unfold cexists. naive_solver. Qed.
326 327
End more_quantifiers.

328 329 330
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
331
Section fresh.
332
  Context `{FreshSpec A C} .
333

334 335 336 337
  Definition fresh_sig (X : C) : { x : A | x  X } :=
    exist ( X) (fresh X) (is_fresh X).

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

340 341 342 343 344 345
  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.

346 347 348 349
  Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
350 351
    * by rewrite E.
    * apply IHn. by rewrite E.
352 353
  Qed.

354 355 356
  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

357
  Lemma fresh_list_is_fresh n X x : x  fresh_list n X  x  X.
358
  Proof.
359 360 361
    revert X. induction n; intros X; simpl.
    * by rewrite elem_of_nil.
    * rewrite elem_of_cons. intros [?| Hin]; subst.
362
      + apply is_fresh.
363
      + apply IHn in Hin. solve_elem_of.
364 365 366 367 368 369 370
  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.
371
    solve_elem_of.
372 373
  Qed.
End fresh.
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436

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

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
437 438 439 440 441 442 443 444 445
  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
  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 
    Forall2 P l1 l2.
  Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
    induction Hl1; inversion_clear 1; constructor; auto.
  Qed.
446
End collection_monad.