collections.v 20.1 KB
 Robbert Krebbers committed Feb 19, 2013 1 ``````(* Copyright (c) 2012-2013, Robbert Krebbers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 3 4 5 6 7 ``````(* 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. `````` Robbert Krebbers committed Feb 19, 2013 8 ``````(** * Basic theorems *) `````` Robbert Krebbers committed Nov 12, 2012 9 10 ``````Section simple_collection. Context `{SimpleCollection A C}. `````` Robbert Krebbers committed Jun 11, 2012 11 `````` `````` Robbert Krebbers committed Aug 29, 2012 12 `````` Lemma elem_of_empty x : x ∈ ∅ ↔ False. `````` Robbert Krebbers committed Oct 19, 2012 13 `````` Proof. split. apply not_elem_of_empty. done. Qed. `````` Robbert Krebbers committed Jun 11, 2012 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. `````` Robbert Krebbers committed Oct 19, 2012 19 `````` Global Instance collection_subseteq: SubsetEq C := λ X Y, `````` Robbert Krebbers committed Aug 29, 2012 20 `````` ∀ x, x ∈ X → x ∈ Y. `````` Robbert Krebbers committed Nov 12, 2012 21 `````` Global Instance: BoundedJoinSemiLattice C. `````` Robbert Krebbers committed Oct 19, 2012 22 `````` Proof. firstorder auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 23 24 `````` Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y. `````` Robbert Krebbers committed Oct 19, 2012 25 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jun 11, 2012 26 27 `````` Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y. Proof. firstorder. Qed. `````` Robbert Krebbers committed Aug 21, 2012 28 29 `````` 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 30 `````` Proof. firstorder. Qed. `````` Robbert Krebbers committed Feb 19, 2013 31 32 33 `````` Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Proof. firstorder. Qed. `````` Robbert Krebbers committed Oct 19, 2012 34 35 36 37 38 39 `````` 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. `````` Robbert Krebbers committed Aug 29, 2012 40 `````` Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton. `````` Robbert Krebbers committed Oct 19, 2012 41 `````` Proof. repeat intro. by subst. Qed. `````` Robbert Krebbers committed Nov 12, 2012 42 `````` Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5. `````` Robbert Krebbers committed Jun 11, 2012 43 44 `````` Proof. intros ???. subst. firstorder. Qed. `````` Robbert Krebbers committed Jan 05, 2013 45 `````` Lemma elem_of_union_list (Xs : list C) (x : A) : `````` Robbert Krebbers committed Nov 12, 2012 46 `````` x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. `````` Robbert Krebbers committed Oct 19, 2012 47 48 49 50 `````` Proof. split. * induction Xs; simpl; intros HXs. + by apply elem_of_empty in HXs. `````` Robbert Krebbers committed Nov 12, 2012 51 52 53 `````` + setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. * intros [X []]. induction 1; simpl. `````` Robbert Krebbers committed Oct 19, 2012 54 `````` + by apply elem_of_union_l. `````` Robbert Krebbers committed Nov 12, 2012 55 `````` + intros. apply elem_of_union_r; auto. `````` Robbert Krebbers committed Oct 19, 2012 56 57 58 59 60 61 62 63 64 65 `````` 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. `````` Robbert Krebbers committed Feb 19, 2013 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 `````` Section leibniz. Context `{!LeibnizEquiv C}. Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y. Proof. unfold_leibniz. apply elem_of_equiv. Qed. Lemma elem_of_equiv_alt_L X Y : X = Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X). Proof. unfold_leibniz. apply elem_of_equiv_alt. Qed. Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X. Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed. Lemma non_empty_singleton_L x : {[ x ]} ≠ ∅. Proof. unfold_leibniz. apply non_empty_singleton. Qed. End leibniz. Section dec. 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. End dec. `````` Robbert Krebbers committed Nov 12, 2012 89 90 ``````End simple_collection. `````` Robbert Krebbers committed Feb 19, 2013 91 92 93 94 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 ``````(** * Tactics *) (** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *) Tactic Notation "decompose_elem_of" hyp(H) := let rec go H := lazymatch type of H with | _ ∈ ∅ => apply elem_of_empty in H; destruct H | ?x ∈ {[ ?y ]} => apply elem_of_singleton in H; try first [subst y | subst x] | _ ∈ _ ∪ _ => 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 | ?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 | _ => idtac end in go H. Tactic Notation "decompose_elem_of" := repeat_on_hyps (fun H => decompose_elem_of H). `````` Robbert Krebbers committed Oct 19, 2012 125 126 ``````Ltac decompose_empty := repeat match goal with `````` Robbert Krebbers committed Feb 19, 2013 127 128 129 130 `````` | H : ∅ ≡ ∅ |- _ => clear H | H : ∅ = ∅ |- _ => clear H | H : ∅ ≡ _ |- _ => symmetry in H | H : ∅ = _ |- _ => symmetry in H `````` Robbert Krebbers committed Oct 19, 2012 131 132 133 `````` | H : _ ∪ _ ≡ ∅ |- _ => apply empty_union in H; destruct H | H : _ ∪ _ ≢ ∅ |- _ => apply non_empty_union in H; destruct H | H : {[ _ ]} ≡ ∅ |- _ => destruct (non_empty_singleton _ H) `````` Robbert Krebbers committed Feb 19, 2013 134 135 136 `````` | H : _ ∪ _ = ∅ |- _ => apply empty_union_L in H; destruct H | H : _ ∪ _ ≠ ∅ |- _ => apply non_empty_union_L in H; destruct H | H : {[ _ ]} = ∅ |- _ => destruct (non_empty_singleton_L _ H) `````` Robbert Krebbers committed Oct 19, 2012 137 138 `````` end. `````` Robbert Krebbers committed Feb 19, 2013 139 140 141 142 ``````(** The first pass of our collection tactic consists of eliminating all occurrences of [(∪)], [(∩)], [(∖)], [(<\$>)], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *) `````` Robbert Krebbers committed Oct 19, 2012 143 144 145 146 ``````Ltac unfold_elem_of := repeat_on_hyps (fun H => repeat match type of H with | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H `````` Robbert Krebbers committed Jan 05, 2013 147 `````` | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H `````` Robbert Krebbers committed Feb 19, 2013 148 `````` | context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty in H `````` Robbert Krebbers committed Oct 19, 2012 149 `````` | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H `````` Robbert Krebbers committed Feb 19, 2013 150 151 `````` | context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L in H | context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H `````` Robbert Krebbers committed Oct 19, 2012 152 153 154 155 156 `````` | 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 `````` Robbert Krebbers committed Nov 12, 2012 157 158 159 160 `````` | 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 `````` Robbert Krebbers committed Oct 19, 2012 161 162 `````` end); repeat match goal with `````` Robbert Krebbers committed Jun 11, 2012 163 `````` | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq `````` Robbert Krebbers committed Jan 05, 2013 164 `````` | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec `````` Robbert Krebbers committed Feb 19, 2013 165 `````` | |- context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty `````` Robbert Krebbers committed Jun 11, 2012 166 `````` | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt `````` Robbert Krebbers committed Feb 19, 2013 167 168 `````` | |- context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L `````` Robbert Krebbers committed Aug 29, 2012 169 `````` | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty `````` Robbert Krebbers committed Aug 21, 2012 170 `````` | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton `````` Robbert Krebbers committed Jun 11, 2012 171 172 173 `````` | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference `````` Robbert Krebbers committed Nov 12, 2012 174 175 176 177 `````` | |- 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 committed Jun 11, 2012 178 179 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 180 181 182 ``````(** 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. *) `````` Robbert Krebbers committed Oct 19, 2012 183 ``````Tactic Notation "solve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Jun 11, 2012 184 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 185 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 186 187 188 189 190 191 192 193 194 `````` 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. *) `````` Robbert Krebbers committed Oct 19, 2012 195 ``````Tactic Notation "esolve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Aug 29, 2012 196 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 197 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 198 199 200 `````` unfold_elem_of; naive_solver tac. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. `````` Robbert Krebbers committed Feb 19, 2013 201 202 `````` (** * More theorems *) `````` Robbert Krebbers committed Jan 05, 2013 203 204 205 206 ``````Section collection. Context `{Collection A C}. Global Instance: LowerBoundedLattice C. `````` Robbert Krebbers committed Feb 19, 2013 207 208 209 210 211 212 `````` Proof. split. * apply _. * firstorder auto. * solve_elem_of. Qed. `````` Robbert Krebbers committed Jan 05, 2013 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 `````` Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}. Proof. esolve_elem_of. Qed. Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y. Proof. esolve_elem_of. Qed. Lemma empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅. Proof. esolve_elem_of. Qed. Lemma difference_diag X : X ∖ X ≡ ∅. Proof. esolve_elem_of. Qed. Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z. Proof. esolve_elem_of. Qed. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Proof. esolve_elem_of. Qed. `````` Robbert Krebbers committed Feb 19, 2013 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 `````` Section leibniz. Context `{!LeibnizEquiv C}. Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = {[x]}. Proof. unfold_leibniz. apply intersection_singletons. Qed. Lemma difference_twice_L X Y : (X ∖ Y) ∖ Y = X ∖ Y. Proof. unfold_leibniz. apply difference_twice. Qed. Lemma empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅. Proof. unfold_leibniz. apply empty_difference. Qed. Lemma difference_diag_L X : X ∖ X = ∅. Proof. unfold_leibniz. apply difference_diag. Qed. Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z. Proof. unfold_leibniz. apply difference_union_distr_l. Qed. Lemma difference_intersection_distr_l_L X Y Z : (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. End leibniz. Section dec. Context `{∀ X Y : C, Decision (X ⊆ Y)}. 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 → Y ≡ X ∪ Y ∖ X. Proof. split; intros x; rewrite !elem_of_union, elem_of_difference. * destruct (decide (x ∈ X)); intuition. * intuition. Qed. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x. destruct (decide (x ∈ X)); esolve_elem_of. Qed. Context `{!LeibnizEquiv C}. Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. unfold_leibniz. apply union_difference. Qed. Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅. Proof. unfold_leibniz. apply non_empty_difference. Qed. End dec. End collection. Section collection_ops. Context `{CollectionOps A C}. `````` Robbert Krebbers committed Jan 05, 2013 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 `````` Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x : x ∈ intersection_with_list f Y Xs ↔ ∃ xs y, Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x. Proof. split. * revert x. induction Xs; simpl; intros x HXs. + eexists [], x. intuition. + rewrite elem_of_intersection_with in HXs. destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?). destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial. eexists (x1 :: xs), y. intuition (simplify_option_equality; auto). * intros (xs & y & Hxs & ? & Hx). revert x Hx. induction Hxs; intros; simplify_option_equality; [done |]. rewrite elem_of_intersection_with. naive_solver. Qed. Lemma intersection_with_list_ind (P Q : A → Prop) f Xs Y : (∀ y, y ∈ Y → P y) → Forall (λ X, ∀ x, x ∈ X → Q x) Xs → (∀ x y z, Q x → P y → f x y = Some z → P z) → ∀ x, x ∈ intersection_with_list f Y Xs → P x. Proof. intros HY HXs Hf. induction Xs; simplify_option_equality; [done |]. intros x Hx. rewrite elem_of_intersection_with in Hx. decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 311 ``````End collection_ops. `````` Robbert Krebbers committed Jan 05, 2013 312 `````` `````` Robbert Krebbers committed Aug 29, 2012 313 ``````(** * Sets without duplicates up to an equivalence *) `````` Robbert Krebbers committed Jun 11, 2012 314 ``````Section no_dup. `````` Robbert Krebbers committed Nov 12, 2012 315 `````` Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}. `````` Robbert Krebbers committed Jun 11, 2012 316 317 318 319 320 `````` 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). `````` Robbert Krebbers committed Jan 05, 2013 321 `````` Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed. `````` Robbert Krebbers committed Jun 11, 2012 322 323 324 `````` Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto. Proof. intros ?? E1 ?? E2. split; intros [z [??]]; exists z. `````` Robbert Krebbers committed Aug 21, 2012 325 326 `````` * rewrite <-E1, <-E2; intuition. * rewrite E1, E2; intuition. `````` Robbert Krebbers committed Jun 11, 2012 327 328 329 330 331 `````` 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 332 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 333 `````` Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅. `````` Robbert Krebbers committed Aug 29, 2012 334 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 335 `````` Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y. `````` Robbert Krebbers committed Aug 29, 2012 336 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 337 `````` `````` Robbert Krebbers committed Aug 21, 2012 338 339 `````` 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 340 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 341 `````` Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y. `````` Robbert Krebbers committed Aug 29, 2012 342 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 343 344 `````` Lemma no_dup_empty: no_dup ∅. `````` Robbert Krebbers committed Aug 29, 2012 345 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 346 `````` Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({[ x ]} ∪ X). `````` Robbert Krebbers committed Aug 29, 2012 347 `````` Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 348 349 350 `````` 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 351 `````` rewrite (Hnodup x y) in Hin; solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 352 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 353 `````` Lemma no_dup_inv_union_l X Y : no_dup (X ∪ Y) → no_dup X. `````` Robbert Krebbers committed Aug 29, 2012 354 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 355 `````` Lemma no_dup_inv_union_r X Y : no_dup (X ∪ Y) → no_dup Y. `````` Robbert Krebbers committed Aug 29, 2012 356 `````` Proof. unfold no_dup. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 357 358 ``````End no_dup. `````` Robbert Krebbers committed Aug 29, 2012 359 ``````(** * Quantifiers *) `````` Robbert Krebbers committed Jun 11, 2012 360 ``````Section quantifiers. `````` Robbert Krebbers committed Nov 12, 2012 361 `````` Context `{SimpleCollection A B} (P : A → Prop). `````` Robbert Krebbers committed Jun 11, 2012 362 363 364 365 366 `````` 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 367 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 368 `````` Lemma cforall_singleton x : cforall {[ x ]} ↔ P x. `````` Robbert Krebbers committed Aug 29, 2012 369 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 370 `````` Lemma cforall_union X Y : cforall X → cforall Y → cforall (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 371 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 372 `````` Lemma cforall_union_inv_1 X Y : cforall (X ∪ Y) → cforall X. `````` Robbert Krebbers committed Aug 29, 2012 373 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 374 `````` Lemma cforall_union_inv_2 X Y : cforall (X ∪ Y) → cforall Y. `````` Robbert Krebbers committed Aug 29, 2012 375 `````` Proof. unfold cforall. solve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 376 377 `````` Lemma cexists_empty : ¬cexists ∅. `````` Robbert Krebbers committed Aug 29, 2012 378 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 379 `````` Lemma cexists_singleton x : cexists {[ x ]} ↔ P x. `````` Robbert Krebbers committed Aug 29, 2012 380 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 381 `````` Lemma cexists_union_1 X Y : cexists X → cexists (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 382 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 383 `````` Lemma cexists_union_2 X Y : cexists Y → cexists (X ∪ Y). `````` Robbert Krebbers committed Aug 29, 2012 384 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 385 `````` Lemma cexists_union_inv X Y : cexists (X ∪ Y) → cexists X ∨ cexists Y. `````` Robbert Krebbers committed Aug 29, 2012 386 `````` Proof. unfold cexists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 387 388 ``````End quantifiers. `````` Robbert Krebbers committed Aug 21, 2012 389 390 ``````Section more_quantifiers. Context `{Collection A B}. `````` Robbert Krebbers committed Aug 29, 2012 391 `````` `````` Robbert Krebbers committed Oct 19, 2012 392 `````` Lemma cforall_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X : `````` Robbert Krebbers committed Aug 21, 2012 393 `````` cforall P X → cforall Q X. `````` Robbert Krebbers committed Aug 29, 2012 394 `````` Proof. unfold cforall. naive_solver. Qed. `````` Robbert Krebbers committed Oct 19, 2012 395 `````` Lemma cexists_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X : `````` Robbert Krebbers committed Aug 21, 2012 396 `````` cexists P X → cexists Q X. `````` Robbert Krebbers committed Aug 29, 2012 397 `````` Proof. unfold cexists. naive_solver. Qed. `````` Robbert Krebbers committed Aug 21, 2012 398 399 ``````End more_quantifiers. `````` Robbert Krebbers committed Aug 29, 2012 400 401 402 ``````(** * 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 403 ``````Section fresh. `````` Robbert Krebbers committed Nov 12, 2012 404 `````` Context `{FreshSpec A C} . `````` Robbert Krebbers committed Aug 21, 2012 405 `````` `````` Robbert Krebbers committed Aug 29, 2012 406 407 408 409 `````` Definition fresh_sig (X : C) : { x : A | x ∉ X } := exist (∉ X) (fresh X) (is_fresh X). Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh. `````` Robbert Krebbers committed Oct 19, 2012 410 `````` Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed. `````` Robbert Krebbers committed Aug 29, 2012 411 `````` `````` Robbert Krebbers committed Aug 21, 2012 412 413 414 415 416 417 `````` 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 418 419 420 421 `````` Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list. Proof. intros ? n ?. subst. induction n; simpl; intros ?? E; f_equal. `````` Robbert Krebbers committed Oct 19, 2012 422 423 `````` * by rewrite E. * apply IHn. by rewrite E. `````` Robbert Krebbers committed Aug 29, 2012 424 425 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 426 427 428 `````` Lemma fresh_list_length n X : length (fresh_list n X) = n. Proof. revert X. induction n; simpl; auto. Qed. `````` Robbert Krebbers committed Nov 12, 2012 429 `````` Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X. `````` Robbert Krebbers committed Aug 21, 2012 430 `````` Proof. `````` Robbert Krebbers committed Nov 12, 2012 431 432 433 `````` revert X. induction n; intros X; simpl. * by rewrite elem_of_nil. * rewrite elem_of_cons. intros [?| Hin]; subst. `````` Robbert Krebbers committed Aug 21, 2012 434 `````` + apply is_fresh. `````` Robbert Krebbers committed Aug 29, 2012 435 `````` + apply IHn in Hin. solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 436 437 438 439 440 441 442 `````` 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 443 `````` solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 444 445 `````` Qed. End fresh. `````` Robbert Krebbers committed Nov 12, 2012 446 447 448 449 450 451 452 `````` Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C := match x with | None => ∅ | Some a => {[ a ]} end. `````` Robbert Krebbers committed Feb 19, 2013 453 ``````(** * Properties of implementations of collections that form a monad *) `````` Robbert Krebbers committed Nov 12, 2012 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 ``````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. `````` Robbert Krebbers committed Jan 05, 2013 510 `````` Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed. `````` Robbert Krebbers committed Feb 19, 2013 511 512 `````` Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P : B → C → Prop) l1 l2 k : `````` Robbert Krebbers committed Jan 05, 2013 513 514 515 516 517 518 519 `````` l1 ∈ mapM f k → Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 → Forall2 P l1 l2. Proof. rewrite elem_of_mapM. intros Hl1. revert l2. induction Hl1; inversion_clear 1; constructor; auto. Qed. `````` Robbert Krebbers committed Nov 12, 2012 520 ``End collection_monad.``