Library zoo.iris.base_logic.lib.mono_list

Require Import zoo.prelude.
Require Import zoo.common.relations.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class MonoListG Σ A :=
  { #[local] mono_list ۰ G ۰ mono ۰ G :: AuthMonoG Σ (A := leibnizO (list A)) prefix
  }.

Definition mono_list ۰ Σ A :=
  #[auth_mono ۰ Σ (A := leibnizO (list A)) prefix
  ].
#[global] Instance subG ｰ mono_list ۰ Σ Σ A :
  subG (mono_list ۰ Σ A) Σ →
  MonoListG Σ A.

Section mono_list ۰ G.
  Context `{mono_list ۰ G : !MonoListG Σ A}.

  Implicit Type i : nat.
  Implicit Type a : A.
  Implicit Type l : list A.

  Definition mono_list ۰ auth γ dq l :=
    auth_mono ۰ auth (A := leibnizO (list A)) prefix γ dq l.
  Definition mono_list ۰ lb γ l :=
    auth_mono ۰ lb (A := leibnizO (list A)) prefix γ l.
  Definition mono_list ۰ at γ i a : iProp Σ :=
    ∃ l ,
    ⌜l !! i = Some a ⌝ ∗
    mono_list ۰ lb γ l.
  Definition mono_list ۰ elem γ a : iProp Σ :=
    ∃ i ,
    mono_list ۰ at γ i a.

  #[global] Instance mono_list ۰ auth ｰ timeless γ dq l :
    Timeless (mono_list ۰ auth γ dq l).
  #[global] Instance mono_list ۰ lb ｰ timeless γ l :
    Timeless (mono_list ۰ lb γ l).
  #[global] Instance mono_list ۰ at ｰ timeless γ i a :
    Timeless (mono_list ۰ at γ i a).
  #[global] Instance mono_list ۰ elem ｰ timeless γ a :
    Timeless (mono_list ۰ elem γ a).

  #[global] Instance mono_list ۰ lb ｰ persistent γ l :
    Persistent (mono_list ۰ lb γ l).
  #[global] Instance mono_list ۰ at ｰ persistent γ i a :
    Persistent (mono_list ۰ at γ i a).
  #[global] Instance mono_list ۰ elem ｰ persistent γ a :
    Persistent (mono_list ۰ elem γ a).

  #[global] Instance mono_list ۰ auth ｰ fractional γ l :
    Fractional (λ q, mono_list ۰ auth γ (DfracOwn q) l).
  #[global] Instance mono_list ۰ auth ｰ as_fractional γ q l :
    AsFractional (mono_list ۰ auth γ (DfracOwn q) l) (λ q, mono_list ۰ auth γ (DfracOwn q) l) q.

  Lemma mono_list ｰ alloc l :
    ⊢ |==>
      ∃ γ ,
      mono_list ۰ auth γ (DfracOwn 1) l.

  Lemma mono_list ۰ auth ｰ valid γ dq l :
    mono_list ۰ auth γ dq l ⊢
    ⌜✓ dq ⌝.
  Lemma mono_list ۰ auth ｰ combine γ dq1 l1 dq2 l2 :
    mono_list ۰ auth γ dq1 l1 -∗
    mono_list ۰ auth γ dq2 l2 -∗
      ⌜l1 = l2 ⌝ ∗
      mono_list ۰ auth γ (dq1 ⋅ dq2) l1.
  Lemma mono_list ۰ auth ｰ valid ｰ2 γ dq1 l1 dq2 l2 :
    mono_list ۰ auth γ dq1 l1 -∗
    mono_list ۰ auth γ dq2 l2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜l1 = l2 ⌝.
  Lemma mono_list ۰ auth ｰ agree γ dq1 l1 dq2 l2 :
    mono_list ۰ auth γ dq1 l1 -∗
    mono_list ۰ auth γ dq2 l2 -∗
    ⌜l1 = l2 ⌝.
  Lemma mono_list ۰ auth ｰ dfrac ｰ ne γ1 dq1 l1 γ2 dq2 l2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    mono_list ۰ auth γ1 dq1 l1 -∗
    mono_list ۰ auth γ2 dq2 l2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma mono_list ۰ auth ｰ ne γ1 l1 γ2 dq2 l2 :
    mono_list ۰ auth γ1 (DfracOwn 1) l1 -∗
    mono_list ۰ auth γ2 dq2 l2 -∗
    ⌜γ1 ≠ γ2 ⌝.
  Lemma mono_list ۰ auth ｰ exclusive γ l1 dq2 l2 :
    mono_list ۰ auth γ (DfracOwn 1) l1 -∗
    mono_list ۰ auth γ dq2 l2 -∗
    False.
  Lemma mono_list ۰ auth ｰ persist γ dq l :
    mono_list ۰ auth γ dq l ⊢ |==>
    mono_list ۰ auth γ DfracDiscarded l.

  Lemma mono_list ۰ lb ｰ get γ q l :
    mono_list ۰ auth γ q l ⊢
    mono_list ۰ lb γ l.
  Lemma mono_list ۰ at ｰ get {γ q l} i a :
    l !! i = Some a →
    mono_list ۰ auth γ q l ⊢
    mono_list ۰ at γ i a.
  Lemma mono_list ۰ elem ｰ get {γ q l} a :
    a ∈ l →
    mono_list ۰ auth γ q l ⊢
    mono_list ۰ elem γ a.

  Lemma mono_list ۰ lb ｰ mono {γ l} l' :
    l' `prefix_of ` l →
    mono_list ۰ lb γ l ⊢
    mono_list ۰ lb γ l'.

  Lemma mono_list ۰ lb ｰ valid γ dq l1 l2 :
    mono_list ۰ auth γ dq l1 -∗
    mono_list ۰ lb γ l2 -∗
    ⌜l2 `prefix_of ` l1 ⌝.
  Lemma mono_list ۰ lb ｰ agree γ l1 l2 :
    mono_list ۰ lb γ l1 -∗
    mono_list ۰ lb γ l2 -∗
      ∃ l ,
      ⌜l1 `prefix_of ` l ⌝ ∧
      ⌜l2 `prefix_of ` l ⌝.
  Lemma mono_list ۰ at ｰ valid γ q l i a :
    mono_list ۰ auth γ q l -∗
    mono_list ۰ at γ i a -∗
    ⌜l !! i = Some a ⌝.
  Lemma mono_list ۰ at ｰ agree γ i a1 a2 :
    mono_list ۰ at γ i a1 -∗
    mono_list ۰ at γ i a2 -∗
    ⌜a1 = a2 ⌝.
  Lemma mono_list ۰ elem ｰ valid γ q l a :
    mono_list ۰ auth γ q l -∗
    mono_list ۰ elem γ a -∗
    ⌜a ∈ l ⌝.

  Lemma mono_list ｰ update {γ l} l' :
    l `prefix_of ` l' →
    mono_list ۰ auth γ (DfracOwn 1) l ⊢ |==>
    mono_list ۰ auth γ (DfracOwn 1) l'.
  Lemma mono_list ｰ update ｰ app {γ l} l' :
    mono_list ۰ auth γ (DfracOwn 1) l ⊢ |==>
    mono_list ۰ auth γ (DfracOwn 1) (l ++ l').
  Lemma mono_list ｰ update ｰ snoc {γ l} a :
    mono_list ۰ auth γ (DfracOwn 1) l ⊢ |==>
    mono_list ۰ auth γ (DfracOwn 1) (l ++ [a]).
End mono_list ۰ G.

#[global] Opaque mono_list ۰ auth.
#[global] Opaque mono_list ۰ lb.
#[global] Typeclasses Opaque mono_list۰at.
#[global] Typeclasses Opaque mono_list۰elem.