Library zoo.iris.base_logic.lib.auth_mono

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

Class AuthMonoG Σ {A : ofe} (R : relation A) :=
  { #[local] auth_mono ۰ G ۰ inG :: inG Σ (auth_mono ۰ UR R)
  }.

Definition auth_mono ۰ Σ {A : ofe} (R : relation A) :=
  #[GFunctor (auth_mono ۰ UR R)
  ].
#[global] Instance subG ｰ auth_mono ۰ Σ Σ {A : ofe} (R : relation A) :
  subG (auth_mono ۰ Σ R) Σ →
  AuthMonoG Σ R.

Section auth_mono ۰ G.
  Context {A : ofe} (R : relation A).
  Context `{auth_mono ۰ G : !AuthMonoG Σ R}.

  Implicit Type a : A.

  Notation Rs := (
    rtc R
  ).

  Definition auth_mono ۰ auth γ dq a :=
    own γ (auth_mono ۰ auth R dq a).
  Definition auth_mono ۰ lb γ a :=
    own γ (auth_mono ۰ lb R a).

  #[global] Instance auth_mono ۰ auth ｰ timeless γ dq a :
    Timeless (auth_mono ۰ auth γ dq a).
  #[global] Instance auth_mono ۰ lb ｰ timeless γ a :
    Timeless (auth_mono ۰ lb γ a).

  #[global] Instance auth_mono ۰ auth ｰ persistent γ a :
    Persistent (auth_mono ۰ auth γ DfracDiscarded a).
  #[global] Instance auth_mono ۰ lb ｰ persistent γ a :
    Persistent (auth_mono ۰ lb γ a).

  #[global] Instance auth_mono ۰ auth ｰ fractional γ a :
    Fractional (λ q, auth_mono ۰ auth γ (DfracOwn q) a).
  #[global] Instance auth_mono ۰ auth ｰ as_fractional γ q a :
    AsFractional (auth_mono ۰ auth γ (DfracOwn q) a) (λ q, auth_mono ۰ auth γ (DfracOwn q) a) q.

  Lemma auth_mono ｰ alloc a :
    ⊢ |==>
      ∃ γ ,
      auth_mono ۰ auth γ (DfracOwn 1) a.

  Lemma auth_mono ۰ auth ｰ valid γ dq a :
    auth_mono ۰ auth γ dq a ⊢
    ⌜✓ dq ⌝.
  Lemma auth_mono ۰ auth ｰ combine `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_mono ۰ auth γ dq1 a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
      ⌜a1 = a2 ⌝ ∗
      auth_mono ۰ auth γ (dq1 ⋅ dq2) a1.
  Lemma auth_mono ۰ auth ｰ valid ｰ2 `{!AntiSymm (≡) Rs} γ dq1 a1 dq2 a2 :
    auth_mono ۰ auth γ dq1 a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜a1 ≡ a2 ⌝.
  Lemma auth_mono ۰ auth ｰ valid ｰ2ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_mono ۰ auth γ dq1 a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜a1 = a2 ⌝.
  Lemma auth_mono ۰ auth ｰ agree `{!AntiSymm (≡) Rs} γ dq1 a1 dq2 a2 :
    auth_mono ۰ auth γ dq1 a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
    ⌜a1 ≡ a2 ⌝.
  Lemma auth_mono ۰ auth ｰ agree ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ dq1 a1 dq2 a2 :
    auth_mono ۰ auth γ dq1 a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
    ⌜a1 = a2 ⌝.
  Lemma auth_mono ۰ auth ｰ dfrac ｰ ne `{!AntiSymm (≡) Rs} γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    auth_mono ۰ auth γ1 dq1 a1 -∗
    auth_mono ۰ auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_mono ۰ auth ｰ dfrac ｰ ne ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ1 dq1 a1 γ2 dq2 a2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    auth_mono ۰ auth γ1 dq1 a1 -∗
    auth_mono ۰ auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_mono ۰ auth ｰ ne `{!AntiSymm (≡) Rs} γ1 a1 γ2 dq2 a2 :
    auth_mono ۰ auth γ1 (DfracOwn 1) a1 -∗
    auth_mono ۰ auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_mono ۰ auth ｰ ne ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ1 a1 γ2 dq2 a2 :
    auth_mono ۰ auth γ1 (DfracOwn 1) a1 -∗
    auth_mono ۰ auth γ2 dq2 a2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma auth_mono ۰ auth ｰ exclusive `{!AntiSymm (≡) Rs} γ a1 dq2 a2 :
    auth_mono ۰ auth γ (DfracOwn 1) a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
    False.
  Lemma auth_mono ۰ auth ｰ exclusive ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} γ a1 dq2 a2 :
    auth_mono ۰ auth γ (DfracOwn 1) a1 -∗
    auth_mono ۰ auth γ dq2 a2 -∗
    False.
  Lemma auth_mono ۰ auth ｰ persist γ dq a :
    auth_mono ۰ auth γ dq a ⊢ |==>
    auth_mono ۰ auth γ DfracDiscarded a.

  Lemma auth_mono ۰ lb ｰ mono {γ a} a' :
    Rs a' a →
    auth_mono ۰ lb γ a ⊢
    auth_mono ۰ lb γ a'.
  Lemma auth_mono ۰ lb ｰ mono' {γ a} a' :
    R a' a →
    auth_mono ۰ lb γ a ⊢
    auth_mono ۰ lb γ a'.

  Lemma auth_mono ۰ lb ｰ get γ q a :
    auth_mono ۰ auth γ q a ⊢
    auth_mono ۰ lb γ a.
  Lemma auth_mono ۰ lb ｰ get ｰ mono' γ q a a' :
    R a' a →
    auth_mono ۰ auth γ q a ⊢
    auth_mono ۰ lb γ a'.
  Lemma auth_mono ۰ lb ｰ get ｰ mono γ q a a' :
    Rs a' a →
    auth_mono ۰ auth γ q a ⊢
    auth_mono ۰ lb γ a'.

  Lemma auth_mono ۰ lb ｰ valid γ dq a a' :
    auth_mono ۰ auth γ dq a -∗
    auth_mono ۰ lb γ a' -∗
    ⌜Rs a' a ⌝.
  Lemma auth_mono ۰ lb ｰ agree γ a1 a2 :
    auth_mono ۰ lb γ a1 -∗
    auth_mono ۰ lb γ a2 -∗
      ∃ a ,
      ⌜Rs a1 a ⌝ ∧
      ⌜Rs a2 a ⌝.

  Lemma auth_mono ｰ update {γ a} a' :
    Rs a a' →
    auth_mono ۰ auth γ (DfracOwn 1) a ⊢ |==>
    auth_mono ۰ auth γ (DfracOwn 1) a'.
  Lemma auth_mono ｰ update' {γ a} a' :
    R a a' →
    auth_mono ۰ auth γ (DfracOwn 1) a ⊢ |==>
    auth_mono ۰ auth γ (DfracOwn 1) a'.
End auth_mono ۰ G.

#[global] Opaque auth_mono ۰ auth.
#[global] Opaque auth_mono ۰ lb.