collections.v 10.4 KB
 Robbert Krebbers committed Aug 29, 2012 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 committed Jun 11, 2012 9 10 11 ``````Section collection. Context `{Collection A B}. `````` Robbert Krebbers committed Aug 29, 2012 12 13 `````` Lemma elem_of_empty x : x ∈ ∅ ↔ False. Proof. split. apply not_elem_of_empty. easy. Qed. `````` Robbert Krebbers committed Jun 11, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 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 committed Jun 11, 2012 22 `````` `````` Robbert Krebbers committed Aug 29, 2012 23 24 `````` Global Instance collection_subseteq: SubsetEq B := λ X Y, ∀ x, x ∈ X → x ∈ Y. `````` Robbert Krebbers committed Jun 11, 2012 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. `````` Robbert Krebbers committed Aug 21, 2012 34 35 `````` Lemma elem_of_equiv_alt X Y : X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X). `````` Robbert Krebbers committed Jun 11, 2012 36 37 `````` Proof. firstorder. Qed. `````` Robbert Krebbers committed Aug 29, 2012 38 39 40 `````` Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton. Proof. repeat intro. now subst. Qed. Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈). `````` Robbert Krebbers committed Jun 11, 2012 41 42 `````` Proof. intros ???. subst. firstorder. Qed. `````` Robbert Krebbers committed Aug 29, 2012 43 `````` Lemma empty_ne_singleton x : ∅ ≢ {[ x ]}. `````` Robbert Krebbers committed Aug 21, 2012 44 `````` Proof. `````` Robbert Krebbers committed Aug 29, 2012 45 `````` intros [_ E]. apply (elem_of_empty x). `````` Robbert Krebbers committed Aug 21, 2012 46 `````` apply E. now apply elem_of_singleton. `````` Robbert Krebbers committed Aug 29, 2012 47 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 48 49 ``````End collection. `````` Robbert Krebbers committed Aug 29, 2012 50 51 ``````(** * Theorems about map *) Section map. `````` Robbert Krebbers committed Jun 11, 2012 52 53 `````` Context `{Collection A C}. `````` Robbert Krebbers committed Aug 21, 2012 54 55 `````` Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) : x ∈ X → f x ∈ map f X. `````` Robbert Krebbers committed Jun 11, 2012 56 `````` Proof. intros. apply (elem_of_map _). eauto. Qed. `````` Robbert Krebbers committed Aug 21, 2012 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 committed Jun 11, 2012 59 `````` Proof. intros. apply (elem_of_map _). eauto. Qed. `````` Robbert Krebbers committed Aug 21, 2012 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 committed Jun 11, 2012 62 `````` Proof. intros. now apply (elem_of_map _). Qed. `````` Robbert Krebbers committed Aug 29, 2012 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 committed Jun 11, 2012 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 `````` Robbert Krebbers committed Aug 29, 2012 74 `````` | H : context [ _ ∈ ∅ ] |- _ => setoid_rewrite elem_of_empty in H `````` Robbert Krebbers committed Aug 21, 2012 75 `````` | H : context [ _ ∈ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H `````` Robbert Krebbers committed Jun 11, 2012 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 `````` Robbert Krebbers committed Aug 29, 2012 82 `````` | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty `````` Robbert Krebbers committed Aug 21, 2012 83 `````` | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton `````` Robbert Krebbers committed Jun 11, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 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 committed Jun 11, 2012 94 `````` simpl in *; `````` Robbert Krebbers committed Aug 29, 2012 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 committed Jun 11, 2012 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. `````` Robbert Krebbers committed Aug 21, 2012 144 145 `````` * rewrite <-E1, <-E2; intuition. * rewrite E1, E2; intuition. `````` Robbert Krebbers committed Jun 11, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 151 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 152 `````` Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅. `````` Robbert Krebbers committed Aug 29, 2012 153 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 154 `````` Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y. `````` Robbert Krebbers committed Aug 29, 2012 155 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 156 `````` `````` Robbert Krebbers committed Aug 21, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 159 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 160 `````` Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y. `````` Robbert Krebbers committed Aug 29, 2012 161 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 162 163 `````` Lemma no_dup_empty: no_dup ∅. `````` Robbert Krebbers committed Aug 29, 2012 164 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 165 `````` Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({[ x ]} ∪ X). `````` Robbert Krebbers committed Aug 29, 2012 166 `````` Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 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 [??]]. `````` Robbert Krebbers committed Aug 29, 2012 170 `````` rewrite (Hnodup x y) in Hin; solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 171 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 172 `````` Lemma no_dup_inv_union_l X Y : no_dup (X ∪ Y) → no_dup X. `````` Robbert Krebbers committed Aug 29, 2012 173 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 174 `````` Lemma no_dup_inv_union_r X Y : no_dup (X ∪ Y) → no_dup Y. `````` Robbert Krebbers committed Aug 29, 2012 175 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 176 177 ``````End no_dup. `````` Robbert Krebbers committed Aug 29, 2012 178 ``````(** * Quantifiers *) `````` Robbert Krebbers committed Jun 11, 2012 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 ∅. `````` Robbert Krebbers committed Aug 29, 2012 186 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 187 `````` Lemma cforall_singleton x : cforall {[ x ]} ↔ P x. `````` Robbert Krebbers committed Aug 29, 2012 188 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 189 `````` Lemma cforall_union X Y : cforall X → cforall Y → cforall (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 190 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 191 `````` Lemma cforall_union_inv_1 X Y : cforall (X ∪ Y) → cforall X. `````` Robbert Krebbers committed Aug 29, 2012 192 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 193 `````` Lemma cforall_union_inv_2 X Y : cforall (X ∪ Y) → cforall Y. `````` Robbert Krebbers committed Aug 29, 2012 194 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 195 196 `````` Lemma cexists_empty : ¬cexists ∅. `````` Robbert Krebbers committed Aug 29, 2012 197 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 198 `````` Lemma cexists_singleton x : cexists {[ x ]} ↔ P x. `````` Robbert Krebbers committed Aug 29, 2012 199 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 200 `````` Lemma cexists_union_1 X Y : cexists X → cexists (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 201 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 202 `````` Lemma cexists_union_2 X Y : cexists Y → cexists (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 203 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 204 `````` Lemma cexists_union_inv X Y : cexists (X ∪ Y) → cexists X ∨ cexists Y. `````` Robbert Krebbers committed Aug 29, 2012 205 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 206 207 ``````End quantifiers. `````` Robbert Krebbers committed Aug 21, 2012 208 209 ``````Section more_quantifiers. Context `{Collection A B}. `````` Robbert Krebbers committed Aug 29, 2012 210 `````` `````` Robbert Krebbers committed Aug 21, 2012 211 212 `````` Lemma cforall_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X : cforall P X → cforall Q X. `````` Robbert Krebbers committed Aug 29, 2012 213 `````` Proof. unfold cforall. naive_solver. Qed. `````` Robbert Krebbers committed Aug 21, 2012 214 215 `````` Lemma cexists_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X : cexists P X → cexists Q X. `````` Robbert Krebbers committed Aug 29, 2012 216 `````` Proof. unfold cexists. naive_solver. Qed. `````` Robbert Krebbers committed Aug 21, 2012 217 218 ``````End more_quantifiers. `````` Robbert Krebbers committed Aug 29, 2012 219 220 221 ``````(** * Fresh elements *) (** We collect some properties on the [fresh] operation. In particular we generalize [fresh] to generate lists of fresh elements. *) `````` Robbert Krebbers committed Aug 21, 2012 222 223 224 ``````Section fresh. Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} . `````` Robbert Krebbers committed Aug 29, 2012 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. `````` Robbert Krebbers committed Aug 21, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 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. `````` Robbert Krebbers committed Aug 21, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 254 `````` + apply IHn in Hin. solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 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. `````` Robbert Krebbers committed Aug 29, 2012 262 `````` solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 263 264 `````` Qed. End fresh.``````