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.