gmultiset.v 17.9 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import gmap.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6

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

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

13
Program Instance gmultiset_countable `{Countable A} :
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18 19 20 21 22 23
    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.
24
  Global Instance gmultiset_elem_of : ElemOf A (gmultiset A) := λ x X,
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    0 < multiplicity x X.
26
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
Robbert Krebbers's avatar
Robbert Krebbers committed
27
    multiplicity x X  multiplicity x Y.
28 29
  Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y,  x,
    multiplicity x X = multiplicity x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
30

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

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

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

57 58 59
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
60
Typeclasses Opaque gmultiset_dom.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62 63 64 65 66 67 68 69 70 71 72 73
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.
74 75
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
76
Global Instance gmultiset_equiv_equivalence : Equivalence (@{gmultiset A}).
77
Proof. constructor; repeat intro; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79 80 81 82 83 84 85 86

(* 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 :
87 88 89 90 91 92 93 94 95 96 97 98 99
  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
100 101
Proof.
  destruct X as [X], Y as [Y]; unfold multiplicity; simpl.
Ralf Jung's avatar
Ralf Jung committed
102
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108
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
109
  destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
110 111
Qed.

112
(* Set_ *)
113 114 115
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

116
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
117 118
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
119
  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
120 121 122 123
  - 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.
Ralf Jung's avatar
Ralf Jung committed
124
  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
125
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
127
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
128

129
(* Algebraic laws *)
130 131
(** For union *)
Global Instance gmultiset_union_comm : Comm (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof.
Ralf Jung's avatar
Ralf Jung committed
133
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Qed.
135
Global Instance gmultiset_union_assoc : Assoc (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
Ralf Jung's avatar
Ralf Jung committed
137
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Qed.
139
Global Instance gmultiset_union_left_id : LeftId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142 143
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_union, multiplicity_empty.
Qed.
144
Global Instance gmultiset_union_right_id : RightId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
146 147 148 149
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
150

151 152 153 154 155 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 182 183 184 185 186 187 188 189
(** 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.

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

Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ).
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
Proof.
  intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
192
  rewrite !multiplicity_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Qed.
194
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) ( X).
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.

197
(** Misc *)
198
Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201
  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
  by rewrite multiplicity_singleton, multiplicity_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
204 205 206 207 208 209 210 211
(* 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.
212 213 214
  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
215 216 217 218 219 220 221 222 223 224
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.
225 226
Lemma gmultiset_elements_disj_union X Y :
  elements (X  Y)  elements X ++ elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228 229 230
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.
231
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236 237
  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.
238 239
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242 243 244 245 246 247 248 249 250
  - 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
251
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
Robbert Krebbers's avatar
Robbert Krebbers committed
252
    exists (x,n); split; [|by apply elem_of_map_to_list].
Ralf Jung's avatar
Ralf Jung committed
253
    apply elem_of_replicate; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Qed.
255 256 257 258
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
259
  destruct (X !! x); naive_solver lia.
260
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295

(* 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.
296
Lemma gmultiset_size_disj_union X Y : size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
297 298
Proof.
  unfold size, gmultiset_size; simpl.
299
  by rewrite gmultiset_elements_disj_union, app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302

(* Order stuff *)
303
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
304 305 306 307 308 309 310
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.

311 312 313 314 315
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
316
  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
317
Qed.
318
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
319
Proof.
320
 refine (λ X Y, cast_if (decide (map_relation ()
321 322 323 324
   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
   by rewrite gmultiset_subseteq_alt.
Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
Tej Chajed's avatar
Tej Chajed committed
327
Hint Resolve gmultiset_subset_subseteq : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329

Lemma gmultiset_empty_subseteq X :   X.
Ralf Jung's avatar
Ralf Jung committed
330
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332

Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
Ralf Jung's avatar
Ralf Jung committed
333
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
335
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
337 338 339 340
Proof.
  intros HX HY x. rewrite !multiplicity_union.
  specialize (HX x); specialize (HY x); lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341 342 343 344
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
345

346 347 348 349 350 351 352 353 354 355 356
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
357
Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
358
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
359
Lemma gmultiset_disj_union_subset_l X Y : Y    X  X  Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
Proof.
  intros HY%gmultiset_size_non_empty_iff.
362 363
  apply gmultiset_subset; auto using gmultiset_disj_union_subseteq_l.
  rewrite gmultiset_size_disj_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Qed.
365 366
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
367

Robbert Krebbers's avatar
Robbert Krebbers committed
368
Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
370 371
  rewrite elem_of_multiplicity. split.
  - intros Hx y; destruct (decide (x = y)) as [->|].
Ralf Jung's avatar
Ralf Jung committed
372 373 374
    + rewrite multiplicity_singleton; lia.
    + rewrite multiplicity_singleton_ne by done; lia.
  - intros Hx. generalize (Hx x). rewrite multiplicity_singleton. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
375 376
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
377 378 379
Lemma gmultiset_elem_of_subseteq X1 X2 x : x  X1  X1  X2  x  X2.
Proof. rewrite !gmultiset_elem_of_singleton_subseteq. by intros ->. Qed.

380
Lemma gmultiset_disj_union_difference X Y : X  Y  Y = X  Y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
381 382
Proof.
  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
383
  rewrite multiplicity_disj_union, multiplicity_difference; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
384
Qed.
385
Lemma gmultiset_disj_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Proof.
387
  intros. by apply gmultiset_disj_union_difference,
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389
    gmultiset_elem_of_singleton_subseteq.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
390

Robbert Krebbers's avatar
Robbert Krebbers committed
391 392
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
393 394
  intros HX%gmultiset_disj_union_difference.
  rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
395 396
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
397 398 399 400
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
401
  rewrite multiplicity_difference, multiplicity_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403 404 405 406
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|].
407
  by rewrite <-(gmultiset_disj_union_difference X Y).
Robbert Krebbers's avatar
Robbert Krebbers committed
408 409
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
410
(* Mononicity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Proof.
413
  intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
  by apply submseteq_inserts_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
417
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
419 420 421 422

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
423
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
424 425
  rewrite (gmultiset_disj_union_difference X Y),
    gmultiset_size_disj_union by auto. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
426 427 428
Qed.

(* Well-foundedness *)
429
Lemma gmultiset_wf : wf (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
430 431 432
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
433 434

Lemma gmultiset_ind (P : gmultiset A  Prop) :
435
  P   ( x X, P X  P ({[ x ]}  X))   X, P X.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437 438
Proof.
  intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
  destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
439
  rewrite (gmultiset_disj_union_difference' x X) by done.
Robbert Krebbers's avatar
Robbert Krebbers committed
440 441
  apply Hinsert, IH, gmultiset_difference_subset,
    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
442
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
End lemmas.