gmultiset.v 21.5 KB
 Robbert Krebbers committed Nov 15, 2016 1 ``````From stdpp Require Import gmap. `````` Ralf Jung committed Jan 31, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Nov 15, 2016 3 4 `````` Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }. `````` Robbert Krebbers committed Sep 08, 2017 5 6 ``````Arguments GMultiSet {_ _ _} _ : assert. Arguments gmultiset_car {_ _ _} _ : assert. `````` Robbert Krebbers committed Nov 15, 2016 7 `````` `````` 8 ``````Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A). `````` Robbert Krebbers committed Nov 15, 2016 9 10 ``````Proof. solve_decision. Defined. `````` 11 ``````Program Instance gmultiset_countable `{Countable A} : `````` Robbert Krebbers committed Nov 15, 2016 12 `````` Countable (gmultiset A) := {| `````` Robbert Krebbers committed Feb 23, 2019 13 `````` encode X := encode (gmultiset_car X); decode p := GMultiSet <\$> decode p `````` Robbert Krebbers committed Nov 15, 2016 14 15 16 17 18 19 20 21 ``````|}. 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. `````` Robbert Krebbers committed Sep 17, 2017 22 `````` Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X, `````` Robbert Krebbers committed Nov 15, 2016 23 `````` 0 < multiplicity x X. `````` Robbert Krebbers committed Sep 17, 2017 24 `````` Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, ∀ x, `````` Robbert Krebbers committed Nov 15, 2016 25 `````` multiplicity x X ≤ multiplicity x Y. `````` Robbert Krebbers committed Apr 09, 2018 26 27 `````` Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, ∀ x, multiplicity x X = multiplicity x Y. `````` Robbert Krebbers committed Nov 15, 2016 28 `````` `````` Robbert Krebbers committed Sep 17, 2017 29 `````` Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X, `````` Robbert Krebbers committed Nov 21, 2017 30 `````` let (X) := X in ''(x,n) ← map_to_list X; replicate (S n) x. `````` Robbert Krebbers committed Sep 17, 2017 31 `````` Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements. `````` Robbert Krebbers committed Nov 15, 2016 32 `````` `````` Robbert Krebbers committed Sep 17, 2017 33 34 `````` Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅. Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x, `````` Robbert Krebbers committed Nov 15, 2016 35 `````` GMultiSet {[ x := 0 ]}. `````` Robbert Krebbers committed Sep 17, 2017 36 `````` Global Instance gmultiset_union : Union (gmultiset A) := λ X Y, `````` Robbert Krebbers committed Feb 21, 2019 37 38 39 40 41 42 43 `````` let (X) := X in let (Y) := Y in GMultiSet \$ union_with (λ x y, Some (x `max` y)) X Y. Global Instance gmultiset_intersection : Intersection (gmultiset A) := λ X Y, let (X) := X in let (Y) := Y in GMultiSet \$ intersection_with (λ x y, Some (x `min` y)) X Y. (** Often called the "sum" *) Global Instance gmultiset_disj_union : DisjUnion (gmultiset A) := λ X Y, `````` Robbert Krebbers committed Nov 15, 2016 44 45 `````` let (X) := X in let (Y) := Y in GMultiSet \$ union_with (λ x y, Some (S (x + y))) X Y. `````` Robbert Krebbers committed Sep 17, 2017 46 `````` Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y, `````` Robbert Krebbers committed Nov 15, 2016 47 48 49 `````` 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 50 `````` `````` Robbert Krebbers committed Sep 17, 2017 51 `````` Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X, `````` Robbert Krebbers committed Nov 22, 2016 52 `````` let (X) := X in dom _ X. `````` Michael Sammler committed Mar 31, 2020 53 ``````End definitions. `````` Robbert Krebbers committed Nov 15, 2016 54 `````` `````` Robbert Krebbers committed Nov 21, 2016 55 56 57 ``````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 58 ``````Typeclasses Opaque gmultiset_dom. `````` Robbert Krebbers committed Nov 21, 2016 59 `````` `````` Robbert Krebbers committed Nov 15, 2016 60 61 62 63 64 65 66 67 68 69 70 71 ``````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. `````` Robbert Krebbers committed Apr 09, 2018 72 73 ``````Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A). Proof. intros X Y. by rewrite gmultiset_eq. Qed. `````` Robbert Krebbers committed Feb 20, 2019 74 ``````Global Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}). `````` Robbert Krebbers committed Apr 11, 2018 75 ``````Proof. constructor; repeat intro; naive_solver. Qed. `````` Robbert Krebbers committed Nov 15, 2016 76 77 78 79 80 81 82 83 `````` (* 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. `````` Robbert Krebbers committed Feb 23, 2019 84 85 86 87 88 89 90 ``````Lemma multiplicity_singleton' x y : multiplicity x {[ y ]} = if decide (x = y) then 1 else 0. Proof. destruct (decide _) as [->|]. - by rewrite multiplicity_singleton. - by rewrite multiplicity_singleton_ne. Qed. `````` Robbert Krebbers committed Nov 15, 2016 91 ``````Lemma multiplicity_union X Y x : `````` Robbert Krebbers committed Feb 21, 2019 92 93 94 95 96 97 98 99 100 101 102 103 104 `````` multiplicity x (X ∪ Y) = multiplicity x X `max` multiplicity x Y. Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia. Qed. Lemma multiplicity_intersection X Y x : multiplicity x (X ∩ Y) = multiplicity x X `min` multiplicity x Y. Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. rewrite lookup_intersection_with. destruct (X !! _), (Y !! _); simpl; lia. Qed. Lemma multiplicity_disj_union X Y x : multiplicity x (X ⊎ Y) = multiplicity x X + multiplicity x Y. `````` Robbert Krebbers committed Nov 15, 2016 105 106 ``````Proof. destruct X as [X], Y as [Y]; unfold multiplicity; simpl. `````` Ralf Jung committed Jun 20, 2018 107 `````` rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia. `````` Robbert Krebbers committed Nov 15, 2016 108 109 110 111 112 113 ``````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. `````` Ralf Jung committed Jun 20, 2018 114 `````` destruct (X !! _), (Y !! _); simplify_option_eq; lia. `````` Robbert Krebbers committed Nov 15, 2016 115 116 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 117 ``````(* Set_ *) `````` Robbert Krebbers committed Nov 17, 2016 118 119 120 ``````Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X. Proof. done. Qed. `````` Robbert Krebbers committed Feb 20, 2019 121 ``````Global Instance gmultiset_simple_set : SemiSet A (gmultiset A). `````` Robbert Krebbers committed Nov 17, 2016 122 123 ``````Proof. split. `````` Ralf Jung committed Jun 20, 2018 124 `````` - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia. `````` Robbert Krebbers committed Feb 23, 2019 125 126 127 `````` - intros x y. rewrite elem_of_multiplicity, multiplicity_singleton'. destruct (decide (x = y)); intuition lia. `````` Ralf Jung committed Jun 20, 2018 128 `````` - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia. `````` Robbert Krebbers committed Nov 17, 2016 129 ``````Qed. `````` Robbert Krebbers committed Apr 05, 2018 130 ``````Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}). `````` 131 ``````Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined. `````` Robbert Krebbers committed Nov 17, 2016 132 `````` `````` Robbert Krebbers committed Feb 21, 2019 133 134 135 ``````Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y. Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed. `````` Robbert Krebbers committed Feb 21, 2019 136 ``````Global Instance set_unfold_gmultiset_disj_union x X Y P Q : `````` 137 138 `````` SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q → SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q). `````` Robbert Krebbers committed Feb 21, 2019 139 ``````Proof. `````` Robbert Krebbers committed Feb 21, 2019 140 `````` intros ??; constructor. rewrite gmultiset_elem_of_disj_union. `````` 141 `````` by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q). `````` Robbert Krebbers committed Feb 21, 2019 142 143 ``````Qed. `````` Robbert Krebbers committed Nov 21, 2016 144 ``````(* Algebraic laws *) `````` Robbert Krebbers committed Feb 21, 2019 145 146 ``````(** For union *) Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) (∪). `````` Robbert Krebbers committed Nov 15, 2016 147 ``````Proof. `````` Ralf Jung committed Jun 20, 2018 148 `````` intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia. `````` Robbert Krebbers committed Nov 15, 2016 149 ``````Qed. `````` Robbert Krebbers committed Feb 21, 2019 150 ``````Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) (∪). `````` Robbert Krebbers committed Nov 15, 2016 151 ``````Proof. `````` Ralf Jung committed Jun 20, 2018 152 `````` intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia. `````` Robbert Krebbers committed Nov 15, 2016 153 ``````Qed. `````` Robbert Krebbers committed Feb 21, 2019 154 ``````Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A}) ∅ (∪). `````` Robbert Krebbers committed Nov 15, 2016 155 156 157 158 ``````Proof. intros X. apply gmultiset_eq; intros x. by rewrite multiplicity_union, multiplicity_empty. Qed. `````` Robbert Krebbers committed Feb 21, 2019 159 ``````Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A}) ∅ (∪). `````` Robbert Krebbers committed Nov 15, 2016 160 ``````Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed. `````` Robbert Krebbers committed Feb 21, 2019 161 162 163 164 ``````Global Instance gmultiset_union_idemp : IdemP (=@{gmultiset A}) (∪). Proof. intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia. Qed. `````` Robbert Krebbers committed Nov 15, 2016 165 `````` `````` Robbert Krebbers committed Feb 21, 2019 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 ``````(** For intersection *) Global Instance gmultiset_intersection_comm : Comm (=@{gmultiset A}) (∩). Proof. intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia. Qed. Global Instance gmultiset_intersection_assoc : Assoc (=@{gmultiset A}) (∩). Proof. intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia. Qed. Global Instance gmultiset_intersection_left_absorb : LeftAbsorb (=@{gmultiset A}) ∅ (∩). Proof. intros X. apply gmultiset_eq; intros x. by rewrite multiplicity_intersection, multiplicity_empty. Qed. Global Instance gmultiset_intersection_right_absorb : RightAbsorb (=@{gmultiset A}) ∅ (∩). Proof. intros X. by rewrite (comm_L (∩)), (left_absorb_L _ _). Qed. Global Instance gmultiset_intersection_idemp : IdemP (=@{gmultiset A}) (∩). Proof. intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia. Qed. `````` Robbert Krebbers committed Feb 21, 2019 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 ``````Lemma gmultiset_union_intersection_l X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z). Proof. apply gmultiset_eq; intros y. rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia. Qed. Lemma gmultiset_union_intersection_r X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z). Proof. by rewrite <-!(comm_L _ Z), gmultiset_union_intersection_l. Qed. Lemma gmultiset_intersection_union_l X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z). Proof. apply gmultiset_eq; intros y. rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia. Qed. Lemma gmultiset_intersection_union_r X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z). Proof. by rewrite <-!(comm_L _ Z), gmultiset_intersection_union_l. Qed. `````` Robbert Krebbers committed Feb 21, 2019 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 ``````(** For disjoint union (aka sum) *) Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) (⊎). Proof. intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia. Qed. Global Instance gmultiset_disj_union_assoc : Assoc (=@{gmultiset A}) (⊎). Proof. intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_disj_union; lia. Qed. Global Instance gmultiset_disj_union_left_id : LeftId (=@{gmultiset A}) ∅ (⊎). Proof. intros X. apply gmultiset_eq; intros x. by rewrite multiplicity_disj_union, multiplicity_empty. Qed. Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎). `````` Robbert Krebbers committed Mar 15, 2019 217 ``````Proof. intros X. by rewrite (comm_L (⊎)), (left_id_L _ _). Qed. `````` Robbert Krebbers committed Feb 21, 2019 218 `````` `````` Robbert Krebbers committed Sep 19, 2019 219 ``````Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.). `````` Robbert Krebbers committed Nov 15, 2016 220 221 ``````Proof. intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x). `````` Robbert Krebbers committed Feb 21, 2019 222 `````` rewrite !multiplicity_disj_union. lia. `````` Robbert Krebbers committed Nov 15, 2016 223 ``````Qed. `````` Robbert Krebbers committed Sep 19, 2019 224 ``````Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X). `````` Paolo G. Giarrusso committed Apr 05, 2020 225 ``````Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X ⊎.)). Qed. `````` Robbert Krebbers committed Nov 15, 2016 226 `````` `````` Robbert Krebbers committed Feb 21, 2019 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 ``````Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z). Proof. apply gmultiset_eq; intros y. rewrite multiplicity_disj_union, !multiplicity_intersection, !multiplicity_disj_union. lia. Qed. Lemma gmultiset_disj_union_intersection_r X Y Z : (X ∩ Y) ⊎ Z = (X ⊎ Z) ∩ (Y ⊎ Z). Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_intersection_l. Qed. Lemma gmultiset_disj_union_union_l X Y Z : X ⊎ (Y ∪ Z) = (X ⊎ Y) ∪ (X ⊎ Z). Proof. apply gmultiset_eq; intros y. rewrite multiplicity_disj_union, !multiplicity_union, !multiplicity_disj_union. lia. Qed. Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z). Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_union_l. Qed. `````` Robbert Krebbers committed Feb 21, 2019 245 ``````(** Misc *) `````` 246 ``````Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅. `````` Robbert Krebbers committed Nov 15, 2016 247 ``````Proof. `````` Robbert Krebbers committed Nov 19, 2016 248 249 `````` rewrite gmultiset_eq. intros Hx; generalize (Hx x). by rewrite multiplicity_singleton, multiplicity_empty. `````` Robbert Krebbers committed Nov 18, 2016 250 251 ``````Qed. `````` Robbert Krebbers committed Feb 23, 2019 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 ``````(** Conversion from lists *) Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} ∅. Proof. done. Qed. Lemma list_to_set_disj_cons x l : list_to_set_disj (x :: l) =@{gmultiset A} {[ x ]} ⊎ list_to_set_disj l. Proof. done. Qed. Lemma list_to_set_disj_app l1 l2 : list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2. Proof. induction l1 as [|x l1 IH]; simpl. - by rewrite (left_id_L _ _). - by rewrite IH, (assoc_L _). Qed. Global Instance list_to_set_disj_perm : Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)). Proof. induction 1 as [|x l l' _ IH|x y l|l l' l'' _ IH1 _ IH2]; simpl; auto. - by rewrite IH. - by rewrite !(assoc_L _), (comm_L _ {[ x ]}). - by rewrite IH1. Qed. (** Properties of the elements operation *) `````` Robbert Krebbers committed Nov 15, 2016 275 276 277 278 279 280 281 ``````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. `````` 282 283 284 `````` intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?. - by apply map_to_list_empty_inv. - naive_solver. `````` Robbert Krebbers committed Nov 15, 2016 285 286 287 288 289 290 291 292 293 294 ``````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. `````` Robbert Krebbers committed Feb 21, 2019 295 296 ``````Lemma gmultiset_elements_disj_union X Y : elements (X ⊎ Y) ≡ₚ elements X ++ elements Y. `````` Robbert Krebbers committed Nov 15, 2016 297 298 299 300 ``````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 301 `````` { by rewrite (left_id_L _ _ Y), map_to_list_empty. } `````` Robbert Krebbers committed Nov 15, 2016 302 303 304 305 306 307 `````` 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 308 309 `````` rewrite (assoc_L _). f_equiv. rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle. `````` Robbert Krebbers committed Nov 15, 2016 310 311 312 313 314 315 316 317 318 319 320 `````` - 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. `````` Ralf Jung committed Jun 20, 2018 321 `````` - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia]. `````` Robbert Krebbers committed Nov 15, 2016 322 `````` exists (x,n); split; [|by apply elem_of_map_to_list]. `````` Ralf Jung committed Jun 20, 2018 323 `````` apply elem_of_replicate; auto with lia. `````` Robbert Krebbers committed Nov 15, 2016 324 ``````Qed. `````` Robbert Krebbers committed Nov 22, 2016 325 326 327 328 ``````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. `````` Ralf Jung committed Jun 20, 2018 329 `````` destruct (X !! x); naive_solver lia. `````` Robbert Krebbers committed Nov 22, 2016 330 ``````Qed. `````` Robbert Krebbers committed Nov 15, 2016 331 `````` `````` Dan Frumin committed Apr 19, 2019 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 ``````(** Properties of the set_fold operation *) Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) : set_fold f b (∅ : gmultiset A) = b. Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed. Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) : set_fold f b ({[a]} : gmultiset A) = f a b. Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed. Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y : Comm (=) f → Assoc (=) f → set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y. Proof. intros Hcomm Hassoc. unfold set_fold; simpl. by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)). Qed. (** Properties of the size operation *) `````` Robbert Krebbers committed Nov 15, 2016 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 ``````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. `````` Robbert Krebbers committed Feb 21, 2019 382 ``````Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y. `````` Robbert Krebbers committed Nov 15, 2016 383 384 ``````Proof. unfold size, gmultiset_size; simpl. `````` Robbert Krebbers committed Feb 21, 2019 385 `````` by rewrite gmultiset_elements_disj_union, app_length. `````` Robbert Krebbers committed Nov 15, 2016 386 ``````Qed. `````` Robbert Krebbers committed Nov 19, 2016 387 `````` `````` Dan Frumin committed Apr 19, 2019 388 ``````(** Order stuff *) `````` Robbert Krebbers committed Apr 05, 2018 389 ``````Global Instance gmultiset_po : PartialOrder (⊆@{gmultiset A}). `````` Robbert Krebbers committed Nov 19, 2016 390 391 392 393 394 395 396 ``````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 397 398 399 400 401 ``````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. `````` Ralf Jung committed Jun 20, 2018 402 `````` destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia. `````` Robbert Krebbers committed Nov 21, 2016 403 ``````Qed. `````` Robbert Krebbers committed Apr 05, 2018 404 ``````Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}). `````` Robbert Krebbers committed Nov 21, 2016 405 ``````Proof. `````` 406 `````` refine (λ X Y, cast_if (decide (map_relation (≤) `````` Robbert Krebbers committed Nov 21, 2016 407 408 409 410 `````` (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y)))); by rewrite gmultiset_subseteq_alt. Defined. `````` Robbert Krebbers committed Nov 19, 2016 411 412 ``````Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. apply strict_include. Qed. `````` Tej Chajed committed Nov 28, 2018 413 ``````Hint Resolve gmultiset_subset_subseteq : core. `````` Robbert Krebbers committed Nov 19, 2016 414 415 `````` Lemma gmultiset_empty_subseteq X : ∅ ⊆ X. `````` Ralf Jung committed Jun 20, 2018 416 ``````Proof. intros x. rewrite multiplicity_empty. lia. Qed. `````` Robbert Krebbers committed Nov 19, 2016 417 418 `````` Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y. `````` Ralf Jung committed Jun 20, 2018 419 ``````Proof. intros x. rewrite multiplicity_union. lia. Qed. `````` Robbert Krebbers committed Nov 19, 2016 420 ``````Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y. `````` Ralf Jung committed Jun 20, 2018 421 ``````Proof. intros x. rewrite multiplicity_union. lia. Qed. `````` Robbert Krebbers committed Mar 09, 2017 422 ``````Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2. `````` Robbert Krebbers committed Feb 21, 2019 423 424 425 426 ``````Proof. intros HX HY x. rewrite !multiplicity_union. specialize (HX x); specialize (HY x); lia. Qed. `````` Robbert Krebbers committed Mar 09, 2017 427 428 429 430 ``````Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2. Proof. intros. by apply gmultiset_union_mono. Qed. Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. Proof. intros. by apply gmultiset_union_mono. Qed. `````` Robbert Krebbers committed Nov 19, 2016 431 `````` `````` Robbert Krebbers committed Feb 21, 2019 432 433 434 435 436 437 438 439 440 441 442 ``````Lemma gmultiset_disj_union_subseteq_l X Y : X ⊆ X ⊎ Y. Proof. intros x. rewrite multiplicity_disj_union. lia. Qed. Lemma gmultiset_disj_union_subseteq_r X Y : Y ⊆ X ⊎ Y. Proof. intros x. rewrite multiplicity_disj_union. lia. Qed. Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ⊎ Y1 ⊆ X2 ⊎ Y2. Proof. intros ?? x. rewrite !multiplicity_disj_union. by apply Nat.add_le_mono. Qed. Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ⊎ Y1 ⊆ X ⊎ Y2. Proof. intros. by apply gmultiset_disj_union_mono. Qed. Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ⊎ Y ⊆ X2 ⊎ Y. Proof. intros. by apply gmultiset_disj_union_mono. Qed. `````` Robbert Krebbers committed Nov 19, 2016 443 ``````Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y. `````` Ralf Jung committed Jun 20, 2018 444 ``````Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed. `````` Robbert Krebbers committed Feb 21, 2019 445 ``````Lemma gmultiset_disj_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ⊎ Y. `````` Robbert Krebbers committed Nov 19, 2016 446 447 ``````Proof. intros HY%gmultiset_size_non_empty_iff. `````` Robbert Krebbers committed Feb 21, 2019 448 449 `````` apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l. rewrite gmultiset_size_disj_union; lia. `````` Robbert Krebbers committed Nov 19, 2016 450 ``````Qed. `````` Robbert Krebbers committed Feb 21, 2019 451 452 ``````Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y. Proof. rewrite (comm_L (⊎)). apply gmultiset_disj_union_subset_l. Qed. `````` Robbert Krebbers committed Nov 19, 2016 453 `````` `````` Robbert Krebbers committed Nov 24, 2016 454 ``````Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X. `````` Robbert Krebbers committed Nov 19, 2016 455 ``````Proof. `````` Robbert Krebbers committed Nov 24, 2016 456 `````` rewrite elem_of_multiplicity. split. `````` Robbert Krebbers committed Feb 23, 2019 457 458 `````` - intros Hx y. rewrite multiplicity_singleton'. destruct (decide (y = x)); naive_solver lia. `````` Ralf Jung committed Jun 20, 2018 459 `````` - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia. `````` Robbert Krebbers committed Nov 19, 2016 460 461 ``````Qed. `````` Robbert Krebbers committed Nov 24, 2016 462 463 464 ``````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 Feb 21, 2019 465 ``````Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X. `````` Robbert Krebbers committed Nov 19, 2016 466 467 ``````Proof. intros HXY. apply gmultiset_eq; intros x; specialize (HXY x). `````` Robbert Krebbers committed Feb 21, 2019 468 `````` rewrite multiplicity_disj_union, multiplicity_difference; lia. `````` Robbert Krebbers committed Nov 19, 2016 469 ``````Qed. `````` Robbert Krebbers committed Feb 21, 2019 470 ``````Lemma gmultiset_disj_union_difference' x Y : x ∈ Y → Y = {[ x ]} ⊎ Y ∖ {[ x ]}. `````` Robbert Krebbers committed Nov 24, 2016 471 ``````Proof. `````` Robbert Krebbers committed Feb 21, 2019 472 `````` intros. by apply gmultiset_disj_union_difference, `````` Robbert Krebbers committed Nov 24, 2016 473 474 `````` gmultiset_elem_of_singleton_subseteq. Qed. `````` Robbert Krebbers committed Nov 19, 2016 475 `````` `````` Robbert Krebbers committed Nov 15, 2016 476 477 ``````Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y. Proof. `````` Robbert Krebbers committed Feb 21, 2019 478 479 `````` intros HX%gmultiset_disj_union_difference. rewrite HX at 2; rewrite gmultiset_size_disj_union. lia. `````` Robbert Krebbers committed Nov 15, 2016 480 481 ``````Qed. `````` Dan Frumin committed Apr 19, 2019 482 483 484 485 486 487 488 ``````Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅. Proof. intros HYX. unfold_leibniz. intros x. rewrite multiplicity_difference, multiplicity_empty. specialize (HYX x). lia. Qed. `````` Robbert Krebbers committed Nov 19, 2016 489 490 491 492 ``````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). `````` Ralf Jung committed Jun 20, 2018 493 `````` rewrite multiplicity_difference, multiplicity_empty; lia. `````` Robbert Krebbers committed Nov 19, 2016 494 495 ``````Qed. `````` Dan Frumin committed Apr 19, 2019 496 497 498 ``````Lemma gmultiset_difference_diag X : X ∖ X = ∅. Proof. by apply gmultiset_empty_difference. Qed. `````` Robbert Krebbers committed Nov 19, 2016 499 500 501 ``````Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y. Proof. intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|]. `````` Robbert Krebbers committed Feb 21, 2019 502 `````` by rewrite <-(gmultiset_disj_union_difference X Y). `````` Robbert Krebbers committed Nov 19, 2016 503 504 ``````Qed. `````` Dan Frumin committed Apr 19, 2019 505 ``````(** Mononicity *) `````` Robbert Krebbers committed Jan 31, 2017 506 ``````Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. `````` Robbert Krebbers committed Nov 19, 2016 507 ``````Proof. `````` Robbert Krebbers committed Feb 21, 2019 508 `````` intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union. `````` Robbert Krebbers committed Jan 31, 2017 509 `````` by apply submseteq_inserts_r. `````` Robbert Krebbers committed Nov 19, 2016 510 511 ``````Qed. `````` Robbert Krebbers committed Nov 15, 2016 512 ``````Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed Jan 31, 2017 513 ``````Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed. `````` Robbert Krebbers committed Nov 15, 2016 514 515 516 517 `````` 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 518 `````` { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. } `````` Robbert Krebbers committed Feb 21, 2019 519 520 `````` rewrite (gmultiset_disj_union_difference X Y), gmultiset_size_disj_union by auto. lia. `````` Robbert Krebbers committed Nov 15, 2016 521 522 ``````Qed. `````` Dan Frumin committed Apr 19, 2019 523 ``````(** Well-foundedness *) `````` Robbert Krebbers committed Apr 05, 2018 524 ``````Lemma gmultiset_wf : wf (⊂@{gmultiset A}). `````` Robbert Krebbers committed Nov 15, 2016 525 526 527 ``````Proof. apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Nov 19, 2016 528 529 `````` Lemma gmultiset_ind (P : gmultiset A → Prop) : `````` Robbert Krebbers committed Feb 21, 2019 530 `````` P ∅ → (∀ x X, P X → P ({[ x ]} ⊎ X)) → ∀ X, P X. `````` Robbert Krebbers committed Nov 19, 2016 531 532 533 ``````Proof. intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH]. destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto. `````` Robbert Krebbers committed Feb 21, 2019 534 `````` rewrite (gmultiset_disj_union_difference' x X) by done. `````` Robbert Krebbers committed Nov 24, 2016 535 536 `````` apply Hinsert, IH, gmultiset_difference_subset, gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton. `````` Robbert Krebbers committed Nov 19, 2016 537 ``````Qed. `````` Robbert Krebbers committed Nov 15, 2016 538 ``End lemmas.``