Library zoo.iris.base_logic.lib.agree

From iris.algebra Require Import
  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 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.