Library zoo.iris.base_logic.lib.auth_mono

From zoo Require Import
  prelude.
From zoo.iris.algebra Require Import
  lib.auth_mono.
From zoo.iris.base_logic Require Export
  lib.base.
From zoo.iris Require Import
  diaframe.
From zoo Require Import
  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 Types 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.