Library zoo.iris.base_logic.lib.saved_pred

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

Class SavedPredG Σ A :=
  { #[local] saved_pred_G :: AgreeG Σ (A -d> ▶ ∙)
  }.

Definition saved_pred_Σ A :=
  #[agree_Σ (A -d> ▶ ∙)
  ].
#[global] Instance subG_saved_pred_Σ Σ A :
  subG (saved_pred_Σ A) Σ →
  SavedPredG Σ A.

Section saved_pred_G.
  Context `{saved_pred_G : !SavedPredG Σ A}.

  Implicit Types Ψ : A → iProp Σ.

  Definition saved_pred γ Ψ :=
    agree_on γ (Next ∘ Ψ).

  #[global] Instance saved_pred_contractive γ n :
    Proper ((pointwise_relation _ (dist_later n)) ==> (≡{n}≡)) (saved_pred γ).
  #[global] Instance saved_pred_proper γ :
    Proper ((≡) ==> (≡)) (saved_pred γ : (A -d> iProp Σ) → _).

  #[global] Instance saved_pred_persistent γ Ψ :
    Persistent (saved_pred γ Ψ).

  Lemma saved_pred_alloc Ψ :
    ⊢ |==>
      ∃ γ,
      saved_pred γ Ψ.
  Lemma saved_pred_alloc_cofinite (γs : gset gname) Ψ :
    ⊢ |==>
      ∃ γ,
      ⌜γ ∉ γs⌝ ∗
      saved_pred γ Ψ.

  Lemma saved_pred_agree {γ Ψ1 Ψ2} x :
    saved_pred γ Ψ1 -∗
    saved_pred γ Ψ2 -∗
    ▷ (Ψ1 x ≡ Ψ2 x).
End saved_pred_G.

#[global] Opaque saved_pred.