Library zoo.iris.base_logic.lib.auth_twins
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class AuthTwinsG Σ (A : ofe) (R : relation A) :=
{ #[local] auth_twins۰G۰var۰G :: GhostVarG Σ (leibnizO gname)
; #[local] auth_twins۰G۰mono۰G :: AuthMonoG Σ R
; #[local] auth_twins۰G۰twins۰G :: TwinsG Σ A
}.
Definition auth_twins۰Σ (A : ofe) (R : relation A) :=
#[ghost_var۰Σ (leibnizO gname)
; auth_mono۰Σ R
; twins۰Σ A
].
#[global] Instance subGｰauth_twins۰Σ Σ (A : ofe) (R : relation A) :
subG (auth_twins۰Σ A R) Σ →
AuthTwinsG Σ A R.
Section auth_twins۰G.
Context {A : ofe} (R : relation A).
Context `{auth_twins۰G : !AuthTwinsG Σ A R}.
Notation Rs := (
rtc R
).
Implicit Type a b : A.
Record auth_twins۰name :=
{ auth_twins۰name۰var : gname
; auth_twins۰name۰twins : gname
}.
Implicit Type γ : auth_twins۰name.
#[global] Instance auth_twins۰nameｰeq_dec : EqDecision auth_twins۰name :=
ltac:(solve_decision).
#[global] Instance auth_twins۰nameｰcountable :
Countable auth_twins۰name.
Definition auth_twins۰auth γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰auth R η (DfracOwn 1) a.
#[local] Instance : CustomIpat "auth" :=
" ( %{{pref}_}η & Hvar{} & {{pref}_}Hauth ) ".
Definition auth_twins۰twin₁ γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰lb R η a ∗
twins۰twin₁ γ.(auth_twins۰name۰twins) (DfracOwn 1) a.
#[local] Instance : CustomIpat "twin₁" :=
" ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin₁{_{suff}} ) ".
Definition auth_twins۰twin₂ γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰lb R η a ∗
twins۰twin₂ γ.(auth_twins۰name۰twins) a.
#[local] Instance : CustomIpat "twin₂" :=
" ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin₂{_{suff}} ) ".
#[global] Instance auth_twins۰authｰtimeless γ a :
Timeless (auth_twins۰auth γ a).
#[global] Instance auth_twins۰twin₁ｰtimeless γ a :
Discrete a →
Timeless (auth_twins۰twin₁ γ a).
#[global] Instance auth_twins۰twin₂ｰtimeless γ a :
Discrete a →
Timeless (auth_twins۰twin₂ γ a).
Lemma auth_twinsｰalloc a :
⊢ |==>
∃ γ,
auth_twins۰auth γ a ∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
Lemma auth_twins۰authｰexclusive `{!AntiSymm (≡) Rs} γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰auth γ a2 -∗
False.
Lemma auth_twins۰authｰexclusiveｰL `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰auth γ a2 -∗
False.
Lemma auth_twins۰twin₁ｰexclusive γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₁ γ a2 -∗
False.
Lemma auth_twins۰twin₂ｰexclusive γ a1 a2 :
auth_twins۰twin₂ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
False.
Lemma auth_twinsｰvalid₁ γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰twin₁ γ a2 -∗
⌜Rs a2 a1⌝.
Lemma auth_twinsｰvalid₂ γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜Rs a2 a1⌝.
Lemma auth_twinsｰagree γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
a1 ≡ a2.
Lemma auth_twinsｰagreeｰdiscrete `{!OfeDiscrete A} γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜a1 ≡ a2⌝.
Lemma auth_twinsｰagreeｰL `{!OfeDiscrete A} `{!LeibnizEquiv A} γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜a1 = a2⌝.
Lemma auth_twinsｰupdateｰauth {γ a a1 a2} a' :
auth_twins۰auth γ a -∗
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰auth γ a' ∗
auth_twins۰twin₁ γ a' ∗
auth_twins۰twin₂ γ a'.
Lemma auth_twinsｰupdateｰtwins {γ a1 a2} a :
Rs a a1 →
Rs a a2 →
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
Lemma auth_twinsｰupdateｰtwinsｰL `{!OfeDiscrete A} `{!LeibnizEquiv A} {γ a1 a2} a :
Rs a a1 →
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
End auth_twins۰G.
#[global] Opaque auth_twins۰auth.
#[global] Opaque auth_twins۰twin₁.
#[global] Opaque auth_twins۰twin₂.
Require Import zoo.common.countable.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class AuthTwinsG Σ (A : ofe) (R : relation A) :=
{ #[local] auth_twins۰G۰var۰G :: GhostVarG Σ (leibnizO gname)
; #[local] auth_twins۰G۰mono۰G :: AuthMonoG Σ R
; #[local] auth_twins۰G۰twins۰G :: TwinsG Σ A
}.
Definition auth_twins۰Σ (A : ofe) (R : relation A) :=
#[ghost_var۰Σ (leibnizO gname)
; auth_mono۰Σ R
; twins۰Σ A
].
#[global] Instance subGｰauth_twins۰Σ Σ (A : ofe) (R : relation A) :
subG (auth_twins۰Σ A R) Σ →
AuthTwinsG Σ A R.
Section auth_twins۰G.
Context {A : ofe} (R : relation A).
Context `{auth_twins۰G : !AuthTwinsG Σ A R}.
Notation Rs := (
rtc R
).
Implicit Type a b : A.
Record auth_twins۰name :=
{ auth_twins۰name۰var : gname
; auth_twins۰name۰twins : gname
}.
Implicit Type γ : auth_twins۰name.
#[global] Instance auth_twins۰nameｰeq_dec : EqDecision auth_twins۰name :=
ltac:(solve_decision).
#[global] Instance auth_twins۰nameｰcountable :
Countable auth_twins۰name.
Definition auth_twins۰auth γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰auth R η (DfracOwn 1) a.
#[local] Instance : CustomIpat "auth" :=
" ( %{{pref}_}η & Hvar{} & {{pref}_}Hauth ) ".
Definition auth_twins۰twin₁ γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰lb R η a ∗
twins۰twin₁ γ.(auth_twins۰name۰twins) (DfracOwn 1) a.
#[local] Instance : CustomIpat "twin₁" :=
" ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin₁{_{suff}} ) ".
Definition auth_twins۰twin₂ γ a : iProp Σ :=
∃ η,
ghost_var γ.(auth_twins۰name۰var) (DfracOwn (1/3)) η ∗
auth_mono۰lb R η a ∗
twins۰twin₂ γ.(auth_twins۰name۰twins) a.
#[local] Instance : CustomIpat "twin₂" :=
" ( %{{pref}_}η & Hvar{} & #Hlb{} & Htwin₂{_{suff}} ) ".
#[global] Instance auth_twins۰authｰtimeless γ a :
Timeless (auth_twins۰auth γ a).
#[global] Instance auth_twins۰twin₁ｰtimeless γ a :
Discrete a →
Timeless (auth_twins۰twin₁ γ a).
#[global] Instance auth_twins۰twin₂ｰtimeless γ a :
Discrete a →
Timeless (auth_twins۰twin₂ γ a).
Lemma auth_twinsｰalloc a :
⊢ |==>
∃ γ,
auth_twins۰auth γ a ∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
Lemma auth_twins۰authｰexclusive `{!AntiSymm (≡) Rs} γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰auth γ a2 -∗
False.
Lemma auth_twins۰authｰexclusiveｰL `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰auth γ a2 -∗
False.
Lemma auth_twins۰twin₁ｰexclusive γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₁ γ a2 -∗
False.
Lemma auth_twins۰twin₂ｰexclusive γ a1 a2 :
auth_twins۰twin₂ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
False.
Lemma auth_twinsｰvalid₁ γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰twin₁ γ a2 -∗
⌜Rs a2 a1⌝.
Lemma auth_twinsｰvalid₂ γ a1 a2 :
auth_twins۰auth γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜Rs a2 a1⌝.
Lemma auth_twinsｰagree γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
a1 ≡ a2.
Lemma auth_twinsｰagreeｰdiscrete `{!OfeDiscrete A} γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜a1 ≡ a2⌝.
Lemma auth_twinsｰagreeｰL `{!OfeDiscrete A} `{!LeibnizEquiv A} γ a1 a2 :
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 -∗
⌜a1 = a2⌝.
Lemma auth_twinsｰupdateｰauth {γ a a1 a2} a' :
auth_twins۰auth γ a -∗
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰auth γ a' ∗
auth_twins۰twin₁ γ a' ∗
auth_twins۰twin₂ γ a'.
Lemma auth_twinsｰupdateｰtwins {γ a1 a2} a :
Rs a a1 →
Rs a a2 →
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
Lemma auth_twinsｰupdateｰtwinsｰL `{!OfeDiscrete A} `{!LeibnizEquiv A} {γ a1 a2} a :
Rs a a1 →
auth_twins۰twin₁ γ a1 -∗
auth_twins۰twin₂ γ a2 ==∗
auth_twins۰twin₁ γ a ∗
auth_twins۰twin₂ γ a.
End auth_twins۰G.
#[global] Opaque auth_twins۰auth.
#[global] Opaque auth_twins۰twin₁.
#[global] Opaque auth_twins۰twin₂.