Library zoo.iris.algebra.monopoi

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

Require Import zoo.prelude.
Require Import zoo.common.listne.
Require Export zoo.common.relations.
Require Import zoo.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 Type a b c : A.
  Implicit Type 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 Type a b c : A.
  Implicit Type 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.