Library zoo.iris.algebra.lib.auth_monoi

Require Import iris.algebra.proofmode_classes.

Require Import zoo.prelude.
Require Export zoo.common.relations.
Require Export zoo.iris.algebra.base.
Require Import zoo.iris.algebra.auth.
Require Import zoo.iris.algebra.monopoi.
Require Import zoo.options.

#[local] Hint Resolve monopoi۰principalｰvalid : core.

Section relation.
  Context {SI : sidx}.
  Context {A : ofe} (R : relation A).
  Context `{!Initial R}.

  Implicit Type a b : A.

  Notation Rs := (
    rtc R
  ).

  #[local] Instance Rs ｰ antisymm `{!AntiSymm (=) Rs} :
    AntiSymm (≡) Rs.

  Definition auth_monoi :=
    auth (monopoi Rs).
  Definition auth_monoi ۰ R :=
    authR (monopoi ۰ UR Rs).
  Definition auth_monoi ۰ UR :=
    authUR (monopoi ۰ UR Rs).

  Definition auth_monoi ۰ auth dq a : auth_monoi ۰ UR :=
    ●{dq } monopoi ۰ principal Rs a ⋅ ◯ monopoi ۰ principal Rs a.
  Definition auth_monoi ۰ lb a : auth_monoi ۰ UR :=
    ◯ monopoi ۰ principal Rs a.

  #[global] Instance auth_monoi ۰ auth ｰ inj `{!AntiSymm (≡) Rs} :
    Inj2 (=) (≡) (≡) auth_monoi ۰ auth
  | 10.
  #[global] Instance auth_monoi ۰ auth ｰ inj ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} :
    Inj2 (=) (=) (≡) auth_monoi ۰ auth
  | 9.
  #[global] Instance auth_monoi ۰ lb ｰ inj `{!AntiSymm (≡) Rs} :
    Inj (≡) (≡) auth_monoi ۰ lb
  | 10.
  #[global] Instance auth_monoi ۰ lb ｰ inj ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} :
    Inj (=) (≡) auth_monoi ۰ lb
  | 9.

  #[global] Instance auth_monoi ｰ cmra_discrete :
    CmraDiscrete auth_monoi ۰ R.

  #[global] Instance auth_monoi ۰ auth ｰ core_id a :
    CoreId (auth_monoi ۰ auth DfracDiscarded a).
  #[global] Instance auth_monoi ۰ lb ｰ core_id a :
    CoreId (auth_monoi ۰ lb a).

  Lemma auth_monoi ۰ auth ｰ dfrac ｰ op dq1 dq2 a :
    auth_monoi ۰ auth (dq1 ⋅ dq2) a ≡ auth_monoi ۰ auth dq1 a ⋅ auth_monoi ۰ auth dq2 a.
  #[global] Instance auth_monoi ۰ auth ｰ dfrac ｰ is_op dq dq1 dq2 a :
    IsOp dq dq1 dq2 →
    IsOp' (auth_monoi ۰ auth dq a) (auth_monoi ۰ auth dq1 a) (auth_monoi ۰ auth dq2 a).

  Lemma auth_monoi ۰ lb ｰ op a a' :
    Rs a a' →
    auth_monoi ۰ lb a' ≡ auth_monoi ۰ lb a ⋅ auth_monoi ۰ lb a'.

  Lemma auth_monoi ۰ auth ｰ lb ｰ op dq a :
    auth_monoi ۰ auth dq a ≡ auth_monoi ۰ auth dq a ⋅ auth_monoi ۰ lb a.

  Lemma auth_monoi ۰ auth ｰ dfrac ｰ valid dq a :
    ✓ auth_monoi ۰ auth dq a ↔
    ✓ dq.
  Lemma auth_monoi ۰ auth ｰ valid a :
    ✓ auth_monoi ۰ auth (DfracOwn 1) a.

  Lemma auth_monoi ۰ auth ｰ dfrac ｰ op ｰ valid `{!AntiSymm (≡) Rs} dq1 a1 dq2 a2 :
    ✓ (auth_monoi ۰ auth dq1 a1 ⋅ auth_monoi ۰ auth dq2 a2 ) →
      ✓ (dq1 ⋅ dq2 ) ∧
      a1 ≡ a2.
  Lemma auth_monoi ۰ auth ｰ dfrac ｰ op ｰ valid ｰ 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 ｰ op ｰ valid `{!AntiSymm (≡) Rs} a1 a2 :
    ✓ (auth_monoi ۰ auth (DfracOwn 1) a1 ⋅ auth_monoi ۰ auth (DfracOwn 1) a2 ) →
    False.
  Lemma auth_monoi ۰ auth ｰ op ｰ valid ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} a1 a2 :
    ✓ (auth_monoi ۰ auth (DfracOwn 1) a1 ⋅ auth_monoi ۰ auth (DfracOwn 1) a2 ) ↔
    False.

  Lemma auth_monoi ۰ lb ｰ op ｰ valid a1 a2 :
    ✓ (auth_monoi ۰ lb a1 ⋅ auth_monoi ۰ lb a2 ) →
      ∃ a,
      Rs a1 a ∧
      Rs a2 a.

  Lemma auth_monoi ｰ both ｰ dfrac ｰ valid dq a b :
    ✓ (auth_monoi ۰ auth dq a ⋅ auth_monoi ۰ lb b ) ↔
      ✓ dq ∧
      Rs b a.
  Lemma auth_monoi ｰ both ｰ valid a b :
    ✓ (auth_monoi ۰ auth (DfracOwn 1) a ⋅ auth_monoi ۰ lb b ) ↔
    Rs b a.

  Lemma auth_monoi ۰ lb ｰ mono a1 a2 :
    Rs a1 a2 →
    auth_monoi ۰ lb a1 ≼ auth_monoi ۰ lb a2.

  Lemma auth_monoi ۰ auth ｰ dfrac ｰ included `{!AntiSymm (≡) Rs} dq1 a1 dq2 a2 :
    auth_monoi ۰ auth dq1 a1 ≼ auth_monoi ۰ auth dq2 a2 →
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧
      a1 ≡ a2.
  Lemma auth_monoi ۰ auth ｰ dfrac ｰ included ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} dq1 a1 dq2 a2 :
    auth_monoi ۰ auth dq1 a1 ≼ auth_monoi ۰ auth dq2 a2 ↔
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧
      a1 = a2.
  Lemma auth_monoi ۰ auth ｰ included `{!AntiSymm (≡) Rs} a1 a2 :
    auth_monoi ۰ auth (DfracOwn 1) a1 ≼ auth_monoi ۰ auth (DfracOwn 1) a2 →
    a1 ≡ a2.
  Lemma auth_monoi ۰ auth ｰ included ｰ L `{!LeibnizEquiv A} `{!AntiSymm (=) Rs} a1 a2 :
    auth_monoi ۰ auth (DfracOwn 1) a1 ≼ auth_monoi ۰ auth (DfracOwn 1) a2 ↔
    a1 = a2.

  Lemma auth_monoi ۰ lb ｰ included a1 dq a2 :
    auth_monoi ۰ lb a1 ≼ auth_monoi ۰ auth dq a2 ↔
    Rs a1 a2.
  Lemma auth_monoi ۰ lb ｰ included' a dq :
    auth_monoi ۰ lb a ≼ auth_monoi ۰ auth dq a.

  Lemma auth_monoi ۰ auth ｰ persist dq a :
    auth_monoi ۰ auth dq a ~~> auth_monoi ۰ auth DfracDiscarded a.
  Lemma auth_monoi ۰ auth ｰ update {a} a' :
    Rs a a' →
    auth_monoi ۰ auth (DfracOwn 1) a ~~> auth_monoi ۰ auth (DfracOwn 1) a'.

  Lemma auth_monoi ۰ auth ｰ local_update a a' :
    Rs a a' →
    (auth_monoi ۰ auth (DfracOwn 1) a , auth_monoi ۰ auth (DfracOwn 1) a ) ¬l ~>
    (auth_monoi ۰ auth (DfracOwn 1) a', auth_monoi ۰ auth (DfracOwn 1) a').
End relation.

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