Library zoo.iris.algebra.monopo

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

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

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

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

  Implicit Type a b c : A.
  Implicit Type 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 Type a b c : A.
  Implicit Type 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.