Library zoo.iris.base_logic.lib.ghost_var

Require Import iris.algebra.lib.dfrac_agree.

Require Import zoo.prelude.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class GhostVarG Σ F :=
  { #[local] ghost_var۰G۰inG :: inG Σ (dfrac_agreeR $ oFunctor_apply F $ iPropO Σ)
  }.

Definition ghost_var۰Σ F `{!oFunctorContractive F} :=
  #[GFunctor (dfrac_agreeRF F)
  ].
#[global] Instance subGｰghost_var۰Σ Σ F `{!oFunctorContractive F} :
  subG (ghost_var۰Σ F) Σ →
  GhostVarG Σ F.

Section ghost_var۰G.
  Context `{ghost_var۰G : !GhostVarG Σ F}.

  Definition ghost_var γ dq a :=
    own γ (to_dfrac_agree dq a).

  #[global] Instance ghost_varｰnonexpansive γ dq :
    NonExpansive (ghost_var γ dq).
  #[global] Instance ghost_varｰproper γ dq :
    Proper ((≡) ==> (≡)) (ghost_var γ dq).

  #[global] Instance ghost_varｰtimeless γ dq a :
    Discrete a →
    Timeless (ghost_var γ dq a).

  #[global] Instance ghost_varｰpersistent γ a :
    Persistent (ghost_var γ DfracDiscarded a).

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

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

  Lemma ghost_varｰvalid γ dq a :
    ghost_var γ dq a ⊢
    ⌜✓ dq⌝.
  Lemma ghost_varｰcombine γ dq1 a1 dq2 a2 :
    ghost_var γ dq1 a1 -∗
    ghost_var γ dq2 a2 -∗
      a1 ≡ a2 ∗
      ghost_var γ (dq1 ⋅ dq2) a1.
  Lemma ghost_varｰvalidｰ2 γ dq1 a1 dq2 a2 :
    ghost_var γ dq1 a1 -∗
    ghost_var γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      a1 ≡ a2.
  Lemma ghost_varｰagree γ dq1 a1 dq2 a2 :
    ghost_var γ dq1 a1 -∗
    ghost_var γ dq2 a2 -∗
    a1 ≡ a2.
  Lemma ghost_varｰdfracｰne γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    ghost_var γ1 dq1 a1 -∗
    ghost_var γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma ghost_varｰne γ1 a1 γ2 dq2 a2 :
    ghost_var γ1 (DfracOwn 1) a1 -∗
    ghost_var γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma ghost_varｰexclusive γ a1 dq2 a2 :
    ghost_var γ (DfracOwn 1) a1 -∗
    ghost_var γ dq2 a2 -∗
    False.
  Lemma ghost_varｰpersist γ dq a :
    ghost_var γ dq a ⊢ |==>
    ghost_var γ DfracDiscarded a.
  Section discrete.
    Context `{!OfeDiscrete $ oFunctor_apply F $ iPropO Σ}.
    Lemma ghost_varｰcombineｰdiscrete γ dq1 a1 dq2 a2 :
      ghost_var γ dq1 a1 -∗
      ghost_var γ dq2 a2 -∗
        ⌜a1 ≡ a2⌝ ∗
        ghost_var γ (dq1 ⋅ dq2) a1.
    Lemma ghost_varｰvalidｰ2ｰdiscrete γ dq1 a1 dq2 a2 :
      ghost_var γ dq1 a1 -∗
      ghost_var γ dq2 a2 -∗
        ⌜✓ (dq1 ⋅ dq2)⌝ ∗
        ⌜a1 ≡ a2⌝.
    Lemma ghost_varｰagreeｰdiscrete γ dq1 a1 dq2 a2 :
      ghost_var γ dq1 a1 -∗
      ghost_var γ dq2 a2 -∗
      ⌜a1 ≡ a2⌝.
    Section leibniz_equiv.
      Context `{!LeibnizEquiv $ oFunctor_apply F $ iPropO Σ}.
      Lemma ghost_varｰcombineｰL γ dq1 a1 dq2 a2 :
        ghost_var γ dq1 a1 -∗
        ghost_var γ dq2 a2 -∗
          ⌜a1 = a2⌝ ∗
          ghost_var γ (dq1 ⋅ dq2) a1.
      Lemma ghost_varｰvalidｰ2ｰL γ dq1 a1 dq2 a2 :
        ghost_var γ dq1 a1 -∗
        ghost_var γ dq2 a2 -∗
          ⌜✓ (dq1 ⋅ dq2)⌝ ∗
          ⌜a1 = a2⌝.
      Lemma ghost_varｰagreeｰL γ dq1 a1 dq2 a2 :
        ghost_var γ dq1 a1 -∗
        ghost_var γ dq2 a2 -∗
        ⌜a1 = a2⌝.
    End leibniz_equiv.
  End discrete.

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

#[global] Opaque ghost_var.