Library zoo.iris.base_logic.lib.auth_gmultiset

From iris.algebra Require Import
  gmultiset.

From zoo Require Import
  prelude.
From zoo.iris.algebra Require Import
  auth.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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 Types 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.