gmultiset.v 3.28 KB
Newer Older
1
From stdpp Require Export sets gmultiset countable.
Dan Frumin's avatar
Dan Frumin committed
2 3 4 5 6 7 8 9 10
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
Set Default Proof Using "Type".

(* The multiset union CMRA *)
Section gmultiset.
  Context `{Countable K}.
  Implicit Types X Y : gmultiset K.

11
  Canonical Structure gmultisetO := discreteO (gmultiset K).
Dan Frumin's avatar
Dan Frumin committed
12 13 14 15

  Instance gmultiset_valid : Valid (gmultiset K) := λ _, True.
  Instance gmultiset_validN : ValidN (gmultiset K) := λ _ _, True.
  Instance gmultiset_unit : Unit (gmultiset K) := ( : gmultiset K).
16
  Instance gmultiset_op : Op (gmultiset K) := disj_union.
Dan Frumin's avatar
Dan Frumin committed
17 18
  Instance gmultiset_pcore : PCore (gmultiset K) := λ X, Some .

19
  Lemma gmultiset_op_disj_union X Y : X  Y = X  Y.
Dan Frumin's avatar
Dan Frumin committed
20 21 22 23 24 25 26
  Proof. done. Qed.
  Lemma gmultiset_core_empty X : core X = .
  Proof. done. Qed.
  Lemma gmultiset_included X Y : X  Y  X  Y.
  Proof.
    split.
    - intros [Z ->%leibniz_equiv].
27 28
      rewrite gmultiset_op_disj_union. apply gmultiset_disj_union_subseteq_l.
    - intros ->%gmultiset_disj_union_difference. by exists (Y  X).
Dan Frumin's avatar
Dan Frumin committed
29 30 31 32 33 34 35 36
  Qed.

  Lemma gmultiset_ra_mixin : RAMixin (gmultiset K).
  Proof.
    apply ra_total_mixin; eauto.
    - by intros X Y Z ->%leibniz_equiv.
    - by intros X Y ->%leibniz_equiv.
    - solve_proper.
37 38
    - intros X1 X2 X3. by rewrite !gmultiset_op_disj_union assoc_L.
    - intros X1 X2. by rewrite !gmultiset_op_disj_union comm_L.
Dan Frumin's avatar
Dan Frumin committed
39 40 41 42 43 44 45 46 47 48 49
    - intros X. by rewrite gmultiset_core_empty left_id.
    - intros X1 X2 HX. rewrite !gmultiset_core_empty. exists .
      by rewrite left_id.
  Qed.

  Canonical Structure gmultisetR := discreteR (gmultiset K) gmultiset_ra_mixin.

  Global Instance gmultiset_cmra_discrete : CmraDiscrete gmultisetR.
  Proof. apply discrete_cmra_discrete. Qed.

  Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
50
  Proof. split. done. intros X. by rewrite gmultiset_op_disj_union left_id_L. done. Qed.
Dan Frumin's avatar
Dan Frumin committed
51 52
  Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.

53 54
  Global Instance gmultiset_cancelable X : Cancelable X.
  Proof.
55
    apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
56 57
  Qed.

58
  Lemma gmultiset_opM X mY : X ? mY = X  default  mY.
Dan Frumin's avatar
Dan Frumin committed
59 60 61 62 63
  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.

  Lemma gmultiset_update X Y : X ~~> Y.
  Proof. done. Qed.

64
  Lemma gmultiset_local_update X Y X' Y' : X  Y' = X'  Y  (X,Y) ~l~> (X', Y').
Dan Frumin's avatar
Dan Frumin committed
65
  Proof.
66 67 68 69
    intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
    split; first done. apply leibniz_equiv_iff, (inj ( Y)).
    rewrite -HXY !gmultiset_op_disj_union.
    by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
Dan Frumin's avatar
Dan Frumin committed
70 71
  Qed.

72 73 74
  Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X  X', Y  X').
  Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.

75
  Lemma gmultiset_local_update_dealloc X Y X' :
76
    X'  Y  (X,Y) ~l~> (X  X', Y  X').
Dan Frumin's avatar
Dan Frumin committed
77
  Proof.
78 79
    intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
    intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
80
    apply gmultiset_local_update. apply gmultiset_eq=> x.
81
    repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
Ralf Jung's avatar
Ralf Jung committed
82
    lia.
Dan Frumin's avatar
Dan Frumin committed
83 84 85
  Qed.
End gmultiset.

86
Arguments gmultisetO _ {_ _}.
Dan Frumin's avatar
Dan Frumin committed
87 88
Arguments gmultisetR _ {_ _}.
Arguments gmultisetUR _ {_ _}.