Library zoo.iris.base_logic.lib.excl

Require Import iris.algebra.excl.

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

Class ExclG Σ F :=
  { #[local] excl۰G۰inG :: inG Σ (exclR $ oFunctor_apply F $ iPropO Σ)
  }.

Definition excl۰Σ F `{!oFunctorContractive F} :=
  #[GFunctor (exclRF F)
  ].
#[global] Instance subGｰexcl۰Σ Σ F `{!oFunctorContractive F} :
  subG (excl۰Σ F) Σ →
  ExclG Σ F.

Section excl۰G.
  Context `{excl۰G : !ExclG Σ F}.

  Definition excl γ a :=
    own γ (Excl a).

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

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

  Lemma exclｰalloc a :
    ⊢ |==>
      ∃ γ,
      excl γ a.

  Lemma exclｰexclusive γ a1 a2 :
    excl γ a1 -∗
    excl γ a2 -∗
    False.

  Lemma exclｰupdate γ a b :
    excl γ a ⊢ |==>
    excl γ b.
End excl۰G.

#[global] Opaque excl.