Library zoo.iris.base_logic.lib.agree

Require Import iris.algebra.agree.

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

Class AgreeG Σ F :=
  { #[local] agree۰G۰inG :: inG Σ (agreeR $ oFunctor_apply F $ iPropO Σ)
  }.

Definition agree۰Σ F `{!oFunctorContractive F} :=
  #[GFunctor (agreeRF F)
  ].
#[global] Instance subGｰagree۰Σ Σ F `{!oFunctorContractive F} :
  subG (agree۰Σ F) Σ →
  AgreeG Σ F.

Section agree۰G.
  Context `{agree۰G : !AgreeG Σ F}.

  Definition agree۰on γ a :=
    own γ (to_agree a).

  #[global] Instance agree۰onｰne γ :
    NonExpansive (agree۰on γ).
  #[global] Instance agree۰onｰproper γ :
    Proper ((≡) ==> (≡)) (agree۰on γ).

  #[global] Instance agree۰onｰtimeless γ a :
    Discrete a →
    Timeless (agree۰on γ a).

  #[global] Instance agree۰onｰpersistent γ a :
    Persistent (agree۰on γ a).

  Lemma agreeｰalloc a :
    ⊢ |==>
      ∃ γ,
      agree۰on γ a.
  Lemma agreeｰallocｰcofinite (γs : gset gname) a :
    ⊢ |==>
      ∃ γ,
      ⌜γ ∉ γs⌝ ∗
      agree۰on γ a.

  Lemma agree۰onｰagree γ a1 a2 :
    agree۰on γ a1 -∗
    agree۰on γ a2 -∗
    a1 ≡ a2.
  Section discrete.
    Context `{!OfeDiscrete $ oFunctor_apply F $ iPropO Σ}.
    Lemma agree۰onｰagreeｰdiscrete γ a1 a2 :
      agree۰on γ a1 -∗
      agree۰on γ a2 -∗
      ⌜a1 ≡ a2⌝.
    Lemma agree۰onｰagreeｰL `{!LeibnizEquiv $ oFunctor_apply F $ iPropO Σ} γ a1 a2 :
      agree۰on γ a1 -∗
      agree۰on γ a2 -∗
      ⌜a1 = a2⌝.
  End discrete.
End agree۰G.

#[global] Opaque agree۰on.