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

Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
7 8
Arguments GMultiSet {_ _ _} _ : assert.
Arguments gmultiset_car {_ _ _} _ : assert.
9

10
Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
11 12
Proof. solve_decision. Defined.

13
Program Instance gmultiset_countable `{Countable A} :
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,
25
    0 < multiplicity x X.
26
  Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y,  x,
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.
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.
34

35 36
  Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet .
  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
37
    GMultiSet {[ x := 0 ]}.
38
  Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
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,
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. 
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

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 70
Global Instance gmultiset_equivalence : Equivalence (@{gmultiset A}).
Proof. constructor; repeat intro; naive_solver. Qed.
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.
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.
91 92
Qed.

93
(* Collection *)
94 95 96 97 98 99
Lemma elem_of_multiplicity x X : x  X  0 < multiplicity x X.
Proof. done. Qed.

Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
Proof.
  split.
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}) ().
112
Proof.
Ralf Jung's avatar
Ralf Jung committed
113
  intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
114
Qed.
115
Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) ().
116
Proof.
Ralf Jung's avatar
Ralf Jung committed
117
  intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; lia.
118
Qed.
119
Global Instance gmultiset_left_id : LeftId (=@{gmultiset A})  ().
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})  ().
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.
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} .
136
Proof.
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.

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.
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. }
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.
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].
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.
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.
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.
238 239

(* Order stuff *)
240
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
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.

262 263
Lemma gmultiset_subset_subseteq X Y : X  Y  X  Y.
Proof. apply strict_include. Qed.
264
Hint Resolve gmultiset_subset_subseteq : core.
265 266

Lemma gmultiset_empty_subseteq X :   X.
Ralf Jung's avatar
Ralf Jung committed
267
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
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.
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.
273
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1  X2  Y1  Y2  X1  Y1  X2  Y2.
274
Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed.
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.
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.
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.
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.
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.
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.

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.
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.
313

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.
318 319
Qed.

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.
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.

333
(* Mononicity *)
334
Lemma gmultiset_elements_submseteq X Y : X  Y  elements X + elements Y.
335 336
Proof.
  intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union.
337
  by apply submseteq_inserts_r.
338 339
Qed.

340
Lemma gmultiset_subseteq_size X Y : X  Y  size X  size Y.
341
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
342 343 344 345

Lemma gmultiset_subset_size X Y : X  Y  size X < size Y.
Proof.
  intros HXY. assert (size (Y  X)  0).
346
  { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
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}).
352 353 354
Proof.
  apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
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.
364
Qed.
365
End lemmas.