Library zoo.iris.base_logic.lib.mono_gmultiset

Require Import zoo.prelude.
Require Import zoo.common.relations.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class MonoGmultisetG Σ A `{Countable A} :=
  { #[local] mono_gmultiset ۰ G ۰ mono ۰ G :: AuthMonoG Σ (A := leibnizO (gmultiset A)) subseteq
  }.

Definition mono_gmultiset ۰ Σ A `{Countable A} :=
  #[auth_mono ۰ Σ (A := leibnizO (gmultiset A)) subseteq
  ].
#[global] Instance subG ｰ mono_gmultiset ۰ Σ Σ V `{Countable V} :
  subG (mono_gmultiset ۰ Σ V) Σ →
  MonoGmultisetG Σ V.

Section mono_gmultiset ۰ G.
  Context `{mono_gmultiset ۰ G : MonoGmultisetG Σ A}.

  Implicit Type a : A.
  Implicit Type s : gmultiset A.

  Definition mono_gmultiset ۰ auth γ dq s :=
    auth_mono ۰ auth subseteq γ dq s.
  Definition mono_gmultiset ۰ lb γ s :=
    auth_mono ۰ lb subseteq γ s.
  Definition mono_gmultiset ۰ elem γ a :=
    mono_gmultiset ۰ lb γ {[+a +]}.

  #[global] Instance mono_gmultiset ۰ auth ｰ proper γ dq :
    Proper ((≡) ==> (≡)) (mono_gmultiset ۰ auth γ dq).
  #[global] Instance mono_gmultiset ۰ lb ｰ proper γ :
    Proper ((≡) ==> (≡)) (mono_gmultiset ۰ lb γ).

  #[global] Instance mono_gmultiset ۰ auth ｰ timeless γ dq s :
    Timeless (mono_gmultiset ۰ auth γ dq s).
  #[global] Instance mono_gmultiset ۰ lb ｰ timeless γ s :
    Timeless (mono_gmultiset ۰ lb γ s).

  #[global] Instance mono_gmultiset ۰ auth ｰ persistent γ s :
    Persistent (mono_gmultiset ۰ auth γ DfracDiscarded s).
  #[global] Instance mono_gmultiset ۰ lb ｰ persistent γ s :
    Persistent (mono_gmultiset ۰ lb γ s).

  #[global] Instance mono_gmultiset ۰ auth ｰ fractional γ s :
    Fractional (λ q, mono_gmultiset ۰ auth γ (DfracOwn q) s).
  #[global] Instance mono_gmultiset ۰ auth ｰ as_fractional γ q s :
    AsFractional (mono_gmultiset ۰ auth γ (DfracOwn q) s) (λ q, mono_gmultiset ۰ auth γ (DfracOwn q) s) q.

  Lemma mono_gmultiset ｰ alloc s :
    ⊢ |==>
      ∃ γ ,
      mono_gmultiset ۰ auth γ (DfracOwn 1) s.

  Lemma mono_gmultiset ۰ auth ｰ valid γ dq s :
    mono_gmultiset ۰ auth γ dq s ⊢
    ⌜✓ dq ⌝.
  Lemma mono_gmultiset ۰ auth ｰ combine γ dq1 s1 dq2 s2 :
    mono_gmultiset ۰ auth γ dq1 s1 -∗
    mono_gmultiset ۰ auth γ dq2 s2 -∗
      ⌜s1 = s2 ⌝ ∗
      mono_gmultiset ۰ auth γ (dq1 ⋅ dq2) s1.
  Lemma mono_gmultiset ۰ auth ｰ valid ｰ2 γ dq1 s1 dq2 s2 :
    mono_gmultiset ۰ auth γ dq1 s1 -∗
    mono_gmultiset ۰ auth γ dq2 s2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜s1 = s2 ⌝.
  Lemma mono_gmultiset ۰ auth ｰ agree γ dq1 s1 dq2 s2 :
    mono_gmultiset ۰ auth γ dq1 s1 -∗
    mono_gmultiset ۰ auth γ dq2 s2 -∗
    ⌜s1 = s2 ⌝.
  Lemma mono_gmultiset ۰ auth ｰ dfrac ｰ ne γ1 dq1 s1 γ2 dq2 s2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    mono_gmultiset ۰ auth γ1 dq1 s1 -∗
    mono_gmultiset ۰ auth γ2 dq2 s2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma mono_gmultiset ۰ auth ｰ ne γ1 s1 γ2 dq2 s2 :
    mono_gmultiset ۰ auth γ1 (DfracOwn 1) s1 -∗
    mono_gmultiset ۰ auth γ2 dq2 s2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma mono_gmultiset ۰ auth ｰ exclusive γ s1 dq2 s2 :
    mono_gmultiset ۰ auth γ (DfracOwn 1) s1 -∗
    mono_gmultiset ۰ auth γ dq2 s2 -∗
    False.
  Lemma mono_gmultiset ۰ auth ｰ persist γ dq s :
    mono_gmultiset ۰ auth γ dq s ⊢ |==>
    mono_gmultiset ۰ auth γ DfracDiscarded s.

  Lemma mono_gmultiset ۰ lb ｰ get γ dq s :
    mono_gmultiset ۰ auth γ dq s ⊢
    mono_gmultiset ۰ lb γ s.
  Lemma mono_gmultiset ۰ lb ｰ mono {γ s} s' :
    s' ⊆ s →
    mono_gmultiset ۰ lb γ s ⊢
    mono_gmultiset ۰ lb γ s'.
  Lemma mono_gmultiset ۰ elem ｰ get {γ dq s} a :
    a ∈ s →
    mono_gmultiset ۰ auth γ dq s ⊢
    mono_gmultiset ۰ elem γ a.

  Lemma mono_gmultiset ۰ lb ｰ valid γ dq s1 s2 :
    mono_gmultiset ۰ auth γ dq s1 -∗
    mono_gmultiset ۰ lb γ s2 -∗
    ⌜s2 ⊆ s1 ⌝.
  Lemma mono_gmultiset ۰ elem ｰ valid γ dq s a :
    mono_gmultiset ۰ auth γ dq s -∗
    mono_gmultiset ۰ elem γ a -∗
    ⌜a ∈ s ⌝.

  Lemma mono_gmultiset ｰ update {γ s} s' :
    s ⊆ s' →
    mono_gmultiset ۰ auth γ (DfracOwn 1) s ⊢ |==>
    mono_gmultiset ۰ auth γ (DfracOwn 1) s'.
  Lemma mono_gmultiset ｰ insert {γ s} a :
    mono_gmultiset ۰ auth γ (DfracOwn 1) s ⊢ |==>
    mono_gmultiset ۰ auth γ (DfracOwn 1) ({[+a +]} ⊎ s).
  Lemma mono_gmultiset ｰ insert' {γ s} a :
    mono_gmultiset ۰ auth γ (DfracOwn 1) s ⊢ |==>
      mono_gmultiset ۰ auth γ (DfracOwn 1) ({[+a +]} ⊎ s) ∗
      mono_gmultiset ۰ elem γ a.
End mono_gmultiset ۰ G.

#[global] Opaque mono_gmultiset ۰ auth.
#[global] Opaque mono_gmultiset ۰ lb.