Library zoo.iris.base_logic.lib.saved_prop

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

Class SavedPropG Σ :=
  { #[local] saved_prop۰G :: AgreeG Σ (▶ ∙)
  }.

Definition saved_prop۰Σ :=
  #[agree۰Σ (▶ ∙)
  ].
#[global] Instance subGｰsaved_prop۰Σ Σ :
  subG saved_prop۰Σ Σ →
  SavedPropG Σ.

Section saved_prop۰G.
  Context `{saved_prop۰G : !SavedPropG Σ}.

  Implicit Type P : iProp Σ.

  Definition saved_prop γ P :=
    agree۰on γ (Next P).

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

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

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

  Lemma saved_propｰagree γ P1 P2 :
    saved_prop γ P1 -∗
    saved_prop γ P2 -∗
    ▷ (P1 ≡ P2).
End saved_prop۰G.

#[global] Opaque saved_prop.