collections.v 12.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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Section collection.
10
  Context `{Collection 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
22
  Global Instance: LowerBoundedLattice C.
  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) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
  Proof. intros ???. subst. firstorder. Qed.

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
  Lemma elem_of_union_list (x : A) (Xs : list C) :
    x   Xs   X, In X Xs  x  X.
  Proof.
    split.
    * induction Xs; simpl; intros HXs.
      + by apply elem_of_empty in HXs.
      + apply elem_of_union in HXs. naive_solver.
    * intros [X []]. induction Xs; [done | intros [?|?] ?; subst; simpl].
      + by apply elem_of_union_l.
      + apply elem_of_union_r; auto.
  Qed.

  Lemma non_empty_singleton x : {[ x ]}  .
  Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.

  Lemma intersection_twice x : {[x]}  {[x]}  {[x]}.
58
  Proof.
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
  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.

  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.

  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  X  X  Y.
  Proof.
    split; intros x; rewrite !elem_of_union, elem_of_difference.
    * tauto.
    * destruct (decide (x  X)); tauto.
89
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
End collection.

92
93
94
95
96
97
98
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.

99
100
(** * Theorems about map *)
Section map.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
  Context `{Collection A C}.

103
  Lemma elem_of_map_1 (f : A  A) (X : C) (x : A) :
104
105
106
    x  map f X   y, x = f y  y  X.
  Proof. intros. by apply (elem_of_map _). Qed.
  Lemma elem_of_map_2 (f : A  A) (X : C) (x : A) :
107
    x  X  f x  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Proof. intros. apply (elem_of_map _). eauto. Qed.
109
  Lemma elem_of_map_2_alt (f : A  A) (X : C) (x : A) y :
110
    x  X  y = f x  y  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  Proof. intros. apply (elem_of_map _). eauto. Qed.
112
113
114
115
116
117
118
End map.

(** * 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]. *)
119
120
121
122
123
124
125
126
127
128
129
130
131
Ltac unfold_elem_of :=
  repeat_on_hyps (fun H =>
    repeat match type of H with
    | context [ _  _ ] => setoid_rewrite elem_of_subseteq in H
    | 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
    | context [ _  map _ _ ] => setoid_rewrite elem_of_map in H
    end);
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
134
  | |- context [ _   ] => setoid_rewrite elem_of_empty
135
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
140
141
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
  | |- context [ _  map _ _ ] => setoid_rewrite elem_of_map
  end.

142
143
144
(** 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. *)
145
Tactic Notation "solve_elem_of" tactic3(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  simpl in *;
147
148
149
150
151
152
153
154
155
  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. *)
156
Tactic Notation "esolve_elem_of" tactic3(tac) :=
157
158
159
160
161
  simpl in *;
  unfold_elem_of;
  naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.

162
(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
163
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
164
Tactic Notation "decompose_elem_of" hyp(H) :=
165
166
167
  let rec go H :=
  lazymatch type of H with
  | _   => apply elem_of_empty in H; destruct H
168
169
  | ?l  {[ ?l' ]} =>
    apply elem_of_singleton in H; first [ subst l' | subst l | idtac ]
170
171
172
173
174
175
176
177
178
179
180
181
182
183
  | _  _  _ =>
    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
  | _  map _ _ =>
    let H1 := fresh in apply elem_of_map in H;
    destruct H as [?[? H1]]; go H1
  | _ => idtac
  end in go H.
184
185
Tactic Notation "decompose_elem_of" :=
  repeat_on_hyps (fun H => decompose_elem_of H).
186
187

(** * Sets without duplicates up to an equivalence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
190
191
192
193
194
195
196
197
198
Section no_dup.
  Context `{Collection A B} (R : relation A) `{!Equivalence R}.

  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).
  Proof. firstorder. Qed.
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
199
200
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
204
205
  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.
206
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
208
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
209
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
210
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
213
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
214
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
216
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218

  Lemma no_dup_empty: no_dup .
219
  Proof. unfold no_dup. solve_elem_of. Qed.
220
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
221
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
222
223
224
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
225
    rewrite (Hnodup x y) in Hin; solve_elem_of.
226
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
228
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
230
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
End no_dup.

233
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
234
235
236
237
238
239
240
Section quantifiers.
  Context `{Collection A B} (P : A  Prop).

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

  Lemma cforall_empty : cforall .
241
  Proof. unfold cforall. solve_elem_of. Qed.
242
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
243
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
245
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
247
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
249
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
251

  Lemma cexists_empty : ¬cexists .
252
  Proof. unfold cexists. esolve_elem_of. Qed.
253
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
254
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
256
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
258
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
260
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
End quantifiers.

263
264
Section more_quantifiers.
  Context `{Collection A B}.
265

266
  Lemma cforall_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
267
    cforall P X  cforall Q X.
268
  Proof. unfold cforall. naive_solver. Qed.
269
  Lemma cexists_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
270
    cexists P X  cexists Q X.
271
  Proof. unfold cexists. naive_solver. Qed.
272
273
End more_quantifiers.

274
275
276
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
277
278
279
Section fresh.
  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .

280
281
282
283
  Definition fresh_sig (X : C) : { x : A | x  X } :=
    exist ( X) (fresh X) (is_fresh X).

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

286
287
288
289
290
291
  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.

292
293
294
295
  Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
296
297
    * by rewrite E.
    * apply IHn. by rewrite E.
298
299
  Qed.

300
301
302
303
304
305
  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X)  x  X.
  Proof.
    revert X. induction n; simpl.
306
    * done.
307
308
    * intros X [?| Hin]. subst.
      + apply is_fresh.
309
      + apply IHn in Hin. solve_elem_of.
310
311
312
313
314
315
316
  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.
317
    solve_elem_of.
318
319
  Qed.
End fresh.