Library zoo.iris.base_logic.lib.auth_dgset
Require Import iris.algebra.gset.
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 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 Type 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.
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 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 Type 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.