Library zoo.iris.base_logic.lib.ghost_prop

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 GhostPropG Σ :=
  { #[local] ghost_prop ۰ G ۰ ghost_var ۰ G :: GhostVarG Σ (▶ ∙)
  }.

Definition ghost_prop ۰ Σ :=
  #[ghost_var ۰ Σ (▶ ∙)
  ].
#[global] Instance subG ｰ ghost_prop ۰ Σ Σ :
  subG ghost_prop ۰ Σ Σ →
  GhostPropG Σ.

Section ghost_prop ۰ G.
  Context `{ghost_prop ۰ G : !GhostPropG Σ}.

  Implicit Type P : iProp Σ.

  Definition ghost_prop γ dq P :=
    ghost_var γ dq (Next P).

  #[global] Instance ghost_prop ｰ contractive γ dq :
    Contractive (ghost_prop γ dq).
  #[global] Instance ghost_prop ｰ proper γ dq :
    Proper ((≡) ==> (≡)) (ghost_prop γ dq).

  #[global] Instance ghost_prop ｰ persistent γ P :
    Persistent (ghost_prop γ DfracDiscarded P).

  #[global] Instance ghost_prop ｰ fractional γ P :
    Fractional (λ q, ghost_prop γ (DfracOwn q) P).
  #[global] Instance ghost_prop ｰ as_fractional γ P q :
    AsFractional (ghost_prop γ (DfracOwn q) P) (λ q, ghost_prop γ (DfracOwn q) P) q.

  Lemma ghost_prop ｰ alloc P :
    ⊢ |==>
      ∃ γ ,
      ghost_prop γ (DfracOwn 1) P.
  Lemma ghost_prop ｰ alloc ｰ cofinite (γs : gset gname) P :
    ⊢ |==>
      ∃ γ ,
      ⌜γ ∉ γs ⌝ ∗
      ghost_prop γ (DfracOwn 1) P.

  Lemma ghost_prop ｰ valid γ dq P :
    ghost_prop γ dq P ⊢
    ⌜✓ dq ⌝.
  Lemma ghost_prop ｰ combine γ dq1 P1 dq2 P2 :
    ghost_prop γ dq1 P1 -∗
    ghost_prop γ dq2 P2 -∗
      ▷ (P1 ≡ P2 ) ∗
      ghost_prop γ (dq1 ⋅ dq2) P1.
  Lemma ghost_prop ｰ valid ｰ2 γ dq1 P1 dq2 P2 :
    ghost_prop γ dq1 P1 -∗
    ghost_prop γ dq2 P2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ▷ (P1 ≡ P2 ).
  Lemma ghost_prop ｰ agree γ dq1 P1 dq2 P2 :
    ghost_prop γ dq1 P1 -∗
    ghost_prop γ dq2 P2 -∗
    ▷ (P1 ≡ P2 ).
  Lemma ghost_prop ｰ dfrac ｰ ne γ1 dq1 P1 γ2 dq2 P2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    ghost_prop γ1 dq1 P1 -∗
    ghost_prop γ2 dq2 P2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma ghost_prop ｰ ne γ1 P1 γ2 dq2 P2 :
    ghost_prop γ1 (DfracOwn 1) P1 -∗
    ghost_prop γ2 dq2 P2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma ghost_prop ｰ exclusive γ P1 dq2 P2 :
    ghost_prop γ (DfracOwn 1) P1 -∗
    ghost_prop γ dq2 P2 -∗
    False.
  Lemma ghost_prop ｰ persist γ dq P :
    ghost_prop γ dq P ⊢ |==>
    ghost_prop γ DfracDiscarded P.

  Lemma ghost_prop ｰ update {γ P} P' :
    ghost_prop γ (DfracOwn 1) P ⊢ |==>
    ghost_prop γ (DfracOwn 1) P'.
End ghost_prop ۰ G.

#[global] Opaque ghost_prop.