Library zoo.iris.bi.big_op.big_sepMS

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Section bi.
  Context {PROP : bi}.

  Section big_sepMS.
    Context `{Countable K}.

    Implicit Type s : gmultiset K.
    Implicit Type P : PROP.
    Implicit Type Φ : K → PROP.

    Lemma big_sepMSｰinsert₁ {Φ} x s :
      ([∗ mset] y ∈ ({[+x+]} ⊎ s), Φ y) ⊢
        Φ x ∗
        [∗ mset] y ∈ s, Φ y.
    Lemma big_sepMSｰinsert₂ {Φ} x s :
      ([∗ mset] y ∈ s, Φ y) -∗
      Φ x -∗
      [∗ mset] y ∈ ({[+x+]} ⊎ s), Φ y.

    Lemma big_sepMSｰdelete₁ {Φ} x s :
      x ∈ s →
      ([∗ mset] y ∈ s, Φ y) ⊢
        Φ x ∗
        [∗ mset] y ∈ (s ∖ {[+x+]}), Φ y.
    Lemma big_sepMSｰdelete₂ {Φ} x s :
      x ∈ s →
      ([∗ mset] y ∈ (s ∖ {[+x+]}), Φ y) -∗
      Φ x -∗
      [∗ mset] y ∈ s, Φ y.

    Lemma big_sepMSｰdisj_union_list {Φ} ss :
      ([∗ mset] x ∈ ⋃+ ss, Φ x) ⊣⊢
      [∗ list] s ∈ ss, [∗ mset] x ∈ s, Φ x.
    Lemma big_sepMSｰdisj_union_list₁ {Φ} ss :
      ([∗ mset] x ∈ ⋃+ ss, Φ x) ⊢
      [∗ list] s ∈ ss, [∗ mset] x ∈ s, Φ x.
    Lemma big_sepMSｰdisj_union_list₂ {Φ} ss :
      ([∗ list] s ∈ ss, [∗ mset] x ∈ s, Φ x) ⊢
      [∗ mset] x ∈ ⋃+ ss, Φ x.
  End big_sepMS.
End bi.