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.