Library zoo.iris.base_logic.lib.auth_monoi

Require Import zoo.prelude.
Require Export zoo.common.relations.
Require Import zoo.iris.algebra.lib.auth_monoi.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.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 Type 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.