collections.v 20.1 KB
 Robbert Krebbers committed May 02, 2014 1 ``````(* Copyright (c) 2012-2014, 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 May 02, 2014 8 9 10 ``````Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y, ∀ x, x ∈ X → x ∈ Y. `````` Robbert Krebbers committed Feb 19, 2013 11 ``````(** * Basic theorems *) `````` Robbert Krebbers committed Nov 12, 2012 12 13 ``````Section simple_collection. Context `{SimpleCollection A C}. `````` Robbert Krebbers committed Jun 11, 2012 14 `````` `````` Robbert Krebbers committed Aug 29, 2012 15 `````` Lemma elem_of_empty x : x ∈ ∅ ↔ False. `````` Robbert Krebbers committed Oct 19, 2012 16 `````` Proof. split. apply not_elem_of_empty. done. Qed. `````` Robbert Krebbers committed Jun 11, 2012 17 18 19 20 21 `````` 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 Nov 12, 2012 22 `````` Global Instance: BoundedJoinSemiLattice C. `````` Robbert Krebbers committed Oct 19, 2012 23 `````` Proof. firstorder auto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 24 25 `````` Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y. `````` Robbert Krebbers committed Oct 19, 2012 26 `````` Proof. done. Qed. `````` Robbert Krebbers committed Jun 11, 2012 27 28 `````` Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y. Proof. firstorder. Qed. `````` Robbert Krebbers committed Aug 21, 2012 29 30 `````` 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 31 `````` Proof. firstorder. Qed. `````` Robbert Krebbers committed Feb 19, 2013 32 33 34 `````` Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Proof. firstorder. Qed. `````` Robbert Krebbers committed Oct 19, 2012 35 36 37 `````` Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X. Proof. split. `````` Robbert Krebbers committed May 02, 2014 38 `````` * intros ??. rewrite elem_of_singleton. by intros ->. `````` Robbert Krebbers committed Oct 19, 2012 39 40 `````` * intros Ex. by apply (Ex x), elem_of_singleton. Qed. `````` Robbert Krebbers committed Aug 29, 2012 41 `````` Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton. `````` Robbert Krebbers committed May 02, 2014 42 `````` Proof. by repeat intro; subst. Qed. `````` Robbert Krebbers committed Nov 12, 2012 43 `````` Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5. `````` Robbert Krebbers committed May 02, 2014 44 `````` Proof. intros ???; subst. firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 45 `````` `````` Robbert Krebbers committed May 07, 2013 46 `````` Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. `````` Robbert Krebbers committed Oct 19, 2012 47 48 `````` Proof. split. `````` Robbert Krebbers committed May 02, 2014 49 50 51 52 `````` * induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |]. intros. apply elem_of_union_r; auto. `````` Robbert Krebbers committed Oct 19, 2012 53 54 55 56 57 58 59 60 61 `````` 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 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 `````` 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 83 84 ``````End simple_collection. `````` Robbert Krebbers committed Feb 19, 2013 85 86 87 88 89 90 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 ``````(** * 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 119 120 ``````Ltac decompose_empty := repeat match goal with `````` Robbert Krebbers committed Feb 19, 2013 121 122 123 124 `````` | H : ∅ ≡ ∅ |- _ => clear H | H : ∅ = ∅ |- _ => clear H | H : ∅ ≡ _ |- _ => symmetry in H | H : ∅ = _ |- _ => symmetry in H `````` Robbert Krebbers committed Oct 19, 2012 125 126 127 `````` | 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 128 129 130 `````` | 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 131 132 `````` end. `````` Robbert Krebbers committed Feb 19, 2013 133 134 135 136 ``````(** 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 137 138 139 140 ``````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 141 `````` | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H `````` Robbert Krebbers committed Feb 19, 2013 142 `````` | context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty in H `````` Robbert Krebbers committed Oct 19, 2012 143 `````` | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H `````` Robbert Krebbers committed Feb 19, 2013 144 145 `````` | 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 146 147 148 149 150 `````` | 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 151 152 153 154 `````` | 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 155 156 `````` end); repeat match goal with `````` Robbert Krebbers committed Jun 11, 2012 157 `````` | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq `````` Robbert Krebbers committed Jan 05, 2013 158 `````` | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec `````` Robbert Krebbers committed Feb 19, 2013 159 `````` | |- context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty `````` Robbert Krebbers committed Jun 11, 2012 160 `````` | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt `````` Robbert Krebbers committed Feb 19, 2013 161 162 `````` | |- context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L `````` Robbert Krebbers committed Aug 29, 2012 163 `````` | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty `````` Robbert Krebbers committed Aug 21, 2012 164 `````` | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton `````` Robbert Krebbers committed Jun 11, 2012 165 166 167 `````` | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference `````` Robbert Krebbers committed Nov 12, 2012 168 169 170 171 `````` | |- 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 172 173 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 174 175 176 ``````(** 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 177 ``````Tactic Notation "solve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Jun 11, 2012 178 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 179 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 180 181 182 183 184 185 186 187 188 `````` 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 189 ``````Tactic Notation "esolve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Aug 29, 2012 190 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 191 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 192 193 194 `````` unfold_elem_of; naive_solver tac. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. `````` Robbert Krebbers committed Feb 19, 2013 195 196 `````` (** * More theorems *) `````` Robbert Krebbers committed Jan 05, 2013 197 198 199 200 ``````Section collection. Context `{Collection A C}. Global Instance: LowerBoundedLattice C. `````` Robbert Krebbers committed May 02, 2014 201 `````` Proof. split. apply _. firstorder auto. solve_elem_of. Qed. `````` Robbert Krebbers committed Jan 05, 2013 202 203 204 205 206 207 208 209 210 211 212 213 214 215 `````` 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 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 `````` 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. `````` Robbert Krebbers committed May 02, 2014 236 `````` Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 237 `````` Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y. `````` Robbert Krebbers committed May 02, 2014 238 `````` Proof. rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 239 240 `````` Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X. Proof. `````` Robbert Krebbers committed May 02, 2014 241 242 `````` split; intros x; rewrite !elem_of_union, elem_of_difference; [|intuition]. destruct (decide (x ∈ X)); intuition. `````` Robbert Krebbers committed Feb 19, 2013 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 `````` 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 261 262 263 264 265 `````` 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. `````` Robbert Krebbers committed May 02, 2014 266 267 268 269 `````` * revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|]. rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?). destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial. eexists (x1 :: xs), y. intuition (simplify_option_equality; auto). `````` Robbert Krebbers committed Jan 05, 2013 270 271 272 273 274 275 276 277 278 279 280 `````` * 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. `````` Robbert Krebbers committed May 07, 2013 281 `````` intros HY HXs Hf. induction Xs; simplify_option_equality; [done |]. `````` Robbert Krebbers committed Jan 05, 2013 282 283 284 `````` intros x Hx. rewrite elem_of_intersection_with in Hx. decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 285 ``````End collection_ops. `````` Robbert Krebbers committed Jan 05, 2013 286 `````` `````` Robbert Krebbers committed Aug 29, 2012 287 ``````(** * Sets without duplicates up to an equivalence *) `````` Robbert Krebbers committed May 07, 2013 288 ``````Section NoDup. `````` Robbert Krebbers committed Nov 12, 2012 289 `````` Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}. `````` Robbert Krebbers committed Jun 11, 2012 290 291 `````` Definition elem_of_upto (x : A) (X : B) := ∃ y, y ∈ X ∧ R x y. `````` Robbert Krebbers committed May 07, 2013 292 `````` Definition set_NoDup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y. `````` Robbert Krebbers committed Jun 11, 2012 293 294 `````` Global Instance: Proper ((≡) ==> iff) (elem_of_upto x). `````` Robbert Krebbers committed Jan 05, 2013 295 `````` Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed. `````` Robbert Krebbers committed Jun 11, 2012 296 297 298 `````` Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto. Proof. intros ?? E1 ?? E2. split; intros [z [??]]; exists z. `````` Robbert Krebbers committed Aug 21, 2012 299 300 `````` * rewrite <-E1, <-E2; intuition. * rewrite E1, E2; intuition. `````` Robbert Krebbers committed Jun 11, 2012 301 `````` Qed. `````` Robbert Krebbers committed May 07, 2013 302 `````` Global Instance: Proper ((≡) ==> iff) set_NoDup. `````` Robbert Krebbers committed Jun 11, 2012 303 304 305 `````` Proof. firstorder. Qed. Lemma elem_of_upto_elem_of x X : x ∈ X → elem_of_upto x X. `````` Robbert Krebbers committed Aug 29, 2012 306 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 307 `````` Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅. `````` Robbert Krebbers committed Aug 29, 2012 308 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 309 `````` Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y. `````` Robbert Krebbers committed Aug 29, 2012 310 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 311 `````` `````` Robbert Krebbers committed Aug 21, 2012 312 313 `````` 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 314 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 315 `````` Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y. `````` Robbert Krebbers committed Aug 29, 2012 316 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 317 `````` `````` Robbert Krebbers committed May 07, 2013 318 319 320 321 322 323 324 `````` Lemma set_NoDup_empty: set_NoDup ∅. Proof. unfold set_NoDup. solve_elem_of. Qed. Lemma set_NoDup_add x X : ¬elem_of_upto x X → set_NoDup X → set_NoDup ({[ x ]} ∪ X). Proof. unfold set_NoDup, elem_of_upto. esolve_elem_of. Qed. Lemma set_NoDup_inv_add x X : x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X. `````` Robbert Krebbers committed Aug 21, 2012 325 326 `````` Proof. intros Hin Hnodup [y [??]]. `````` Robbert Krebbers committed Aug 29, 2012 327 `````` rewrite (Hnodup x y) in Hin; solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 328 `````` Qed. `````` Robbert Krebbers committed May 07, 2013 329 330 331 332 333 `````` Lemma set_NoDup_inv_union_l X Y : set_NoDup (X ∪ Y) → set_NoDup X. Proof. unfold set_NoDup. solve_elem_of. Qed. Lemma set_NoDup_inv_union_r X Y : set_NoDup (X ∪ Y) → set_NoDup Y. Proof. unfold set_NoDup. solve_elem_of. Qed. End NoDup. `````` Robbert Krebbers committed Jun 11, 2012 334 `````` `````` Robbert Krebbers committed Aug 29, 2012 335 ``````(** * Quantifiers *) `````` Robbert Krebbers committed Jun 11, 2012 336 ``````Section quantifiers. `````` Robbert Krebbers committed Nov 12, 2012 337 `````` Context `{SimpleCollection A B} (P : A → Prop). `````` Robbert Krebbers committed Jun 11, 2012 338 `````` `````` Robbert Krebbers committed May 07, 2013 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 `````` Definition set_Forall X := ∀ x, x ∈ X → P x. Definition set_Exists X := ∃ x, x ∈ X ∧ P x. Lemma set_Forall_empty : set_Forall ∅. Proof. unfold set_Forall. solve_elem_of. Qed. Lemma set_Forall_singleton x : set_Forall {[ x ]} ↔ P x. Proof. unfold set_Forall. solve_elem_of. Qed. Lemma set_Forall_union X Y : set_Forall X → set_Forall Y → set_Forall (X ∪ Y). Proof. unfold set_Forall. solve_elem_of. Qed. Lemma set_Forall_union_inv_1 X Y : set_Forall (X ∪ Y) → set_Forall X. Proof. unfold set_Forall. solve_elem_of. Qed. Lemma set_Forall_union_inv_2 X Y : set_Forall (X ∪ Y) → set_Forall Y. Proof. unfold set_Forall. solve_elem_of. Qed. Lemma set_Exists_empty : ¬set_Exists ∅. Proof. unfold set_Exists. esolve_elem_of. Qed. Lemma set_Exists_singleton x : set_Exists {[ x ]} ↔ P x. Proof. unfold set_Exists. esolve_elem_of. Qed. Lemma set_Exists_union_1 X Y : set_Exists X → set_Exists (X ∪ Y). Proof. unfold set_Exists. esolve_elem_of. Qed. Lemma set_Exists_union_2 X Y : set_Exists Y → set_Exists (X ∪ Y). Proof. unfold set_Exists. esolve_elem_of. Qed. Lemma set_Exists_union_inv X Y : set_Exists (X ∪ Y) → set_Exists X ∨ set_Exists Y. Proof. unfold set_Exists. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 364 365 ``````End quantifiers. `````` Robbert Krebbers committed Aug 21, 2012 366 367 ``````Section more_quantifiers. Context `{Collection A B}. `````` Robbert Krebbers committed Aug 29, 2012 368 `````` `````` Robbert Krebbers committed May 07, 2013 369 370 371 372 373 374 `````` Lemma set_Forall_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X : set_Forall P X → set_Forall Q X. Proof. unfold set_Forall. naive_solver. Qed. Lemma set_Exists_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X : set_Exists P X → set_Exists Q X. Proof. unfold set_Exists. naive_solver. Qed. `````` Robbert Krebbers committed Aug 21, 2012 375 376 ``````End more_quantifiers. `````` Robbert Krebbers committed Aug 29, 2012 377 378 379 ``````(** * 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 380 ``````Section fresh. `````` Robbert Krebbers committed Nov 12, 2012 381 `````` Context `{FreshSpec A C} . `````` Robbert Krebbers committed Aug 21, 2012 382 `````` `````` Robbert Krebbers committed Aug 29, 2012 383 384 385 386 `````` 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 387 `````` Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed. `````` Robbert Krebbers committed Aug 29, 2012 388 `````` `````` Robbert Krebbers committed Aug 21, 2012 389 390 391 392 393 394 `````` 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 395 396 `````` Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list. Proof. `````` Robbert Krebbers committed May 02, 2014 397 398 `````` intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|]. apply IH. by rewrite E. `````` Robbert Krebbers committed Aug 29, 2012 399 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 400 401 `````` 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 402 `````` Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X. `````` Robbert Krebbers committed Aug 21, 2012 403 `````` Proof. `````` Robbert Krebbers committed May 02, 2014 404 405 406 `````` revert X. induction n as [|n IH]; intros X; simpl; [by rewrite elem_of_nil|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. apply IH in Hin; solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 407 408 409 `````` Qed. Lemma fresh_list_nodup n X : NoDup (fresh_list n X). Proof. `````` Robbert Krebbers committed May 07, 2013 410 411 `````` revert X. induction n; simpl; constructor; auto. intros Hin. apply fresh_list_is_fresh in Hin. solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 412 413 `````` Qed. End fresh. `````` Robbert Krebbers committed Nov 12, 2012 414 415 `````` Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C := `````` Robbert Krebbers committed May 02, 2014 416 `````` match x with None => ∅ | Some a => {[ a ]} end. `````` Robbert Krebbers committed Nov 12, 2012 417 `````` `````` Robbert Krebbers committed Feb 19, 2013 418 ``````(** * Properties of implementations of collections that form a monad *) `````` Robbert Krebbers committed Nov 12, 2012 419 420 421 422 ``````Section collection_monad. Context `{CollectionMonad M}. Global Instance collection_guard: MGuard M := λ P dec A x, `````` Robbert Krebbers committed May 02, 2014 423 `````` match dec with left H => x H | _ => ∅ end. `````` Robbert Krebbers committed Nov 12, 2012 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 `````` 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. `````` Robbert Krebbers committed Jun 17, 2013 458 `````` Lemma collection_mapM_length {A B} (f : A → M B) l k : `````` Robbert Krebbers committed Nov 12, 2012 459 460 461 462 `````` 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 : `````` Robbert Krebbers committed May 07, 2013 463 `````` Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. `````` Robbert Krebbers committed Nov 12, 2012 464 `````` Proof. `````` Robbert Krebbers committed May 02, 2014 465 466 `````` intros Hl. revert k. induction Hl; simpl; intros; decompose_elem_of; f_equal'; auto. `````` Robbert Krebbers committed Nov 12, 2012 467 468 469 `````` Qed. Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k : `````` Robbert Krebbers committed May 07, 2013 470 `````` l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l. `````` Robbert Krebbers committed Jan 05, 2013 471 `````` Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed. `````` Robbert Krebbers committed May 07, 2013 472 473 `````` Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P: B → C → Prop) l1 l2 k : l1 ∈ mapM f k → Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 → `````` Robbert Krebbers committed Jan 05, 2013 474 475 476 477 478 `````` 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 479 ``End collection_monad.``