Library zoo.iris.algebra.monopo

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

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo Require Import
  options.

Definition monopo `(R : relation A) : Type :=
  list A.

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

  Implicit Types a b c : A.
  Implicit Types x y z : monopo 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 (x ++ y) ↔
    below a x ∨ below a y.

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

  #[local] Instance monopo_equiv_equiv :
    Equivalence monopo_equiv.

  #[local] Lemma monopo_equiv_nil x :
    x ≡ [] →
    x = [].

  Canonical monopo_O :=
    discreteO (monopo R).

  #[local] Instance monopo_valid : Valid (monopo R) :=
    λ x,
      x ≠ [] →
        ∃ a,
        Forall (flip R a) x.
  #[local] Instance monopo_validN : ValidN (monopo R) :=
    λ _,
      valid.
  #[local] Program Instance monopo_op : Op (monopo R) :=
    λ x1 x2,
      x1 ++ x2.
  #[local] Instance monopo_pcore : PCore (monopo R) :=
    Some.

  #[local] Lemma monopo_cmra_mixin :
    CmraMixin (monopo R).
  Canonical monopo_R :=
    Cmra (monopo R) monopo_cmra_mixin.

  #[global] Instance monopo_cmra_total :
    CmraTotal monopo_R.
  #[global] Instance monopo_core_id x :
    CoreId x.

  #[global] Instance monopo_cmra_discrete :
    CmraDiscrete monopo_R.

  #[local] Instance monopo_unit : Unit (monopo R) :=
    nil.
  #[local] Lemma monopo_ucmra_mixin :
    UcmraMixin (monopo R).
  Canonical monopo_UR :=
    Ucmra (monopo R) monopo_ucmra_mixin.

  Lemma monopo_idemp x :
    x ⋅ x ≡ x.

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

  Definition monopo_principal a : monopo_UR :=
    [a].

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

  Lemma monopo_principal_R_opN_base n x y :
    ( ∀ b,
      b ∈ y →
        ∃ c,
        c ∈ x ∧
        R b c
    ) →
    y ⋅ x ≡{n}≡ x.
  Lemma monopo_principal_R_opN n a b :
    R a b →
    monopo_principal a ⋅ monopo_principal b ≡{n}≡ monopo_principal b.
  Lemma monopo_principal_R_op a b :
    R a b →
    monopo_principal a ⋅ monopo_principal b ≡ monopo_principal b.

  Lemma monopo_principal_opN_R n a b x :
    R a a →
    monopo_principal a ⋅ x ≡{n}≡ monopo_principal b →
    R a b.
  Lemma monopo_principal_op_R' a b x :
    R a a →
    monopo_principal a ⋅ x ≡ monopo_principal b →
    R a b.
  Lemma monopo_principal_op_R a b x :
    monopo_principal a ⋅ x ≡ monopo_principal b →
    R a b.

  Lemma monopo_principal_valid a :
    ✓ monopo_principal a.
  Lemma monopo_principal_op_valid a1 a2 :
    ✓ (monopo_principal a1 ⋅ monopo_principal a2) →
      ∃ a,
      R a1 a ∧
      R a2 a.

  Lemma monopo_principal_includedN n a b :
    monopo_principal a ≼{n} monopo_principal b ↔
    R a b.
  Lemma monopo_principal_included a b :
    monopo_principal a ≼ monopo_principal b ↔
    R a b.

  Lemma monopo_local_update_grow a x b:
    R a b →
    (monopo_principal a, x) ¬l~> (monopo_principal b, monopo_principal b).

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

#[global] Arguments monopo_R {_ _} _ {_ _} : assert.
#[global] Arguments monopo_UR {_ _} _ {_ _} : assert.
#[global] Arguments monopo_principal {_ _} _ {_ _} _ : assert.

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

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

  #[global] Instance monopo_principal_ne :
    (∀ n, Proper ((≡{n}≡) ==> (≡{n}≡) ==> (↔)) R) →
    NonExpansive (monopo_principal R).
  #[global] Instance monopo_principal_proper :
    Proper ((≡) ==> (≡) ==> (↔)) R →
    Proper ((≡) ==> (≡)) (monopo_principal R).

  Lemma monopo_principal_inj_related a b :
    monopo_principal R a ≡ monopo_principal R b →
    R a a →
    R a b.
  Lemma monopo_principal_inj_general a b :
    monopo_principal R a ≡ monopo_principal R b →
    R a a →
    R b b →
    (R a b → R b a → a ≡ b) →
    a ≡ b.

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

#[global] Opaque monopo_principal.