Library zoo.iris.base_logic.lib.auth_gmultiset

Require Import iris.algebra.gmultiset.

Require Import zoo.prelude.
Require Import zoo.iris.algebra.auth.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class AuthGmultisetG Σ A `{Countable A} :=
  { #[local] auth_gmultiset ۰ G ۰ inG :: inG Σ (authR (gmultisetUR A))
  }.

Definition auth_gmultiset ۰ Σ A `{Countable A} :=
  #[GFunctor (authR (gmultisetUR A))
  ].
#[global] Instance subG ｰ auth_gmultiset ۰ Σ Σ A `{Countable A} :
  subG (auth_gmultiset ۰ Σ A) Σ →
  AuthGmultisetG Σ A.

Section auth_gmultiset ۰ G.
  Context `{auth_gmultiset ۰ G : AuthGmultisetG Σ A}.

  Implicit Type x y : gmultiset A.

  Definition auth_gmultiset ۰ auth γ dq x :=
    own γ (●{dq } x).
  Definition auth_gmultiset ۰ frag γ y :=
    own γ (◯ y).

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

  #[global] Instance auth_gmultiset ۰ auth ｰ timeless γ dq x :
    Timeless (auth_gmultiset ۰ auth γ dq x).
  #[global] Instance auth_gmultiset ۰ frag ｰ timeless γ y :
    Timeless (auth_gmultiset ۰ frag γ y).

  #[global] Instance auth_gmultiset ۰ auth ｰ persistent γ x :
    Persistent (auth_gmultiset ۰ auth γ DfracDiscarded x).

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

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

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

  Lemma auth_gmultiset ۰ frag ｰ combine γ y1 y2 :
    auth_gmultiset ۰ frag γ y1 -∗
    auth_gmultiset ۰ frag γ y2 -∗
    auth_gmultiset ۰ frag γ (y1 ⊎ y2).

  Lemma auth_gmultiset ｰ subseteq γ dq x y :
    auth_gmultiset ۰ auth γ dq x -∗
    auth_gmultiset ۰ frag γ y -∗
    ⌜y ⊆ x ⌝.
  Lemma auth_gmultiset ｰ elem_of γ dq x b :
    auth_gmultiset ۰ auth γ dq x -∗
    auth_gmultiset ۰ frag γ {[+b +]} -∗
    ⌜b ∈ x ⌝.

  Lemma auth_gmultiset ｰ update ｰ alloc {γ x} y :
    auth_gmultiset ۰ auth γ (DfracOwn 1) x ⊢ |==>
      auth_gmultiset ۰ auth γ (DfracOwn 1) (y ⊎ x) ∗
      auth_gmultiset ۰ frag γ y.
  Lemma auth_gmultiset ｰ update ｰ alloc ｰ singleton {γ x} a :
    auth_gmultiset ۰ auth γ (DfracOwn 1) x ⊢ |==>
      auth_gmultiset ۰ auth γ (DfracOwn 1) ({[+a +]} ⊎ x) ∗
      auth_gmultiset ۰ frag γ {[+a +]}.

  Lemma auth_gmultiset ｰ update ｰ dealloc {γ x} y :
    auth_gmultiset ۰ auth γ (DfracOwn 1) x -∗
    auth_gmultiset ۰ frag γ y ==∗
    auth_gmultiset ۰ auth γ (DfracOwn 1) (x ∖ y).
End auth_gmultiset ۰ G.

#[global] Opaque auth_gmultiset ۰ auth.
#[global] Opaque auth_gmultiset ۰ frag.