Library zoo.iris.base_logic.lib.ghost_list

Require Import iris.base_logic.lib.ghost_map.

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class GhostListG Σ A :=
  { #[local] ghost_list۰G۰map۰G :: ghost_mapG Σ nat A
  }.

Definition ghost_list۰Σ A :=
  #[ghost_mapΣ nat A
  ].
#[global] Instance subGｰghost_list۰Σ Σ A :
  subG (ghost_list۰Σ A) Σ →
  GhostListG Σ A.

Section ghost_list۰G.
  Context `{ghost_list۰G : !GhostListG Σ A}.

  Implicit Type x : A.
  Implicit Type xs : list A.

  Definition ghost_list۰auth γ xs :=
    ghost_map_auth γ 1 (map_seq 0 xs).
  Definition ghost_list۰at γ :=
    ghost_map_elem γ.

  #[global] Instance ghost_list۰authｰtimeless γ vs :
    Timeless (ghost_list۰auth γ vs).
  #[global] Instance ghost_list۰atｰtimeless γ i dq x :
    Timeless (ghost_list۰at γ i dq x).

  #[global] Instance ghost_list۰atｰpersistent γ i x :
    Persistent (ghost_list۰at γ i DfracDiscarded x).

  #[global] Instance ghost_list۰atｰfractional γ i x :
    Fractional (λ q, ghost_list۰at γ i (DfracOwn q) x).
  #[global] Instance ghost_list۰atｰas_fractional γ i q x :
    AsFractional (ghost_list۰at γ i (DfracOwn q) x) (λ q, ghost_list۰at γ i (DfracOwn q) x) q.

  Lemma ghost_listｰalloc xs :
    ⊢ |==>
      ∃ γ,
      ghost_list۰auth γ xs ∗
      [∗ list] i ↦ x ∈ xs,
        ghost_list۰at γ i (DfracOwn 1) x.

  Lemma ghost_list۰authｰexclusive γ xs1 xs2 :
    ghost_list۰auth γ xs1 -∗
    ghost_list۰auth γ xs2 -∗
    False.

  Lemma ghost_list۰atｰvalid γ i dq x :
    ghost_list۰at γ i dq x ⊢
    ⌜✓ dq⌝.
  Lemma ghost_list۰atｰcombine γ i dq1 x1 dq2 x2 :
    ghost_list۰at γ i dq1 x1 -∗
    ghost_list۰at γ i dq2 x2 -∗
      ⌜x1 = x2⌝ ∗
      ghost_list۰at γ i (dq1 ⋅ dq2) x1.
  Lemma ghost_list۰atｰvalidｰ2 γ i dq1 x1 dq2 x2 :
    ghost_list۰at γ i dq1 x1 -∗
    ghost_list۰at γ i dq2 x2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜x1 = x2⌝.
  Lemma ghost_list۰atｰagree γ i dq1 x1 dq2 x2 :
    ghost_list۰at γ i dq1 x1 -∗
    ghost_list۰at γ i dq2 x2 -∗
    ⌜x1 = x2⌝.
  Lemma ghost_list۰atｰdfracｰne γ1 i1 dq1 x1 γ2 i2 dq2 x2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    ghost_list۰at γ1 i1 dq1 x1 -∗
    ghost_list۰at γ2 i2 dq2 x2 -∗
    ⌜γ1 ≠ γ2 ∨ i1 ≠ i2⌝.
  Lemma ghost_list۰atｰne γ1 i1 x1 γ2 i2 dq2 x2 :
    ghost_list۰at γ1 i1 (DfracOwn 1) x1 -∗
    ghost_list۰at γ2 i2 dq2 x2 -∗
    ⌜γ1 ≠ γ2 ∨ i1 ≠ i2⌝.
  Lemma ghost_list۰atｰexclusive γ i x1 dq2 x2 :
    ghost_list۰at γ i (DfracOwn 1) x1 -∗
    ghost_list۰at γ i dq2 x2 -∗
    False.
  Lemma ghost_list۰atｰpersist γ i dq x :
    ghost_list۰at γ i dq x ⊢ |==>
    ghost_list۰at γ i DfracDiscarded x.

  Lemma ghost_listｰlookup γ xs i dq x :
    ghost_list۰auth γ xs -∗
    ghost_list۰at γ i dq x -∗
    ⌜xs !! i = Some x⌝.
  Lemma ghost_listｰauthｰats γ xs1 dq xs2 :
    length xs1 = length xs2 →
    ghost_list۰auth γ xs1 -∗
    ([∗ list] i ↦ x ∈ xs2, ghost_list۰at γ i dq x) -∗
    ⌜xs1 = xs2⌝.

  Lemma ghost_listｰupdateｰpush {γ xs} x :
    ghost_list۰auth γ xs ⊢ |==>
      ghost_list۰auth γ (xs ++ [x]) ∗
      ghost_list۰at γ (length xs) (DfracOwn 1) x.
  Lemma ghost_listｰupdateｰat {γ xs i x} x' :
    ghost_list۰auth γ xs -∗
    ghost_list۰at γ i (DfracOwn 1) x ==∗
      ghost_list۰auth γ (<[i := x']> xs) ∗
      ghost_list۰at γ i (DfracOwn 1) x'.
End ghost_list۰G.

#[global] Opaque ghost_list۰auth.
#[global] Opaque ghost_list۰at.