Library zoo.iris.algebra.lib.auth_mono

From iris.algebra Require Import
  proofmode_classes.

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

#[local] Hint Resolve monopo_principal_valid : core.

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

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