collections.v 10.4 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
10
11
Section collection.
  Context `{Collection A B}.

12
13
  Lemma elem_of_empty x : x    False.
  Proof. split. apply not_elem_of_empty. easy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
17
  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.
18
19
20
21
  Lemma not_elem_of_singleton x y : x  {[ y ]}  x  y.
  Proof. now 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
22

23
24
  Global Instance collection_subseteq: SubsetEq B := λ X Y,
     x, x  X  x  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
28
29
30
31
32
33
  Global Instance: BoundedJoinSemiLattice B.
  Proof. firstorder. Qed.
  Global Instance: MeetSemiLattice B.
  Proof. firstorder. Qed.

  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
  Proof. easy. Qed.
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. firstorder. Qed.
34
35
  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
36
37
  Proof. firstorder. Qed.

38
39
40
  Global Instance singleton_proper : Proper ((=) ==> ()) singleton.
  Proof. repeat intro. now subst. Qed.
  Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
  Proof. intros ???. subst. firstorder. Qed.

43
  Lemma empty_ne_singleton x :   {[ x ]}.
44
  Proof.
45
    intros [_ E]. apply (elem_of_empty x).
46
    apply E. now apply elem_of_singleton.
47
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
End collection.

50
51
(** * Theorems about map *)
Section map.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
  Context `{Collection A C}.

54
55
  Lemma elem_of_map_1 (f : A  A) (X : C) (x : A) :
    x  X  f x  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Proof. intros. apply (elem_of_map _). eauto. Qed.
57
58
  Lemma elem_of_map_1_alt (f : A  A) (X : C) (x : A) y :
    x  X  y = f x  y  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  Proof. intros. apply (elem_of_map _). eauto. Qed.
60
61
  Lemma elem_of_map_2 (f : A  A) (X : C) (x : A) :
    x  map f X   y, x = f y  y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof. intros. now apply (elem_of_map _). Qed.
63
64
65
66
67
68
69
70
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]. *)
Ltac unfold_elem_of := repeat
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
  match goal with
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_subseteq in H
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
74
  | H : context [ _   ] |- _ => setoid_rewrite elem_of_empty in H
75
  | H : context [ _  {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
81
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_union in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_intersection in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_difference in H
  | H : context [ _  map _ _ ] |- _ => setoid_rewrite elem_of_map in H
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
82
  | |- context [ _   ] => setoid_rewrite elem_of_empty
83
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89
  | |- 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.

90
91
92
93
(** 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. *)
Tactic Notation "solve_elem_of" tactic(tac) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  simpl in *;
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
125
126
127
128
129
130
131
132
  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. *)
Tactic Notation "esolve_elem_of" tactic(tac) :=
  simpl in *;
  unfold_elem_of;
  naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.

(** Given an assumption [H : _ ∈ _], the tactic [destruct_elem_of H] will
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
Tactic Notation "destruct_elem_of" hyp(H) :=
  let rec go H :=
  lazymatch type of H with
  | _   => apply elem_of_empty in H; destruct H
  | _  {[ ?l' ]} => apply elem_of_singleton in H; subst l'
  | _  _  _ =>
    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.

(** * Sets without duplicates up to an equivalence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
136
137
138
139
140
141
142
143
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.
144
145
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
148
149
150
  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.
151
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
153
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
154
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
155
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157
158
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
159
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
161
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163

  Lemma no_dup_empty: no_dup .
164
  Proof. unfold no_dup. solve_elem_of. Qed.
165
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
166
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
167
168
169
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
170
    rewrite (Hnodup x y) in Hin; solve_elem_of.
171
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
173
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
175
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
End no_dup.

178
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
182
183
184
185
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 .
186
  Proof. unfold cforall. solve_elem_of. Qed.
187
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
188
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
190
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
192
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
194
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196

  Lemma cexists_empty : ¬cexists .
197
  Proof. unfold cexists. esolve_elem_of. Qed.
198
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
199
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
201
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
203
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
205
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
End quantifiers.

208
209
Section more_quantifiers.
  Context `{Collection A B}.
210

211
212
  Lemma cforall_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cforall P X  cforall Q X.
213
  Proof. unfold cforall. naive_solver. Qed.
214
215
  Lemma cexists_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cexists P X  cexists Q X.
216
  Proof. unfold cexists. naive_solver. Qed.
217
218
End more_quantifiers.

219
220
221
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
222
223
224
Section fresh.
  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .

225
226
227
228
229
230
  Definition fresh_sig (X : C) : { x : A | x  X } :=
    exist ( X) (fresh X) (is_fresh X).

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

231
232
233
234
235
236
  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.

237
238
239
240
241
242
243
244
  Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
    * now rewrite E.
    * apply IHn. now rewrite E.
  Qed.

245
246
247
248
249
250
251
252
253
  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.
    * easy.
    * intros X [?| Hin]. subst.
      + apply is_fresh.
254
      + apply IHn in Hin. solve_elem_of.
255
256
257
258
259
260
261
  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.
262
    solve_elem_of.
263
264
  Qed.
End fresh.