collections.v 15.1 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.

42
  Lemma elem_of_union_list (x : A) (Xs : list C) :
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 63 64 65 66 67 68 69
  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.

  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.
70 71 72 73 74 75 76 77 78 79 80 81 82 83
End simple_collection.

Section collection.
  Context `{Collection A C}.

  Global Instance: LowerBoundedLattice C.
  Proof. split. apply _. firstorder auto. Qed.

  Lemma intersection_twice x : {[x]}  {[x]}  {[x]}.
  Proof.
    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
  Qed.

  Context `{ (X Y : C), Decision (X  Y)}.
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99

  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.
100
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102
End collection.

103 104 105 106 107 108 109
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.

110 111 112 113 114
(** * 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]. *)
115 116 117 118 119 120 121 122 123 124
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
125 126 127 128
    | 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
129 130
    end);
  repeat match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
133
  | |- context [ _   ] => setoid_rewrite elem_of_empty
134
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
138 139 140 141
  | |- 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
142 143
  end.

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

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

(** * Sets without duplicates up to an equivalence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Section no_dup.
199
  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202 203 204 205 206 207 208

  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.
209 210
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212 213 214 215
  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.
216
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
218
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
219
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
220
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222 223
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
224
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
226
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228

  Lemma no_dup_empty: no_dup .
229
  Proof. unfold no_dup. solve_elem_of. Qed.
230
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
231
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
232 233 234
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
235
    rewrite (Hnodup x y) in Hin; solve_elem_of.
236
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
238
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
240
  Proof. unfold no_dup. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
241 242
End no_dup.

243
(** * Quantifiers *)
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Section quantifiers.
245
  Context `{SimpleCollection A B} (P : A  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248 249 250

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

  Lemma cforall_empty : cforall .
251
  Proof. unfold cforall. solve_elem_of. Qed.
252
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
253
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
255
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
257
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
259
  Proof. unfold cforall. solve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261

  Lemma cexists_empty : ¬cexists .
262
  Proof. unfold cexists. esolve_elem_of. Qed.
263
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
264
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
266
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
268
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
270
  Proof. unfold cexists. esolve_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272
End quantifiers.

273 274
Section more_quantifiers.
  Context `{Collection A B}.
275

276
  Lemma cforall_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
277
    cforall P X  cforall Q X.
278
  Proof. unfold cforall. naive_solver. Qed.
279
  Lemma cexists_weaken (P Q : A  Prop) (Hweaken :  x, P x  Q x) X :
280
    cexists P X  cexists Q X.
281
  Proof. unfold cexists. naive_solver. Qed.
282 283
End more_quantifiers.

284 285 286
(** * Fresh elements *)
(** We collect some properties on the [fresh] operation. In particular we
generalize [fresh] to generate lists of fresh elements. *)
287
Section fresh.
288
  Context `{FreshSpec A C} .
289

290 291 292 293
  Definition fresh_sig (X : C) : { x : A | x  X } :=
    exist ( X) (fresh X) (is_fresh X).

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

296 297 298 299 300 301
  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.

302 303 304 305
  Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
306 307
    * by rewrite E.
    * apply IHn. by rewrite E.
308 309
  Qed.

310 311 312
  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

313
  Lemma fresh_list_is_fresh n X x : x  fresh_list n X  x  X.
314
  Proof.
315 316 317
    revert X. induction n; intros X; simpl.
    * by rewrite elem_of_nil.
    * rewrite elem_of_cons. intros [?| Hin]; subst.
318
      + apply is_fresh.
319
      + apply IHn in Hin. solve_elem_of.
320 321 322 323 324 325 326
  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.
327
    solve_elem_of.
328 329
  Qed.
End fresh.
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 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

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.
  Proof. rewrite elem_of_mapM. apply Forall2_Forall_1. Qed.

  Lemma mapM_non_empty {A B} (f : A  M B) l :
    Forall (λ x,  y, y  f x) l 
     k, k  mapM f l.
  Proof. induction 1; esolve_elem_of. Qed.
End collection_monad.