Library zoo.iris.base_logic.lib.ghost_var

From iris.algebra Require Import
  dfrac_agree.

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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.