gmultiset.v 15 KB
 Robbert Krebbers committed Nov 15, 2016 1 2 3 ``````(* Copyright (c) 2012-2016, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) From iris.prelude Require Import gmap. `````` Ralf Jung committed Jan 03, 2017 4 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Nov 15, 2016 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }. Arguments GMultiSet {_ _ _} _. Arguments gmultiset_car {_ _ _} _. Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A). Proof. solve_decision. Defined. Program Instance gmultiset_countable `{Countable A} : Countable (gmultiset A) := {| encode X := encode (gmultiset_car X); decode p := GMultiSet <\$> decode p |}. Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed. Section definitions. Context `{Countable A}. Definition multiplicity (x : A) (X : gmultiset A) : nat := match gmultiset_car X !! x with Some n => S n | None => 0 end. Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X, 0 < multiplicity x X. Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x, multiplicity x X ≤ multiplicity x Y. Instance gmultiset_elements : Elements A (gmultiset A) := λ X, let (X) := X in '(x,n) ← map_to_list X; replicate (S n) x. Instance gmultiset_size : Size (gmultiset A) := length ∘ elements. Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅. Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x, GMultiSet {[ x := 0 ]}. Instance gmultiset_union : Union (gmultiset A) := λ X Y, let (X) := X in let (Y) := Y in GMultiSet \$ union_with (λ x y, Some (S (x + y))) X Y. Instance gmultiset_difference : Difference (gmultiset A) := λ X Y, let (X) := X in let (Y) := Y in GMultiSet \$ difference_with (λ x y, let z := x - y in guard (0 < z); Some (pred z)) X Y. `````` Robbert Krebbers committed Nov 22, 2016 43 44 45 `````` Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, let (X) := X in dom _ X. `````` Robbert Krebbers committed Nov 15, 2016 46 47 ``````End definitions. `````` Robbert Krebbers committed Nov 21, 2016 48 49 50 ``````Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq. Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty. Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference. `````` Robbert Krebbers committed Nov 22, 2016 51 ``````Typeclasses Opaque gmultiset_dom. `````` Robbert Krebbers committed Nov 21, 2016 52 `````` `````` Robbert Krebbers committed Nov 15, 2016 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 ``````(** These instances are declared using [Hint Extern] to avoid too eager type class search. *) Hint Extern 1 (ElemOf _ (gmultiset _)) => eapply @gmultiset_elem_of : typeclass_instances. Hint Extern 1 (SubsetEq (gmultiset _)) => eapply @gmultiset_subseteq : typeclass_instances. Hint Extern 1 (Empty (gmultiset _)) => eapply @gmultiset_empty : typeclass_instances. Hint Extern 1 (Singleton _ (gmultiset _)) => eapply @gmultiset_singleton : typeclass_instances. Hint Extern 1 (Union (gmultiset _)) => eapply @gmultiset_union : typeclass_instances. Hint Extern 1 (Difference (gmultiset _)) => eapply @gmultiset_difference : typeclass_instances. Hint Extern 1 (Elements _ (gmultiset _)) => eapply @gmultiset_elements : typeclass_instances. Hint Extern 1 (Size (gmultiset _)) => eapply @gmultiset_size : typeclass_instances. `````` Robbert Krebbers committed Nov 22, 2016 71 72 ``````Hint Extern 1 (Dom (gmultiset _) _) => eapply @gmultiset_dom : typeclass_instances. `````` Robbert Krebbers committed Nov 15, 2016 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 `````` Section lemmas. Context `{Countable A}. Implicit Types x y : A. Implicit Types X Y : gmultiset A. Lemma gmultiset_eq X Y : X = Y ↔ ∀ x, multiplicity x X = multiplicity x Y. Proof. split; [by intros ->|intros HXY]. destruct X as [X], Y as [Y]; f_equal; apply map_eq; intros x. specialize (HXY x); unfold multiplicity in *; simpl in *. repeat case_match; naive_solver. Qed. (* Multiplicity *) Lemma multiplicity_empty x : multiplicity x ∅ = 0. Proof. done. Qed. Lemma multiplicity_singleton x : multiplicity x {[ x ]} = 1. Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed. Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[ y ]} = 0. Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed. Lemma multiplicity_union X Y x : multiplicity x (X ∪ Y) = multiplicity x X + multiplicity x Y. Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; omega. Qed. Lemma multiplicity_difference X Y x : multiplicity x (X ∖ Y) = multiplicity x X - multiplicity x Y. Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_difference_with. destruct (X !! _), (Y !! _); simplify_option_eq; omega. Qed. `````` Robbert Krebbers committed Nov 21, 2016 108 ``````(* Collection *) `````` Robbert Krebbers committed Nov 17, 2016 109 110 111 112 113 114 115 116 117 118 119 120 121 ``````Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X. Proof. done. Qed. Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A). Proof. split. - intros x. rewrite elem_of_multiplicity, multiplicity_empty. omega. - intros x y. destruct (decide (x = y)) as [->|]. + rewrite elem_of_multiplicity, multiplicity_singleton. split; auto with lia. + rewrite elem_of_multiplicity, multiplicity_singleton_ne by done. by split; auto with lia. - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega. Qed. `````` Robbert Krebbers committed Nov 21, 2016 122 123 ``````Global Instance gmultiset_elem_of_dec x X : Decision (x ∈ X). Proof. unfold elem_of, gmultiset_elem_of. apply _. Defined. `````` Robbert Krebbers committed Nov 17, 2016 124 `````` `````` Robbert Krebbers committed Nov 21, 2016 125 ``````(* Algebraic laws *) `````` Robbert Krebbers committed Nov 15, 2016 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 ``````Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) (∪). Proof. intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. Qed. Global Instance gmultiset_assoc : Assoc (@eq (gmultiset A)) (∪). Proof. intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. Qed. Global Instance gmultiset_left_id : LeftId (@eq (gmultiset A)) ∅ (∪). Proof. intros X. apply gmultiset_eq; intros x. by rewrite multiplicity_union, multiplicity_empty. Qed. Global Instance gmultiset_right_id : RightId (@eq (gmultiset A)) ∅ (∪). Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed. Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ∪). Proof. intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x). rewrite !multiplicity_union. omega. Qed. Global Instance gmultiset_union_inj_2 X : Inj (=) (=) (∪ X). Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed. `````` Robbert Krebbers committed Nov 19, 2016 150 ``````Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠ (∅ : gmultiset A). `````` Robbert Krebbers committed Nov 15, 2016 151 ``````Proof. `````` Robbert Krebbers committed Nov 19, 2016 152 153 `````` rewrite gmultiset_eq. intros Hx; generalize (Hx x). by rewrite multiplicity_singleton, multiplicity_empty. `````` Robbert Krebbers committed Nov 18, 2016 154 155 ``````Qed. `````` Robbert Krebbers committed Nov 15, 2016 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 ``````(* Properties of the elements operation *) Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = []. Proof. unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty. Qed. Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅. Proof. destruct X as [X]; unfold elements, gmultiset_elements; simpl. intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?; naive_solver eauto using map_to_list_empty_inv. Qed. Lemma gmultiset_elements_empty' X : elements X = [] ↔ X = ∅. Proof. split; intros HX; [by apply gmultiset_elements_empty_inv|]. by rewrite HX, gmultiset_elements_empty. Qed. Lemma gmultiset_elements_singleton x : elements ({[ x ]} : gmultiset A) = [ x ]. Proof. unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton. Qed. Lemma gmultiset_elements_union X Y : elements (X ∪ Y) ≡ₚ elements X ++ elements Y. Proof. destruct X as [X], Y as [Y]; unfold elements, gmultiset_elements. set (f xn := let '(x, n) := xn in replicate (S n) x); simpl. revert Y; induction X as [|x n X HX IH] using map_ind; intros Y. `````` Ralf Jung committed Dec 06, 2016 182 `````` { by rewrite (left_id_L _ _ Y), map_to_list_empty. } `````` Robbert Krebbers committed Nov 15, 2016 183 184 185 186 187 188 `````` destruct (Y !! x) as [n'|] eqn:HY. - rewrite <-(insert_id Y x n'), <-(insert_delete Y) by done. erewrite <-insert_union_with by done. rewrite !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX). rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH. `````` Robbert Krebbers committed Dec 05, 2016 189 190 `````` rewrite (assoc_L _). f_equiv. rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle. `````` Robbert Krebbers committed Nov 15, 2016 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 `````` - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?HX, ?HY). by rewrite <-(assoc_L (++)), <-IH. Qed. Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X. Proof. destruct X as [X]. unfold elements, gmultiset_elements. set (f xn := let '(x, n) := xn in replicate (S n) x); simpl. unfold elem_of at 2, gmultiset_elem_of, multiplicity; simpl. rewrite elem_of_list_bind. split. - intros [[??] [[<- ?]%elem_of_replicate ->%elem_of_map_to_list]]; lia. - intros. destruct (X !! x) as [n|] eqn:Hx; [|omega]. exists (x,n); split; [|by apply elem_of_map_to_list]. apply elem_of_replicate; auto with omega. Qed. `````` Robbert Krebbers committed Nov 22, 2016 206 207 208 209 210 211 ``````Lemma gmultiset_elem_of_dom x X : x ∈ dom (gset A) X ↔ x ∈ X. Proof. unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity. destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some. destruct (X !! x); naive_solver omega. Qed. `````` Robbert Krebbers committed Nov 15, 2016 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 `````` (* Properties of the size operation *) Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0. Proof. done. Qed. Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅. Proof. unfold size, gmultiset_size; simpl. rewrite length_zero_iff_nil. apply gmultiset_elements_empty_inv. Qed. Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅. Proof. split; [apply gmultiset_size_empty_inv|]. by intros ->; rewrite gmultiset_size_empty. Qed. Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅. Proof. by rewrite gmultiset_size_empty_iff. Qed. Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅. Proof. destruct (elements X) as [|x l] eqn:HX; [right|left]. - by apply gmultiset_elements_empty_inv. - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left. Qed. Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X. Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed. Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. Proof. intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|]. contradict Hsz. rewrite HX, gmultiset_size_empty; lia. Qed. Lemma gmultiset_size_singleton x : size ({[ x ]} : gmultiset A) = 1. Proof. unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton. Qed. Lemma gmultiset_size_union X Y : size (X ∪ Y) = size X + size Y. Proof. unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_union, app_length. Qed. `````` Robbert Krebbers committed Nov 19, 2016 252 253 254 255 256 257 258 259 260 261 `````` (* Order stuff *) Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _). Proof. split; [split|]. - by intros X x. - intros X Y Z HXY HYZ x. by trans (multiplicity x Y). - intros X Y HXY HYX; apply gmultiset_eq; intros x. by apply (anti_symm (≤)). Qed. `````` Robbert Krebbers committed Nov 21, 2016 262 263 264 265 266 267 268 269 270 271 272 273 274 275 ``````Lemma gmultiset_subseteq_alt X Y : X ⊆ Y ↔ map_relation (≤) (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y). Proof. apply forall_proper; intros x. unfold multiplicity. destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver omega. Qed. Global Instance gmultiset_subseteq_dec X Y : Decision (X ⊆ Y). Proof. refine (cast_if (decide (map_relation (≤) (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y)))); by rewrite gmultiset_subseteq_alt. Defined. `````` Robbert Krebbers committed Nov 19, 2016 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 ``````Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. apply strict_include. Qed. Hint Resolve gmultiset_subset_subseteq. Lemma gmultiset_empty_subseteq X : ∅ ⊆ X. Proof. intros x. rewrite multiplicity_empty. omega. Qed. Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. Lemma gmultiset_union_preserving X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2. Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed. Lemma gmultiset_union_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2. Proof. intros. by apply gmultiset_union_preserving. Qed. Lemma gmultiset_union_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. Proof. intros. by apply gmultiset_union_preserving. Qed. Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y. Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed. Lemma gmultiset_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ∪ Y. Proof. intros HY%gmultiset_size_non_empty_iff. apply gmultiset_subset; auto using gmultiset_union_subseteq_l. rewrite gmultiset_size_union; omega. Qed. Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ∪ Y. Proof. rewrite (comm_L (∪)). apply gmultiset_union_subset_l. Qed. `````` Robbert Krebbers committed Nov 24, 2016 305 ``````Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X. `````` Robbert Krebbers committed Nov 19, 2016 306 ``````Proof. `````` Robbert Krebbers committed Nov 24, 2016 307 308 309 310 311 `````` rewrite elem_of_multiplicity. split. - intros Hx y; destruct (decide (x = y)) as [->|]. + rewrite multiplicity_singleton; omega. + rewrite multiplicity_singleton_ne by done; omega. - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. omega. `````` Robbert Krebbers committed Nov 19, 2016 312 313 ``````Qed. `````` Robbert Krebbers committed Nov 24, 2016 314 315 316 ``````Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2. Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed. `````` Robbert Krebbers committed Nov 19, 2016 317 318 319 320 321 322 ``````Lemma gmultiset_union_difference X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. intros HXY. apply gmultiset_eq; intros x; specialize (HXY x). rewrite multiplicity_union, multiplicity_difference; omega. Qed. Lemma gmultiset_union_difference' x Y : x ∈ Y → Y = {[ x ]} ∪ Y ∖ {[ x ]}. `````` Robbert Krebbers committed Nov 24, 2016 323 324 325 326 ``````Proof. intros. by apply gmultiset_union_difference, gmultiset_elem_of_singleton_subseteq. Qed. `````` Robbert Krebbers committed Nov 19, 2016 327 `````` `````` Robbert Krebbers committed Nov 15, 2016 328 329 330 331 332 333 ``````Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y. Proof. intros HX%gmultiset_union_difference. rewrite HX at 2; rewrite gmultiset_size_union. omega. Qed. `````` Robbert Krebbers committed Nov 19, 2016 334 335 336 337 338 339 340 341 342 343 344 345 346 ``````Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅. Proof. intros [_ HXY2] Hdiff; destruct HXY2; intros x. generalize (f_equal (multiplicity x) Hdiff). rewrite multiplicity_difference, multiplicity_empty; omega. Qed. Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y. Proof. intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|]. by rewrite <-(gmultiset_union_difference X Y). Qed. `````` Robbert Krebbers committed Nov 15, 2016 347 ``````(* Mononicity *) `````` Robbert Krebbers committed Nov 19, 2016 348 349 350 351 352 353 ``````Lemma gmultiset_elements_contains X Y : X ⊆ Y → elements X `contains` elements Y. Proof. intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union. by apply contains_inserts_r. Qed. `````` Robbert Krebbers committed Nov 15, 2016 354 355 356 357 358 359 ``````Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y. Proof. intros. by apply contains_length, gmultiset_elements_contains. Qed. Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y. Proof. intros HXY. assert (size (Y ∖ X) ≠ 0). `````` Robbert Krebbers committed Nov 19, 2016 360 `````` { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. } `````` Robbert Krebbers committed Nov 15, 2016 361 362 363 364 365 366 367 368 `````` rewrite (gmultiset_union_difference X Y), gmultiset_size_union by auto. lia. Qed. (* Well-foundedness *) Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)). Proof. apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Nov 19, 2016 369 370 371 372 373 374 375 `````` Lemma gmultiset_ind (P : gmultiset A → Prop) : P ∅ → (∀ x X, P X → P ({[ x ]} ∪ X)) → ∀ X, P X. Proof. intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH]. destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto. rewrite (gmultiset_union_difference' x X) by done. `````` Robbert Krebbers committed Nov 24, 2016 376 377 `````` apply Hinsert, IH, gmultiset_difference_subset, gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton. `````` Robbert Krebbers committed Nov 19, 2016 378 ``````Qed. `````` Robbert Krebbers committed Nov 15, 2016 379 ``End lemmas.``