Library zoo.iris.base_logic.lib.auth_monoi

From zoo Require Import
  prelude.
From zoo.common Require Export
  relations.
From zoo.iris.algebra Require Import
  lib.auth_monoi.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  options.

Class AuthMonoiG Σ {A : ofe} (R : relation A) `{!Initial R} :=
  { #[local] auth_monoi_G_inG :: inG Σ (auth_monoi_UR R)
  }.

Definition auth_monoi_Σ {A : ofe} (R : relation A) `{!Initial R} :=
  #[GFunctor (auth_monoi_UR R)
  ].
#[global] Instance subG_auth_monoi_Σ Σ {A : ofe} (R : relation A) `{!Initial R} :
  subG (auth_monoi_Σ R) Σ →
  AuthMonoiG Σ R.

Section auth_monoi_G.
  Context {A : ofe} (R : relation A) `{!Initial R}.
  Context `{auth_monoi_G : !AuthMonoiG Σ R}.

  Implicit Types a : A.

  Notation Rs := (
    rtc R
  ).

  Definition auth_monoi_auth γ dq a :=
    own γ (auth_monoi_auth R dq a).
  Definition auth_monoi_lb γ a :=
    own γ (auth_monoi_lb R a).

  #[global] Instance auth_monoi_auth_timeless γ dq a :
    Timeless (auth_monoi_auth γ dq a).
  #[global] Instance auth_monoi_lb_timeless γ a :
    Timeless (auth_monoi_lb γ a).

  #[global] Instance auth_monoi_auth_persistent γ a :
    Persistent (auth_monoi_auth γ DfracDiscarded a).
  #[global] Instance auth_monoi_lb_persistent γ a :
    Persistent (auth_monoi_lb γ a).

  #[global] Instance auth_monoi_auth_fractional γ a :
    Fractional (λ q, auth_monoi_auth γ (DfracOwn q) a).
  #[global] Instance auth_monoi_auth_as_fractional γ q a :
    AsFractional (auth_monoi_auth γ (DfracOwn q) a) (λ q, auth_monoi_auth γ (DfracOwn q) a) q.

  Lemma auth_monoi_alloc a :
    ⊢ |==>
      ∃ γ,
      auth_monoi_auth γ (DfracOwn 1) a.

  Lemma auth_monoi_auth_valid γ dq a :
    auth_monoi_auth γ dq a ⊢
    ⌜✓ dq⌝.
  Lemma auth_monoi_auth_combine `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_monoi_auth γ dq1 a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
      ⌜a1 = a2⌝ ∗
      auth_monoi_auth γ (dq1 ⋅ dq2) a1.
  Lemma auth_monoi_auth_valid_2 `{!AntiSymm (≡) Rs} γ dq1 a1 dq2 a2 :
    auth_monoi_auth γ dq1 a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜a1 ≡ a2⌝.
  Lemma auth_monoi_auth_valid_2_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_monoi_auth γ dq1 a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜a1 = a2⌝.
  Lemma auth_monoi_auth_agree `{!AntiSymm (≡) Rs} γ dq1 a1 dq2 a2 :
    auth_monoi_auth γ dq1 a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
    ⌜a1 ≡ a2⌝.
  Lemma auth_monoi_auth_agree_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_monoi_auth γ dq1 a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
    ⌜a1 = a2⌝.
  Lemma auth_monoi_auth_dfrac_ne `{!AntiSymm (≡) Rs} γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    auth_monoi_auth γ1 dq1 a1 -∗
    auth_monoi_auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_monoi_auth_dfrac_ne_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    auth_monoi_auth γ1 dq1 a1 -∗
    auth_monoi_auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_monoi_auth_ne `{!AntiSymm (≡) Rs} γ1 a1 γ2 dq2 a2 :
    auth_monoi_auth γ1 (DfracOwn 1) a1 -∗
    auth_monoi_auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_monoi_auth_ne_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ1 a1 γ2 dq2 a2 :
    auth_monoi_auth γ1 (DfracOwn 1) a1 -∗
    auth_monoi_auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2⌝.
  Lemma auth_monoi_auth_exclusive `{!AntiSymm (≡) Rs} γ a1 dq2 a2 :
    auth_monoi_auth γ (DfracOwn 1) a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
    False.
  Lemma auth_monoi_auth_exclusive_L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ a1 dq2 a2 :
    auth_monoi_auth γ (DfracOwn 1) a1 -∗
    auth_monoi_auth γ dq2 a2 -∗
    False.
  Lemma auth_monoi_auth_persist γ dq a :
    auth_monoi_auth γ dq a ⊢ |==>
    auth_monoi_auth γ DfracDiscarded a.

  Lemma auth_monoi_lb_initial γ :
    ⊢ |==>
      auth_monoi_lb γ initial.
  Lemma auth_monoi_lb_mono {γ a} a' :
    Rs a' a →
    auth_monoi_lb γ a ⊢
    auth_monoi_lb γ a'.
  Lemma auth_monoi_lb_mono' {γ a} a' :
    R a' a →
    auth_monoi_lb γ a ⊢
    auth_monoi_lb γ a'.

  Lemma auth_monoi_lb_get γ q a :
    auth_monoi_auth γ q a ⊢
    auth_monoi_lb γ a.
  Lemma auth_monoi_lb_get_mono' γ q a a' :
    R a' a →
    auth_monoi_auth γ q a ⊢
    auth_monoi_lb γ a'.
  Lemma auth_monoi_lb_get_mono γ q a a' :
    Rs a' a →
    auth_monoi_auth γ q a ⊢
    auth_monoi_lb γ a'.

  Lemma auth_monoi_lb_valid γ dq a a' :
    auth_monoi_auth γ dq a -∗
    auth_monoi_lb γ a' -∗
    ⌜Rs a' a⌝.
  Lemma auth_monoi_lb_agree γ a1 a2 :
    auth_monoi_lb γ a1 -∗
    auth_monoi_lb γ a2 -∗
      ∃ a,
      ⌜Rs a1 a⌝ ∧
      ⌜Rs a2 a⌝.

  Lemma auth_monoi_update {γ a} a' :
    Rs a a' →
    auth_monoi_auth γ (DfracOwn 1) a ⊢ |==>
    auth_monoi_auth γ (DfracOwn 1) a'.
  Lemma auth_monoi_update' {γ a} a' :
    R a a' →
    auth_monoi_auth γ (DfracOwn 1) a ⊢ |==>
    auth_monoi_auth γ (DfracOwn 1) a'.
End auth_monoi_G.

#[global] Opaque auth_monoi_auth.
#[global] Opaque auth_monoi_lb.