Library zoo.iris.base_logic.lib.excl

From iris.algebra Require Import
  excl.

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 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.