Library zoo.iris.algebra.monopoi

From iris.algebra Require Export
  cmra.
From iris.algebra Require Import
  local_updates.

From zoo Require Import
  prelude.
From zoo.common Require Import
  listne.
From zoo.common Require Export
  relations.
From zoo Require Import
  options.

Definition monopoi `(R : relation A) : Type :=
  listne A.

Section relation.
  Context {SI : sidx}.
  Context `{R : relation A}.
  Context `{!Reflexive R} `{!Transitive R}.
  Context `{!Initial R}.

  Implicit Types a b c : A.
  Implicit Types x y z : monopoi R.

  #[local] Definition below a x :=
    ∃ b,
    b ∈ x ∧
    R a b.

  #[local] Lemma below_elem_of a x :
    a ∈ x →
    below a x.
  #[local] Lemma below_app a x y :
    below a (listne_app x y) ↔
    below a x ∨ below a y.

  #[local] Instance monopoi_equiv : Equiv (monopoi R) :=
    λ x y,
      ∀ a,
      below a x ↔
      below a y.

  #[local] Instance monopoi_equiv_equiv :
    Equivalence monopoi_equiv.

  Canonical monopoi_O :=
    discreteO (monopoi R).

  #[local] Instance monopoi_valid : Valid (monopoi R) :=
    λ x,
      ∃ a,
      listne_Forall (flip R a) x.
  #[local] Instance monopoi_validN : ValidN (monopoi R) :=
    λ _,
      valid.
  #[local] Instance monopoi_op : Op (monopoi R) :=
    λ x1 x2,
      listne_app x1 x2.
  #[local] Instance monopoi_pcore : PCore (monopoi R) :=
    Some.

  #[local] Lemma monopoi_cmra_mixin :
    CmraMixin (monopoi R).
  Canonical monopoi_R :=
    Cmra (monopoi R) monopoi_cmra_mixin.

  #[global] Instance monopoi_cmra_total :
    CmraTotal monopoi_R.
  #[global] Instance monopoi_core_id x :
    CoreId x.

  #[global] Instance monopoi_cmra_discrete :
    CmraDiscrete monopoi_R.

  #[local] Program Definition principal a : monopoi R :=
    [a].

  #[local] Instance monopoi_unit : Unit (monopoi R) :=
    principal initial.
  #[local] Lemma monopoi_ucmra_mixin :
    UcmraMixin (monopoi R).
  Canonical monopoi_UR :=
    Ucmra (monopoi R) monopoi_ucmra_mixin.

  Lemma monopoi_idemp x :
    x ⋅ x ≡ x.

  Lemma monopoi_included x y :
    x ≼ y ↔
    y ≡ x ⋅ y.

  Definition monopoi_principal : A → monopoi_UR :=
    principal.

  #[local] Lemma below_principal a b :
    below a (monopoi_principal b) ↔
    R a b.

  Lemma monopoi_principal_R_opN_base n x y :
    ( ∀ b,
      b ∈ y →
        ∃ c,
        c ∈ x ∧
        R b c
    ) →
    y ⋅ x ≡{n}≡ x.
  Lemma monopoi_principal_R_opN n a b :
    R a b →
    monopoi_principal a ⋅ monopoi_principal b ≡{n}≡ monopoi_principal b.
  Lemma monopoi_principal_R_op a b :
    R a b →
    monopoi_principal a ⋅ monopoi_principal b ≡ monopoi_principal b.

  Lemma monopoi_principal_opN_R n a b x :
    R a a →
    monopoi_principal a ⋅ x ≡{n}≡ monopoi_principal b →
    R a b.
  Lemma monopoi_principal_op_R' a b x :
    R a a →
    monopoi_principal a ⋅ x ≡ monopoi_principal b →
    R a b.
  Lemma monopoi_principal_op_R a b x :
    monopoi_principal a ⋅ x ≡ monopoi_principal b →
    R a b.

  Lemma monopoi_principal_valid a :
    ✓ monopoi_principal a.
  Lemma monopoi_principal_op_valid a1 a2 :
    ✓ (monopoi_principal a1 ⋅ monopoi_principal a2) →
      ∃ a,
      R a1 a ∧
      R a2 a.

  Lemma monopoi_principal_includedN n a b :
    monopoi_principal a ≼{n} monopoi_principal b ↔
    R a b.
  Lemma monopoi_principal_included a b :
    monopoi_principal a ≼ monopoi_principal b ↔
    R a b.

  Lemma monopoi_local_update_grow a x b:
    R a b →
    (monopoi_principal a, x) ¬l~> (monopoi_principal b, monopoi_principal b).

  Lemma monopoi_local_update_get_frag a b:
    R b a →
    (monopoi_principal a, ε) ¬l~> (monopoi_principal a, monopoi_principal b).
End relation.

#[global] Arguments monopoi_R {_ _} _ {_ _ _} : assert.
#[global] Arguments monopoi_UR {_ _} _ {_ _ _} : assert.
#[global] Arguments monopoi_principal {_ _} _ {_ _ _} _ : assert.

Section ofe_relation.
  Context {SI : sidx}.
  Context {A : ofe} {R : relation A}.
  Context `{!Reflexive R} `{!Transitive R}.
  Context `{!Initial R}.

  Implicit Types a b c : A.
  Implicit Types x y z : monopoi R.

  #[global] Instance monopoi_principal_ne :
    (∀ n, Proper ((≡{n}≡) ==> (≡{n}≡) ==> (↔)) R) →
    NonExpansive (monopoi_principal R).
  #[global] Instance monopoi_principal_proper :
    Proper ((≡) ==> (≡) ==> (↔)) R →
    Proper ((≡) ==> (≡)) (monopoi_principal R).

  Lemma monopoi_principal_inj_related a b :
    monopoi_principal R a ≡ monopoi_principal R b →
    R a a →
    R a b.
  Lemma monopoi_principal_inj_general a b :
    monopoi_principal R a ≡ monopoi_principal R b →
    R a a →
    R b b →
    (R a b → R b a → a ≡ b) →
    a ≡ b.

  #[global] Instance monopoi_principal_inj `{!AntiSymm (≡) R} :
    Inj (≡) (≡) (monopoi_principal R).
  #[global] Instance monopoi_principal_inj' `{!AntiSymm (≡) R} n :
    Inj (≡{n}≡) (≡{n}≡) (monopoi_principal R).
End ofe_relation.

#[global] Opaque monopoi_principal.