Library zoo.iris.algebra.mono

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

Require Import zoo.prelude.
Require Import zoo.options.

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

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

  Implicit Type a b c : A.
  Implicit Type x y z : mono R.

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

  #[local] Lemma belowｰapp a x y :
    below a (x ++ y) ↔
    below a x ∨ below a y.

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

  #[local] Instance mono۰equivｰequiv :
    Equivalence mono۰equiv.

  Canonical mono۰O :=
    discreteO (mono R).

  #[local] Instance mono۰valid : Valid (mono R) :=
    λ x,
      True.
  #[local] Instance mono۰validN : ValidN (mono R) :=
    λ n x,
      True.
  #[local] Program Instance mono۰op : Op (mono R) :=
    λ x1 x2,
      x1 ++ x2.
  #[local] Instance mono۰pcore : PCore (mono R) :=
    Some.

  #[local] Lemma monoｰcmra_mixin :
    CmraMixin (mono R).
  Canonical mono۰R :=
    Cmra (mono R) monoｰcmra_mixin.

  #[global] Instance monoｰcmra_total :
    CmraTotal mono۰R.
  #[global] Instance monoｰcore_id x :
    CoreId x.

  #[global] Instance monoｰcmra_discrete :
    CmraDiscrete mono۰R.

  #[local] Instance mono۰unit : Unit (mono R) :=
    nil.
  #[local] Lemma monoｰucmra_mixin :
    UcmraMixin (mono R).
  Canonical mono۰UR :=
    Ucmra (mono R) monoｰucmra_mixin.

  Lemma monoｰidemp x :
    x ⋅ x ≡ x.

  Lemma monoｰincluded x y :
    x ≼ y ↔
    y ≡ x ⋅ y.

  Definition mono۰principal a : mono۰UR :=
    [a].

  #[local] Lemma belowｰprincipal a b :
    below a (mono۰principal b) ↔
    R a b.

  Lemma mono۰principalｰRｰopNｰbase `{!Transitive R} n x y :
    ( ∀ b,
      b ∈ y →
        ∃ c,
        c ∈ x ∧
        R b c
    ) →
    y ⋅ x ≡{n}≡ x.
  Lemma mono۰principalｰRｰopN `{!Transitive R} n a b :
    R a b →
    mono۰principal a ⋅ mono۰principal b ≡{n}≡ mono۰principal b.
  Lemma mono۰principalｰRｰop `{!Transitive R} a b :
    R a b →
    mono۰principal a ⋅ mono۰principal b ≡ mono۰principal b.

  Lemma mono۰principalｰopNｰR n a b x :
    R a a →
    mono۰principal a ⋅ x ≡{n}≡ mono۰principal b →
    R a b.
  Lemma mono۰principalｰopｰR' a b x :
    R a a →
    mono۰principal a ⋅ x ≡ mono۰principal b →
    R a b.
  Lemma mono۰principalｰopｰR `{!Reflexive R} a b x :
    mono۰principal a ⋅ x ≡ mono۰principal b →
    R a b.

  Lemma mono۰principalｰincludedN `{!Reflexive R} `{!Transitive R} n a b :
    mono۰principal a ≼{n} mono۰principal b ↔
    R a b.
  Lemma mono۰principalｰincluded `{!Reflexive R} `{!Transitive R} a b :
    mono۰principal a ≼ mono۰principal b ↔
    R a b.

  Lemma monoｰlocal_updateｰgrow `{!Transitive R} a x b:
    R a b →
    (mono۰principal a, x) ¬l~> (mono۰principal b, mono۰principal b).

  Lemma monoｰlocal_updateｰget_frag `{!Reflexive R} `{!Transitive R} a b:
    R b a →
    (mono۰principal a, ε) ¬l~> (mono۰principal a, mono۰principal b).
End relation.

#[global] Arguments mono۰R {_ _} _ : assert.
#[global] Arguments mono۰UR {_ _} _ : assert.
#[global] Arguments mono۰principal {_ _} _ _ : assert.

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

  Implicit Type a b c : A.
  Implicit Type x y z : mono R.

  #[global] Instance mono۰principalｰne :
    (∀ n, Proper ((≡{n}≡) ==> (≡{n}≡) ==> (↔)) R) →
    NonExpansive (mono۰principal R).
  #[global] Instance mono۰principalｰproper :
    Proper ((≡) ==> (≡) ==> (↔)) R →
    Proper ((≡) ==> (≡)) (mono۰principal R).

  Lemma mono۰principalｰinjｰrelated a b :
    mono۰principal R a ≡ mono۰principal R b →
    R a a →
    R a b.
  Lemma mono۰principalｰinjｰgeneral a b :
    mono۰principal R a ≡ mono۰principal R b →
    R a a →
    R b b →
    (R a b → R b a → a ≡ b) →
    a ≡ b.

  #[global] Instance mono۰principalｰinj `{!Reflexive R} `{!AntiSymm (≡) R} :
    Inj (≡) (≡) (mono۰principal R).
  #[global] Instance mono۰principalｰinj' `{!Reflexive R} `{!AntiSymm (≡) R} n :
    Inj (≡{n}≡) (≡{n}≡) (mono۰principal R).
End ofe_relation.

#[global] Opaque mono۰principal.