Library zoo.iris.base_logic.lib.twins
Require Import zoo.prelude.
Require Import zoo.iris.algebra.lib.twins.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.algebra.twins.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class TwinsG Σ F :=
{ #[local] twins۰G۰inG :: inG Σ (twins۰R $ oFunctor_apply F $ iPropO Σ)
}.
Definition twins۰Σ F `{!oFunctorContractive F} :=
#[GFunctor (twins۰RF F)
].
#[global] Instance subGｰtwins۰Σ Σ F `{!oFunctorContractive F} :
subG (twins۰Σ F) Σ →
TwinsG Σ F.
Section twins۰G.
Context `{twins۰G : !TwinsG Σ F}.
Definition twins۰twin₁ γ dq a :=
own γ (twins۰twin₁ dq a).
Definition twins۰twin₂ γ a :=
own γ (twins۰twin₂ a).
#[global] Instance twins۰twin₁ｰproper γ dq :
Proper ((≡) ==> (≡)) (twins۰twin₁ γ dq).
#[global] Instance twins۰twin₂ｰproper γ :
Proper ((≡) ==> (≡)) (twins۰twin₂ γ).
#[global] Instance twins۰twin₁ｰtimeless γ dq a :
Discrete a →
Timeless (twins۰twin₁ γ dq a).
#[global] Instance twins۰twin₂ｰtimeless γ a :
Discrete a →
Timeless (twins۰twin₂ γ a).
#[global] Instance twins۰twin₁ｰpersistent γ a :
Persistent (twins۰twin₁ γ DfracDiscarded a).
#[global] Instance twins۰twin₁ｰfractional γ a :
Fractional (λ q, twins۰twin₁ γ (DfracOwn q) a).
#[global] Instance twins۰twin₁ｰas_fractional γ q a :
AsFractional (twins۰twin₁ γ (DfracOwn q) a) (λ q, twins۰twin₁ γ (DfracOwn q) a) q.
Lemma twinsｰalloc a b :
a ≡ b →
⊢ |==>
∃ γ,
twins۰twin₁ γ (DfracOwn 1) a ∗
twins۰twin₂ γ b.
Lemma twinsｰalloc' a :
⊢ |==>
∃ γ,
twins۰twin₁ γ (DfracOwn 1) a ∗ twins۰twin₂ γ a.
Lemma twins۰twin₁ｰvalid γ dq a :
twins۰twin₁ γ dq a ⊢
⌜✓ dq⌝.
Lemma twins۰twin₁ｰcombine γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
a1 ≡ a2 ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2 γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
a1 ≡ a2.
Lemma twins۰twin₁ｰagree γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
a1 ≡ a2.
Lemma twins۰twin₁ｰdfracｰne γ1 dq1 a1 γ2 dq2 a2 :
¬ ✓ (dq1 ⋅ dq2) →
twins۰twin₁ γ1 dq1 a1 -∗
twins۰twin₁ γ2 dq2 a2 -∗
⌜γ1 ≠ γ2⌝.
Lemma twins۰twin₁ｰne γ1 a1 γ2 dq2 a2 :
twins۰twin₁ γ1 (DfracOwn 1) a1 -∗
twins۰twin₁ γ2 dq2 a2 -∗
⌜γ1 ≠ γ2⌝.
Lemma twins۰twin₁ｰexclusive γ a1 dq2 a2 :
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₁ γ dq2 a2 -∗
False.
Lemma twins۰twin₁ｰpersist γ dq a :
twins۰twin₁ γ dq a ⊢ |==>
twins۰twin₁ γ DfracDiscarded a.
Lemma twins۰twin₂ｰexclusive γ a1 a2 :
twins۰twin₂ γ a1 -∗
twins۰twin₂ γ a2 -∗
False.
Lemma twinsｰagree γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
a ≡ b.
Section ofe_discrete.
Context `{!OfeDiscrete $ oFunctor_apply F $ iPropO Σ}.
Lemma twins۰twin₁ｰcombineｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 ≡ a2⌝ ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2ｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜a1 ≡ a2⌝.
Lemma twins۰twin₁ｰagreeｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 ≡ a2⌝.
Lemma twinsｰagreeｰdiscrete γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
⌜a ≡ b⌝.
Section leibniz_equiv.
Context `{!LeibnizEquiv $ oFunctor_apply F $ iPropO Σ}.
Lemma twins۰twin₁ｰcombineｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 = a2⌝ ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2ｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜a1 = a2⌝.
Lemma twins۰twin₁ｰagreeｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 = a2⌝.
Lemma twinsｰagreeｰL γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
⌜a = b⌝.
End leibniz_equiv.
End ofe_discrete.
Lemma twinsｰupdateｰequivI {γ a1 b1} a2 b2 :
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₂ γ b1 -∗
a2 ≡ b2 ==∗
twins۰twin₁ γ (DfracOwn 1) a2 ∗
twins۰twin₂ γ b2.
Lemma twinsｰupdateｰequiv {γ a1 b1} a2 b2 :
a2 ≡ b2 →
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₂ γ b1 ==∗
twins۰twin₁ γ (DfracOwn 1) a2 ∗
twins۰twin₂ γ b2.
Lemma twinsｰupdate {γ a b} a' :
twins۰twin₁ γ (DfracOwn 1) a -∗
twins۰twin₂ γ b ==∗
twins۰twin₁ γ (DfracOwn 1) a' ∗
twins۰twin₂ γ a'.
End twins۰G.
#[global] Opaque twins۰twin₁.
#[global] Opaque twins۰twin₂.
Require Import zoo.iris.algebra.lib.twins.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.algebra.twins.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class TwinsG Σ F :=
{ #[local] twins۰G۰inG :: inG Σ (twins۰R $ oFunctor_apply F $ iPropO Σ)
}.
Definition twins۰Σ F `{!oFunctorContractive F} :=
#[GFunctor (twins۰RF F)
].
#[global] Instance subGｰtwins۰Σ Σ F `{!oFunctorContractive F} :
subG (twins۰Σ F) Σ →
TwinsG Σ F.
Section twins۰G.
Context `{twins۰G : !TwinsG Σ F}.
Definition twins۰twin₁ γ dq a :=
own γ (twins۰twin₁ dq a).
Definition twins۰twin₂ γ a :=
own γ (twins۰twin₂ a).
#[global] Instance twins۰twin₁ｰproper γ dq :
Proper ((≡) ==> (≡)) (twins۰twin₁ γ dq).
#[global] Instance twins۰twin₂ｰproper γ :
Proper ((≡) ==> (≡)) (twins۰twin₂ γ).
#[global] Instance twins۰twin₁ｰtimeless γ dq a :
Discrete a →
Timeless (twins۰twin₁ γ dq a).
#[global] Instance twins۰twin₂ｰtimeless γ a :
Discrete a →
Timeless (twins۰twin₂ γ a).
#[global] Instance twins۰twin₁ｰpersistent γ a :
Persistent (twins۰twin₁ γ DfracDiscarded a).
#[global] Instance twins۰twin₁ｰfractional γ a :
Fractional (λ q, twins۰twin₁ γ (DfracOwn q) a).
#[global] Instance twins۰twin₁ｰas_fractional γ q a :
AsFractional (twins۰twin₁ γ (DfracOwn q) a) (λ q, twins۰twin₁ γ (DfracOwn q) a) q.
Lemma twinsｰalloc a b :
a ≡ b →
⊢ |==>
∃ γ,
twins۰twin₁ γ (DfracOwn 1) a ∗
twins۰twin₂ γ b.
Lemma twinsｰalloc' a :
⊢ |==>
∃ γ,
twins۰twin₁ γ (DfracOwn 1) a ∗ twins۰twin₂ γ a.
Lemma twins۰twin₁ｰvalid γ dq a :
twins۰twin₁ γ dq a ⊢
⌜✓ dq⌝.
Lemma twins۰twin₁ｰcombine γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
a1 ≡ a2 ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2 γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
a1 ≡ a2.
Lemma twins۰twin₁ｰagree γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
a1 ≡ a2.
Lemma twins۰twin₁ｰdfracｰne γ1 dq1 a1 γ2 dq2 a2 :
¬ ✓ (dq1 ⋅ dq2) →
twins۰twin₁ γ1 dq1 a1 -∗
twins۰twin₁ γ2 dq2 a2 -∗
⌜γ1 ≠ γ2⌝.
Lemma twins۰twin₁ｰne γ1 a1 γ2 dq2 a2 :
twins۰twin₁ γ1 (DfracOwn 1) a1 -∗
twins۰twin₁ γ2 dq2 a2 -∗
⌜γ1 ≠ γ2⌝.
Lemma twins۰twin₁ｰexclusive γ a1 dq2 a2 :
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₁ γ dq2 a2 -∗
False.
Lemma twins۰twin₁ｰpersist γ dq a :
twins۰twin₁ γ dq a ⊢ |==>
twins۰twin₁ γ DfracDiscarded a.
Lemma twins۰twin₂ｰexclusive γ a1 a2 :
twins۰twin₂ γ a1 -∗
twins۰twin₂ γ a2 -∗
False.
Lemma twinsｰagree γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
a ≡ b.
Section ofe_discrete.
Context `{!OfeDiscrete $ oFunctor_apply F $ iPropO Σ}.
Lemma twins۰twin₁ｰcombineｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 ≡ a2⌝ ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2ｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜a1 ≡ a2⌝.
Lemma twins۰twin₁ｰagreeｰdiscrete γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 ≡ a2⌝.
Lemma twinsｰagreeｰdiscrete γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
⌜a ≡ b⌝.
Section leibniz_equiv.
Context `{!LeibnizEquiv $ oFunctor_apply F $ iPropO Σ}.
Lemma twins۰twin₁ｰcombineｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 = a2⌝ ∗
twins۰twin₁ γ (dq1 ⋅ dq2) a1.
Lemma twins۰twin₁ｰvalidｰ2ｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜a1 = a2⌝.
Lemma twins۰twin₁ｰagreeｰL γ dq1 a1 dq2 a2 :
twins۰twin₁ γ dq1 a1 -∗
twins۰twin₁ γ dq2 a2 -∗
⌜a1 = a2⌝.
Lemma twinsｰagreeｰL γ dq a b :
twins۰twin₁ γ dq a -∗
twins۰twin₂ γ b -∗
⌜a = b⌝.
End leibniz_equiv.
End ofe_discrete.
Lemma twinsｰupdateｰequivI {γ a1 b1} a2 b2 :
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₂ γ b1 -∗
a2 ≡ b2 ==∗
twins۰twin₁ γ (DfracOwn 1) a2 ∗
twins۰twin₂ γ b2.
Lemma twinsｰupdateｰequiv {γ a1 b1} a2 b2 :
a2 ≡ b2 →
twins۰twin₁ γ (DfracOwn 1) a1 -∗
twins۰twin₂ γ b1 ==∗
twins۰twin₁ γ (DfracOwn 1) a2 ∗
twins۰twin₂ γ b2.
Lemma twinsｰupdate {γ a b} a' :
twins۰twin₁ γ (DfracOwn 1) a -∗
twins۰twin₂ γ b ==∗
twins۰twin₁ γ (DfracOwn 1) a' ∗
twins۰twin₂ γ a'.
End twins۰G.
#[global] Opaque twins۰twin₁.
#[global] Opaque twins۰twin₂.