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.