Library zoo.iris.base_logic.lib.ghost_pred
Require Import zoo.prelude.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class GhostPredG Σ A :=
{ #[local] ghost_pred۰G۰ghost_var۰G :: GhostVarG Σ (A -d> ▶ ∙)
}.
Definition ghost_pred۰Σ A :=
#[ghost_var۰Σ (A -d> ▶ ∙)
].
#[global] Instance subGｰghost_pred۰Σ Σ A :
subG (ghost_pred۰Σ A) Σ →
GhostPredG Σ A.
Section ghost_pred۰G.
Context `{ghost_pred۰G : !GhostPredG Σ A}.
Implicit Type Ψ : A → iProp Σ.
Definition ghost_pred γ dq Ψ :=
ghost_var γ dq (Next ∘ Ψ).
#[global] Instance ghost_predｰcontractive γ dq n :
Proper ((pointwise_relation _ (dist_later n)) ==> (≡{n}≡)) (ghost_pred γ dq).
#[global] Instance ghost_predｰproper γ dq :
Proper ((≡) ==> (≡)) (ghost_pred γ dq : (A -d> iProp Σ) → _).
#[global] Instance ghost_predｰpersistent γ Ψ :
Persistent (ghost_pred γ DfracDiscarded Ψ).
#[global] Instance ghost_predｰfractional γ Ψ :
Fractional (λ q, ghost_pred γ (DfracOwn q) Ψ).
#[global] Instance ghost_predｰas_fractional γ Ψ q :
AsFractional (ghost_pred γ (DfracOwn q) Ψ) (λ q, ghost_pred γ (DfracOwn q) Ψ) q.
Lemma ghost_predｰalloc Ψ :
⊢ |==>
∃ γ,
ghost_pred γ (DfracOwn 1) Ψ.
Lemma ghost_predｰallocｰcofinite (γs : gset gname) Ψ :
⊢ |==>
∃ γ,
⌜γ ∉ γs⌝ ∗
ghost_pred γ (DfracOwn 1) Ψ.
Lemma ghost_predｰvalid γ dq Ψ :
ghost_pred γ dq Ψ ⊢
⌜✓ dq⌝.
Lemma ghost_predｰcombine {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
▷ (Ψ1 x ≡ Ψ2 x) ∗
ghost_pred γ (dq1 ⋅ dq2) Ψ1.
Lemma ghost_predｰvalidｰ2 {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
▷ (Ψ1 x ≡ Ψ2 x).
Lemma ghost_predｰagree {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
▷ (Ψ1 x ≡ Ψ2 x).
Lemma ghost_predｰdfracｰne γ1 dq1 Ψ1 γ2 dq2 Ψ2 :
¬ ✓ (dq1 ⋅ dq2) →
ghost_pred γ1 dq1 Ψ1 -∗
ghost_pred γ2 dq2 Ψ2 -∗
⌜γ1 ≠ γ2⌝.
Lemma ghost_predｰne γ1 Ψ1 γ2 dq2 Ψ2 :
ghost_pred γ1 (DfracOwn 1) Ψ1 -∗
ghost_pred γ2 dq2 Ψ2 -∗
⌜γ1 ≠ γ2⌝.
Lemma ghost_predｰexclusive γ Ψ1 dq2 Ψ2 :
ghost_pred γ (DfracOwn 1) Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
False.
Lemma ghost_predｰpersist γ dq Ψ :
ghost_pred γ dq Ψ ⊢ |==>
ghost_pred γ DfracDiscarded Ψ.
Lemma ghost_predｰupdate {γ Ψ} Ψ' :
ghost_pred γ (DfracOwn 1) Ψ ⊢ |==>
ghost_pred γ (DfracOwn 1) Ψ'.
End ghost_pred۰G.
#[global] Opaque ghost_pred.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Class GhostPredG Σ A :=
{ #[local] ghost_pred۰G۰ghost_var۰G :: GhostVarG Σ (A -d> ▶ ∙)
}.
Definition ghost_pred۰Σ A :=
#[ghost_var۰Σ (A -d> ▶ ∙)
].
#[global] Instance subGｰghost_pred۰Σ Σ A :
subG (ghost_pred۰Σ A) Σ →
GhostPredG Σ A.
Section ghost_pred۰G.
Context `{ghost_pred۰G : !GhostPredG Σ A}.
Implicit Type Ψ : A → iProp Σ.
Definition ghost_pred γ dq Ψ :=
ghost_var γ dq (Next ∘ Ψ).
#[global] Instance ghost_predｰcontractive γ dq n :
Proper ((pointwise_relation _ (dist_later n)) ==> (≡{n}≡)) (ghost_pred γ dq).
#[global] Instance ghost_predｰproper γ dq :
Proper ((≡) ==> (≡)) (ghost_pred γ dq : (A -d> iProp Σ) → _).
#[global] Instance ghost_predｰpersistent γ Ψ :
Persistent (ghost_pred γ DfracDiscarded Ψ).
#[global] Instance ghost_predｰfractional γ Ψ :
Fractional (λ q, ghost_pred γ (DfracOwn q) Ψ).
#[global] Instance ghost_predｰas_fractional γ Ψ q :
AsFractional (ghost_pred γ (DfracOwn q) Ψ) (λ q, ghost_pred γ (DfracOwn q) Ψ) q.
Lemma ghost_predｰalloc Ψ :
⊢ |==>
∃ γ,
ghost_pred γ (DfracOwn 1) Ψ.
Lemma ghost_predｰallocｰcofinite (γs : gset gname) Ψ :
⊢ |==>
∃ γ,
⌜γ ∉ γs⌝ ∗
ghost_pred γ (DfracOwn 1) Ψ.
Lemma ghost_predｰvalid γ dq Ψ :
ghost_pred γ dq Ψ ⊢
⌜✓ dq⌝.
Lemma ghost_predｰcombine {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
▷ (Ψ1 x ≡ Ψ2 x) ∗
ghost_pred γ (dq1 ⋅ dq2) Ψ1.
Lemma ghost_predｰvalidｰ2 {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
▷ (Ψ1 x ≡ Ψ2 x).
Lemma ghost_predｰagree {γ dq1 Ψ1 dq2 Ψ2} x :
ghost_pred γ dq1 Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
▷ (Ψ1 x ≡ Ψ2 x).
Lemma ghost_predｰdfracｰne γ1 dq1 Ψ1 γ2 dq2 Ψ2 :
¬ ✓ (dq1 ⋅ dq2) →
ghost_pred γ1 dq1 Ψ1 -∗
ghost_pred γ2 dq2 Ψ2 -∗
⌜γ1 ≠ γ2⌝.
Lemma ghost_predｰne γ1 Ψ1 γ2 dq2 Ψ2 :
ghost_pred γ1 (DfracOwn 1) Ψ1 -∗
ghost_pred γ2 dq2 Ψ2 -∗
⌜γ1 ≠ γ2⌝.
Lemma ghost_predｰexclusive γ Ψ1 dq2 Ψ2 :
ghost_pred γ (DfracOwn 1) Ψ1 -∗
ghost_pred γ dq2 Ψ2 -∗
False.
Lemma ghost_predｰpersist γ dq Ψ :
ghost_pred γ dq Ψ ⊢ |==>
ghost_pred γ DfracDiscarded Ψ.
Lemma ghost_predｰupdate {γ Ψ} Ψ' :
ghost_pred γ (DfracOwn 1) Ψ ⊢ |==>
ghost_pred γ (DfracOwn 1) Ψ'.
End ghost_pred۰G.
#[global] Opaque ghost_pred.