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.