Library zoo.iris.algebra.mono

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

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

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

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

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