Library zoo.iris.algebra.lib.auth_mono

Require Import iris.algebra.proofmode_classes.

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

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

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

  Implicit Type a b : A.

  Notation Rs := (
    rtc R
  ).

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

  Definition auth_mono :=
    auth (monopo Rs).
  Definition auth_mono ۰ R :=
    authR (monopo ۰ UR Rs).
  Definition auth_mono ۰ UR :=
    authUR (monopo ۰ UR Rs).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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