gmultiset.v 21.5 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From stdpp Require Import gmap.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4

Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
5 6
Arguments GMultiSet {_ _ _} _ : assert.
Arguments gmultiset_car {_ _ _} _ : assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10
Proof. solve_decision. Defined.

11
Program Instance gmultiset_countable `{Countable A} :
Robbert Krebbers's avatar
Robbert Krebbers committed
12
    Countable (gmultiset A) := {|
13
  encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
22
  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    0 < multiplicity x X.
24
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    multiplicity x X  multiplicity x Y.
26 27
  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y,  x,
    multiplicity x X = multiplicity x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
28

29
  Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
30
    let (X) := X in ''(x,n)  map_to_list X; replicate (S n) x.
31
  Global Instance gmultiset_size : Size (gmultiset A) := length  elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

33 34
  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    GMultiSet {[ x := 0 ]}.
36
  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
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's avatar
Robbert Krebbers committed
44 45
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
46
  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
50

51
  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
52
    let (X) := X in dom _ X.
53
End definitions. 
Robbert Krebbers's avatar
Robbert Krebbers committed
54

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.
58
Typeclasses Opaque gmultiset_dom.
59

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
72 73
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
74
Global Instance gmultiset_equiv_equivalence : Equivalence (@{gmultiset A}).
75
Proof. constructor; repeat intro; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
91
Lemma multiplicity_union X Y x :
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's avatar
Robbert Krebbers committed
105 106
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
Ralf Jung's avatar
Ralf Jung committed
107
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
114
  destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
Qed.

117
(* Set_ *)
118 119 120
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

121
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
122 123
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
124
  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
125 126 127
  - intros x y.
    rewrite elem_of_multiplicity, multiplicity_singleton'.
    destruct (decide (x = y)); intuition lia.
Ralf Jung's avatar
Ralf Jung committed
128
  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
129
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
131
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
132

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.

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).
139
Proof.
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).
142 143
Qed.

144
(* Algebraic laws *)
145 146
(** For union *)
Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof.
Ralf Jung's avatar
Ralf Jung committed
148
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Qed.
150
Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
Ralf Jung's avatar
Ralf Jung committed
152
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Qed.
154
Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_union, multiplicity_empty.
Qed.
159
Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
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's avatar
Robbert Krebbers committed
165

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.

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.

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})  ().
217
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
218

219
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X .).
Robbert Krebbers's avatar
Robbert Krebbers committed
220 221
Proof.
  intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
222
  rewrite !multiplicity_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Qed.
224
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (. X).
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.

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.

245
(** Misc *)
246
Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
248 249
  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
  by rewrite multiplicity_singleton, multiplicity_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
Qed.

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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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.
295 296
Lemma gmultiset_elements_disj_union X Y :
  elements (X  Y)  elements X ++ elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
301
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
308 309
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
321
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
Robbert Krebbers's avatar
Robbert Krebbers committed
322
    exists (x,n); split; [|by apply elem_of_map_to_list].
Ralf Jung's avatar
Ralf Jung committed
323
    apply elem_of_replicate; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Qed.
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's avatar
Ralf Jung committed
329
  destruct (X !! x); naive_solver lia.
330
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331

Dan Frumin's avatar
Dan Frumin committed
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's avatar
Robbert Krebbers committed
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.
382
Lemma gmultiset_size_disj_union X Y : size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384
Proof.
  unfold size, gmultiset_size; simpl.
385
  by rewrite gmultiset_elements_disj_union, app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
387

Dan Frumin's avatar
Dan Frumin committed
388
(** Order stuff *)
389
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

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's avatar
Ralf Jung committed
402
  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
403
Qed.
404
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
405
Proof.
406
 refine (λ X Y, cast_if (decide (map_relation ()
407 408 409 410
   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
   by rewrite gmultiset_subseteq_alt.
Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
411 412
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
Tej Chajed's avatar
Tej Chajed committed
413
Hint Resolve gmultiset_subset_subseteq : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415

Lemma gmultiset_empty_subseteq X :   X.
Ralf Jung's avatar
Ralf Jung committed
416
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417 418

Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
Ralf Jung's avatar
Ralf Jung committed
419
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
421
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
422
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
423 424 425 426
Proof.
  intros HX HY x. rewrite !multiplicity_union.
  specialize (HX x); specialize (HY x); lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
431

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's avatar
Robbert Krebbers committed
443
Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
444
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
445
Lemma gmultiset_disj_union_subset_l X Y : Y    X  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447
Proof.
  intros HY%gmultiset_size_non_empty_iff.
448 449
  apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l.
  rewrite gmultiset_size_disj_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Qed.
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's avatar
Robbert Krebbers committed
453

Robbert Krebbers's avatar
Robbert Krebbers committed
454
Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
455
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
  rewrite elem_of_multiplicity. split.
457 458
  - intros Hx y. rewrite multiplicity_singleton'.
    destruct (decide (y = x)); naive_solver lia.
Ralf Jung's avatar
Ralf Jung committed
459
  - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
460 461
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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.

465
Lemma gmultiset_disj_union_difference X Y : X  Y  Y = X  Y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467
Proof.
  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
468
  rewrite multiplicity_disj_union, multiplicity_difference; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Qed.
470
Lemma gmultiset_disj_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
Proof.
472
  intros. by apply gmultiset_disj_union_difference,
Robbert Krebbers's avatar
Robbert Krebbers committed
473 474
    gmultiset_elem_of_singleton_subseteq.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
475

Robbert Krebbers's avatar
Robbert Krebbers committed
476 477
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
478 479
  intros HX%gmultiset_disj_union_difference.
  rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
480 481
Qed.

Dan Frumin's avatar
Dan Frumin committed
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's avatar
Robbert Krebbers committed
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's avatar
Ralf Jung committed
493
  rewrite multiplicity_difference, multiplicity_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
494 495
Qed.

Dan Frumin's avatar
Dan Frumin committed
496 497 498
Lemma gmultiset_difference_diag X : X  X = .
Proof. by apply gmultiset_empty_difference. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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|].
502
  by rewrite <-(gmultiset_disj_union_difference X Y).
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504
Qed.

Dan Frumin's avatar
Dan Frumin committed
505
(** Mononicity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
506
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
Proof.
508
  intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
  by apply submseteq_inserts_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
512
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
518
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
519 520
  rewrite (gmultiset_disj_union_difference X Y),
    gmultiset_size_disj_union by auto. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522
Qed.

Dan Frumin's avatar
Dan Frumin committed
523
(** Well-foundedness *)
524
Lemma gmultiset_wf : wf (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
525 526 527
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529

Lemma gmultiset_ind (P : gmultiset A  Prop) :
530
  P   ( x X, P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
534
  rewrite (gmultiset_disj_union_difference' x X) by done.
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536
  apply Hinsert, IH, gmultiset_difference_subset,
    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
End lemmas.