collections.v 20.7 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 Jun 05, 2014 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 ``````Definition of_option `{Singleton A C} `{Empty C} (x : option A) : C := match x with None => ∅ | Some a => {[ a ]} end. Lemma elem_of_of_option `{SimpleCollection A C} (x : A) o : x ∈ of_option o ↔ o = Some x. Proof. destruct o; simpl; rewrite ?elem_of_empty, ?elem_of_singleton; naive_solver. Qed. Global Instance collection_guard `{CollectionMonad M} : MGuard M := λ P dec A x, match dec with left H => x H | _ => ∅ end. Lemma elem_of_guard `{CollectionMonad M} `{Decision P} {A} (x : A) (X : M A) : x ∈ guard P; X ↔ P ∧ x ∈ X. Proof. unfold mguard, collection_guard; simpl; case_match; rewrite ?elem_of_empty; naive_solver. Qed. `````` Robbert Krebbers committed Feb 19, 2013 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 ``````(** * 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 `````` Robbert Krebbers committed Jun 05, 2014 131 132 133 134 `````` | _ ∈ guard _; _ => let H1 := fresh in let H2 := fresh in apply elem_of_guard in H; destruct H as [H1 H2]; go H2 | _ ∈ of_option _ => apply elem_of_of_option in H `````` Robbert Krebbers committed Feb 19, 2013 135 136 137 138 139 `````` | _ => 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 140 141 ``````Ltac decompose_empty := repeat match goal with `````` Robbert Krebbers committed Feb 19, 2013 142 143 144 145 `````` | H : ∅ ≡ ∅ |- _ => clear H | H : ∅ = ∅ |- _ => clear H | H : ∅ ≡ _ |- _ => symmetry in H | H : ∅ = _ |- _ => symmetry in H `````` Robbert Krebbers committed Oct 19, 2012 146 147 148 `````` | 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 149 150 151 `````` | 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 152 153 `````` end. `````` Robbert Krebbers committed Feb 19, 2013 154 155 156 157 ``````(** 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 158 159 160 161 ``````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 162 `````` | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H `````` Robbert Krebbers committed Feb 19, 2013 163 `````` | context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty in H `````` Robbert Krebbers committed Oct 19, 2012 164 `````` | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H `````` Robbert Krebbers committed Feb 19, 2013 165 166 `````` | 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 167 168 169 170 171 `````` | 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 172 173 174 175 `````` | 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 176 177 `````` end); repeat match goal with `````` Robbert Krebbers committed Jun 11, 2012 178 `````` | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq `````` Robbert Krebbers committed Jan 05, 2013 179 `````` | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec `````` Robbert Krebbers committed Feb 19, 2013 180 `````` | |- context [ _ ≡ ∅ ] => setoid_rewrite elem_of_equiv_empty `````` Robbert Krebbers committed Jun 11, 2012 181 `````` | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt `````` Robbert Krebbers committed Feb 19, 2013 182 183 `````` | |- context [ _ = ∅ ] => setoid_rewrite elem_of_equiv_empty_L | |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L `````` Robbert Krebbers committed Aug 29, 2012 184 `````` | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty `````` Robbert Krebbers committed Aug 21, 2012 185 `````` | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton `````` Robbert Krebbers committed Jun 11, 2012 186 187 188 `````` | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference `````` Robbert Krebbers committed Nov 12, 2012 189 190 191 192 `````` | |- 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 193 194 `````` end. `````` Robbert Krebbers committed Aug 29, 2012 195 196 197 ``````(** 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 198 ``````Tactic Notation "solve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Jun 11, 2012 199 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 200 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 201 202 203 204 205 206 207 208 209 `````` 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 210 ``````Tactic Notation "esolve_elem_of" tactic3(tac) := `````` Robbert Krebbers committed Aug 29, 2012 211 `````` simpl in *; `````` Robbert Krebbers committed Feb 19, 2013 212 `````` decompose_empty; `````` Robbert Krebbers committed Aug 29, 2012 213 214 215 `````` unfold_elem_of; naive_solver tac. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. `````` Robbert Krebbers committed Feb 19, 2013 216 217 `````` (** * More theorems *) `````` Robbert Krebbers committed Jan 05, 2013 218 219 220 221 ``````Section collection. Context `{Collection A C}. Global Instance: LowerBoundedLattice C. `````` Robbert Krebbers committed May 02, 2014 222 `````` Proof. split. apply _. firstorder auto. solve_elem_of. Qed. `````` Robbert Krebbers committed Jan 05, 2013 223 224 225 226 227 228 229 230 231 232 233 234 235 236 `````` 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 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 `````` 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 257 `````` Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 258 `````` Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y. `````` Robbert Krebbers committed May 02, 2014 259 `````` Proof. rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 260 261 `````` Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X. Proof. `````` Robbert Krebbers committed May 02, 2014 262 263 `````` split; intros x; rewrite !elem_of_union, elem_of_difference; [|intuition]. destruct (decide (x ∈ X)); intuition. `````` Robbert Krebbers committed Feb 19, 2013 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 `````` 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 282 283 284 285 286 `````` 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 287 288 289 290 `````` * 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 291 292 293 294 295 296 297 298 299 300 301 `````` * 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 302 `````` intros HY HXs Hf. induction Xs; simplify_option_equality; [done |]. `````` Robbert Krebbers committed Jan 05, 2013 303 304 305 `````` intros x Hx. rewrite elem_of_intersection_with in Hx. decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 306 ``````End collection_ops. `````` Robbert Krebbers committed Jan 05, 2013 307 `````` `````` Robbert Krebbers committed Aug 29, 2012 308 ``````(** * Sets without duplicates up to an equivalence *) `````` Robbert Krebbers committed May 07, 2013 309 ``````Section NoDup. `````` Robbert Krebbers committed Nov 12, 2012 310 `````` Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}. `````` Robbert Krebbers committed Jun 11, 2012 311 312 `````` Definition elem_of_upto (x : A) (X : B) := ∃ y, y ∈ X ∧ R x y. `````` Robbert Krebbers committed May 07, 2013 313 `````` Definition set_NoDup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y. `````` Robbert Krebbers committed Jun 11, 2012 314 315 `````` Global Instance: Proper ((≡) ==> iff) (elem_of_upto x). `````` Robbert Krebbers committed Jan 05, 2013 316 `````` Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed. `````` Robbert Krebbers committed Jun 11, 2012 317 318 319 `````` Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto. Proof. intros ?? E1 ?? E2. split; intros [z [??]]; exists z. `````` Robbert Krebbers committed Aug 21, 2012 320 321 `````` * rewrite <-E1, <-E2; intuition. * rewrite E1, E2; intuition. `````` Robbert Krebbers committed Jun 11, 2012 322 `````` Qed. `````` Robbert Krebbers committed May 07, 2013 323 `````` Global Instance: Proper ((≡) ==> iff) set_NoDup. `````` Robbert Krebbers committed Jun 11, 2012 324 325 326 `````` Proof. firstorder. Qed. Lemma elem_of_upto_elem_of x X : x ∈ X → elem_of_upto x X. `````` Robbert Krebbers committed Aug 29, 2012 327 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 328 `````` Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅. `````` Robbert Krebbers committed Aug 29, 2012 329 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Aug 21, 2012 330 `````` Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y. `````` Robbert Krebbers committed Aug 29, 2012 331 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 332 `````` `````` Robbert Krebbers committed Aug 21, 2012 333 334 `````` 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 335 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 336 `````` Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y. `````` Robbert Krebbers committed Aug 29, 2012 337 `````` Proof. unfold elem_of_upto. esolve_elem_of. Qed. `````` Robbert Krebbers committed Jun 11, 2012 338 `````` `````` Robbert Krebbers committed May 07, 2013 339 340 341 342 343 344 345 `````` 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 346 347 `````` Proof. intros Hin Hnodup [y [??]]. `````` Robbert Krebbers committed Aug 29, 2012 348 `````` rewrite (Hnodup x y) in Hin; solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 349 `````` Qed. `````` Robbert Krebbers committed May 07, 2013 350 351 352 353 354 `````` 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 355 `````` `````` Robbert Krebbers committed Aug 29, 2012 356 ``````(** * Quantifiers *) `````` Robbert Krebbers committed Jun 11, 2012 357 ``````Section quantifiers. `````` Robbert Krebbers committed Nov 12, 2012 358 `````` Context `{SimpleCollection A B} (P : A → Prop). `````` Robbert Krebbers committed Jun 11, 2012 359 `````` `````` Robbert Krebbers committed May 07, 2013 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 `````` 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 385 386 ``````End quantifiers. `````` Robbert Krebbers committed Aug 21, 2012 387 388 ``````Section more_quantifiers. Context `{Collection A B}. `````` Robbert Krebbers committed Aug 29, 2012 389 `````` `````` Robbert Krebbers committed May 07, 2013 390 391 392 393 394 395 `````` 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 396 397 ``````End more_quantifiers. `````` Robbert Krebbers committed Aug 29, 2012 398 399 400 ``````(** * 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 401 ``````Section fresh. `````` Robbert Krebbers committed Nov 12, 2012 402 `````` Context `{FreshSpec A C} . `````` Robbert Krebbers committed Aug 21, 2012 403 `````` `````` Robbert Krebbers committed Aug 29, 2012 404 405 406 407 `````` 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 408 `````` Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed. `````` Robbert Krebbers committed Aug 29, 2012 409 `````` `````` Robbert Krebbers committed Aug 21, 2012 410 411 412 413 414 415 `````` 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 416 417 `````` Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list. Proof. `````` Robbert Krebbers committed May 02, 2014 418 419 `````` 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 420 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 421 422 `````` 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 423 `````` Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X. `````` Robbert Krebbers committed Aug 21, 2012 424 `````` Proof. `````` Robbert Krebbers committed May 02, 2014 425 426 427 `````` 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 428 429 430 `````` Qed. Lemma fresh_list_nodup n X : NoDup (fresh_list n X). Proof. `````` Robbert Krebbers committed May 07, 2013 431 432 `````` 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 433 434 `````` Qed. End fresh. `````` Robbert Krebbers committed Nov 12, 2012 435 `````` `````` Robbert Krebbers committed Feb 19, 2013 436 ``````(** * Properties of implementations of collections that form a monad *) `````` Robbert Krebbers committed Nov 12, 2012 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 ``````Section collection_monad. Context `{CollectionMonad M}. 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 473 `````` Lemma collection_mapM_length {A B} (f : A → M B) l k : `````` Robbert Krebbers committed Nov 12, 2012 474 475 476 477 `````` 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 478 `````` Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l. `````` Robbert Krebbers committed Nov 12, 2012 479 `````` Proof. `````` Robbert Krebbers committed May 02, 2014 480 481 `````` intros Hl. revert k. induction Hl; simpl; intros; decompose_elem_of; f_equal'; auto. `````` Robbert Krebbers committed Nov 12, 2012 482 483 484 `````` Qed. Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k : `````` Robbert Krebbers committed May 07, 2013 485 `````` l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l. `````` Robbert Krebbers committed Jan 05, 2013 486 `````` Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed. `````` Robbert Krebbers committed May 07, 2013 487 488 `````` 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 489 490 491 492 493 `````` 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 494 ``End collection_monad.``