Library zoo.iris.algebra.lib.auth_monoi

From iris.algebra Require Import
  proofmode_classes.

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

#[local] Hint Resolve monopoi_principal_valid : core.

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

  Implicit Types 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.