gmultiset.v 14.4 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,
Robbert Krebbers's avatar
Robbert Krebbers committed
39 40
    let (X) := X in let (Y) := Y in
    GMultiSet $ union_with (λ x y, Some (S (x + y))) X Y.
41
  Global Instance gmultiset_difference : Difference (gmultiset A) := λ X Y,
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44
    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.
45

46
  Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
47
    let (X) := X in dom _ X.
48
End definitions. 
Robbert Krebbers's avatar
Robbert Krebbers committed
49

50 51 52
Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
53
Typeclasses Opaque gmultiset_dom.
54

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

(* 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.
Ralf Jung's avatar
Ralf Jung committed
83
  rewrite lookup_union_with. destruct (X !! _), (Y !! _); simpl; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86 87 88 89
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
90
  destruct (X !! _), (Y !! _); simplify_option_eq; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
Qed.

93
(* Set_ *)
94 95 96
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

97
Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
98 99
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
100
  - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
101 102 103 104
  - 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
105
  - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
106
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Global Instance gmultiset_elem_of_dec : RelDecision (@{gmultiset A}).
108
Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
109

110
(* Algebraic laws *)
111
Global Instance gmultiset_comm : Comm (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
Ralf Jung's avatar
Ralf Jung committed
113
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Qed.
115
Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) ().
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Proof.
Ralf Jung's avatar
Ralf Jung committed
117
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Qed.
119
Global Instance gmultiset_left_id : LeftId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123
Proof.
  intros X. apply gmultiset_eq; intros x.
  by rewrite multiplicity_union, multiplicity_empty.
Qed.
124
Global Instance gmultiset_right_id : RightId (=@{gmultiset A})  ().
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126 127 128 129
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).
Ralf Jung's avatar
Ralf Jung committed
130
  rewrite !multiplicity_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133 134
Qed.
Global Instance gmultiset_union_inj_2 X : Inj (=) (=) ( X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.

135
Lemma gmultiset_non_empty_singleton x : {[ x ]} @{gmultiset A} .
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
  rewrite gmultiset_eq. intros Hx; generalize (Hx x).
  by rewrite multiplicity_singleton, multiplicity_empty.
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144 145 146 147 148
(* 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.
149 150 151
  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
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
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.
168
  { by rewrite (left_id_L _ _ Y), map_to_list_empty. }
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171 172 173 174
  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.
175 176
    rewrite (assoc_L _). f_equiv.
    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180 181 182 183 184 185 186 187
  - 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
188
  - intros. destruct (X !! x) as [n|] eqn:Hx; [|lia].
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    exists (x,n); split; [|by apply elem_of_map_to_list].
Ralf Jung's avatar
Ralf Jung committed
190
    apply elem_of_replicate; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Qed.
192 193 194 195
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
196
  destruct (X !! x); naive_solver lia.
197
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211 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

(* 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's avatar
Robbert Krebbers committed
238 239

(* Order stuff *)
240
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
241 242 243 244 245 246 247
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.

248 249 250 251 252
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
253
  destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
254
Qed.
255
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
256
Proof.
257
 refine (λ X Y, cast_if (decide (map_relation ()
258 259 260 261
   (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
   by rewrite gmultiset_subseteq_alt.
Defined.

Robbert Krebbers's avatar
Robbert Krebbers committed
262 263
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
Tej Chajed's avatar
Tej Chajed committed
264
Hint Resolve gmultiset_subset_subseteq : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
265 266

Lemma gmultiset_empty_subseteq X :   X.
Ralf Jung's avatar
Ralf Jung committed
267
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269

Lemma gmultiset_union_subseteq_l X Y : X  X  Y.
Ralf Jung's avatar
Ralf Jung committed
270
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Lemma gmultiset_union_subseteq_r X Y : Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
272
Proof. intros x. rewrite multiplicity_union. lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
275 276 277 278
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
279 280

Lemma gmultiset_subset X Y : X  Y  size X < size Y  X  Y.
Ralf Jung's avatar
Ralf Jung committed
281
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284 285
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.
Ralf Jung's avatar
Ralf Jung committed
286
  rewrite gmultiset_size_union; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289 290
Qed.
Lemma gmultiset_union_subset_r X Y : X    Y  X  Y.
Proof. rewrite (comm_L ()). apply gmultiset_union_subset_l. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
291
Lemma gmultiset_elem_of_singleton_subseteq x X : x  X  {[ x ]}  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294
  rewrite elem_of_multiplicity. split.
  - intros Hx y; destruct (decide (x = y)) as [->|].
Ralf Jung's avatar
Ralf Jung committed
295 296 297
    + 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
298 299
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
300 301 302
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's avatar
Robbert Krebbers committed
303 304 305
Lemma gmultiset_union_difference X Y : X  Y  Y = X  Y  X.
Proof.
  intros HXY. apply gmultiset_eq; intros x; specialize (HXY x).
Ralf Jung's avatar
Ralf Jung committed
306
  rewrite multiplicity_union, multiplicity_difference; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308
Qed.
Lemma gmultiset_union_difference' x Y : x  Y  Y = {[ x ]}  Y  {[ x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310 311 312
Proof.
  intros. by apply gmultiset_union_difference,
    gmultiset_elem_of_singleton_subseteq.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313

Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316
Lemma gmultiset_size_difference X Y : Y  X  size (X  Y) = size X - size Y.
Proof.
  intros HX%gmultiset_union_difference.
Ralf Jung's avatar
Ralf Jung committed
317
  rewrite HX at 2; rewrite gmultiset_size_union. lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
320 321 322 323
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
324
  rewrite multiplicity_difference, multiplicity_empty; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326 327 328 329 330 331 332
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's avatar
Robbert Krebbers committed
333
(* Mononicity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336
Proof.
  intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  by apply submseteq_inserts_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
338 339
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
342 343 344 345

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
346
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348 349 350
  rewrite (gmultiset_union_difference X Y), gmultiset_size_union by auto. lia.
Qed.

(* Well-foundedness *)
351
Lemma gmultiset_wf : wf (@{gmultiset A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353 354
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
355 356 357 358 359 360 361

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's avatar
Robbert Krebbers committed
362 363
  apply Hinsert, IH, gmultiset_difference_subset,
    gmultiset_elem_of_singleton_subseteq; auto using gmultiset_non_empty_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
End lemmas.