Library zoo.iris.base_logic.lib.auth_dgset

From iris.algebra Require Import
  gset.

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 AuthDgsetG Σ A `{Countable A} :=
  { #[local] auth_dgset_G_inG :: inG Σ (authR (gset_disjUR A))
  }.

Definition auth_dgset_Σ A `{Countable A} :=
  #[GFunctor (authR (gset_disjUR A))
  ].
#[global] Instance subG_auth_dgset_Σ Σ A `{Countable A} :
  subG (auth_dgset_Σ A) Σ →
  AuthDgsetG Σ A.

Section auth_dgset_G.
  Context `{auth_dgset_G : AuthDgsetG Σ A}.

  Implicit Types x y : gset A.

  Definition auth_dgset_auth γ dq x :=
    own γ (●{dq} GSet x).
  Definition auth_dgset_frag γ y :=
    own γ (◯ GSet y).

  #[global] Instance auth_dgset_auth_proper γ dq :
    Proper ((≡) ==> (≡)) (auth_dgset_auth γ dq).
  #[global] Instance auth_dgset_frag_proper γ :
    Proper ((≡) ==> (≡)) (auth_dgset_frag γ).

  #[global] Instance auth_dgset_auth_timeless γ dq x :
    Timeless (auth_dgset_auth γ dq x).
  #[global] Instance auth_dgset_frag_timeless γ y :
    Timeless (auth_dgset_frag γ y).

  #[global] Instance auth_dgset_auth_persistent γ x :
    Persistent (auth_dgset_auth γ DfracDiscarded x).

  #[global] Instance auth_dgset_auth_fractional γ x :
    Fractional (λ q, auth_dgset_auth γ (DfracOwn q) x).
  #[global] Instance auth_dgset_auth_as_fractional γ q x :
    AsFractional (auth_dgset_auth γ (DfracOwn q) x) (λ q, auth_dgset_auth γ (DfracOwn q) x) q.

  Lemma auth_dgset_alloc x :
    ⊢ |==>
      ∃ γ,
      auth_dgset_auth γ (DfracOwn 1) x ∗
      auth_dgset_frag γ x.
  Lemma auth_dgset_alloc_empty :
    ⊢ |==>
      ∃ γ,
      auth_dgset_auth γ (DfracOwn 1) ∅.

  Lemma auth_dgset_auth_valid γ dq x :
    auth_dgset_auth γ dq x ⊢
    ⌜✓ dq⌝.
  Lemma auth_dgset_auth_combine γ dq1 x1 dq2 x2 :
    auth_dgset_auth γ dq1 x1 -∗
    auth_dgset_auth γ dq2 x2 -∗
      ⌜x1 = x2⌝ ∗
      auth_dgset_auth γ (dq1 ⋅ dq2) x1.
  Lemma auth_dgset_auth_valid_2 γ dq1 x1 dq2 x2 :
    auth_dgset_auth γ dq1 x1 -∗
    auth_dgset_auth γ dq2 x2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜x1 = x2⌝.
  Lemma auth_dgset_auth_agree γ dq1 x1 dq2 x2 :
    auth_dgset_auth γ dq1 x1 -∗
    auth_dgset_auth γ dq2 x2 -∗
    ⌜x1 = x2⌝.
  Lemma auth_dgset_auth_dfrac_ne γ1 dq1 x1 γ2 dq2 x2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    auth_dgset_auth γ1 dq1 x1 -∗
    auth_dgset_auth γ2 dq2 x2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_dgset_auth_ne γ1 x1 γ2 dq2 x2 :
    auth_dgset_auth γ1 (DfracOwn 1) x1 -∗
    auth_dgset_auth γ2 dq2 x2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_dgset_auth_exclusive γ x1 dq2 x2 :
    auth_dgset_auth γ (DfracOwn 1) x1 -∗
    auth_dgset_auth γ dq2 x2 -∗
    False.
  Lemma auth_dgset_auth_persist γ dq x :
    auth_dgset_auth γ dq x ⊢ |==>
    auth_dgset_auth γ DfracDiscarded x.

  Lemma auth_dgset_frag_disjoint γ y1 y2 :
    auth_dgset_frag γ y1 -∗
    auth_dgset_frag γ y2 -∗
    ⌜y1 ## y2⌝.
  Lemma auth_dgset_frag_singleton_ne γ b1 b2 :
    auth_dgset_frag γ {[b1]} -∗
    auth_dgset_frag γ {[b2]} -∗
    ⌜b1 ≠ b2⌝.
  Lemma auth_dgset_frag_exclusive γ y :
    y ≠ ∅ →
    auth_dgset_frag γ y -∗
    auth_dgset_frag γ y -∗
    False.
  Lemma auth_dgset_frag_singleton_exclusive γ b :
    auth_dgset_frag γ {[b]} -∗
    auth_dgset_frag γ {[b]} -∗
    False.

  Lemma auth_dgset_frag_combine γ y1 y2 :
    auth_dgset_frag γ y1 -∗
    auth_dgset_frag γ y2 -∗
    auth_dgset_frag γ (y1 ∪ y2).

  Lemma auth_dgset_subseteq γ dq x y :
    auth_dgset_auth γ dq x -∗
    auth_dgset_frag γ y -∗
    ⌜y ⊆ x⌝.
  Lemma auth_dgset_elem_of γ dq x b :
    auth_dgset_auth γ dq x -∗
    auth_dgset_frag γ {[b]} -∗
    ⌜b ∈ x⌝.

  Lemma auth_dgset_update_alloc {γ x} y :
    x ## y →
    auth_dgset_auth γ (DfracOwn 1) x ⊢ |==>
      auth_dgset_auth γ (DfracOwn 1) (y ∪ x) ∗
      auth_dgset_frag γ y.
  Lemma auth_dgset_update_alloc_singleton {γ x} a :
    a ∉ x →
    auth_dgset_auth γ (DfracOwn 1) x ⊢ |==>
      auth_dgset_auth γ (DfracOwn 1) ({[a]} ∪ x) ∗
      auth_dgset_frag γ {[a]}.

  Lemma auth_dgset_update_dealloc {γ x} y :
    auth_dgset_auth γ (DfracOwn 1) x -∗
    auth_dgset_frag γ y ==∗
    auth_dgset_auth γ (DfracOwn 1) (x ∖ y).
End auth_dgset_G.

#[global] Opaque auth_dgset_auth.
#[global] Opaque auth_dgset_frag.