Library zoo.iris.bi.big_op.big_sepL

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

Section bi.
  Context {PROP : bi}.

  Section big_sepL.
    Context {A : Type}.

    Implicit Types Φ : nat → A → PROP.

    Lemma big_sepL_to_seq `{!BiAffine PROP} Φ l i :
      ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢
      [∗ list] k ∈ seq i (length l),
        ∃ y,
        ⌜l !! (k - i) = Some y⌝ ∗
        Φ (k - i) y.
    Lemma big_sepL_to_seq0 `{!BiAffine PROP} Φ l :
      ([∗ list] k ↦ y ∈ l, Φ k y) ⊣⊢
      [∗ list] k ∈ seq 0 (length l),
        ∃ y,
        ⌜l !! k = Some y⌝ ∗
        Φ k y.
  End big_sepL.

  Section big_sepL.
    Context {A : Type}.

    Implicit Types Φ : nat → A → PROP.

    Lemma big_sepL_cons_1 Φ x l :
      ([∗ list] k ↦ y ∈ (x :: l), Φ k y) ⊢
        Φ 0 x ∗
        [∗ list] k ↦ y ∈ l, Φ (S k) y.
    Lemma big_sepL_cons_2 Φ x l :
      Φ 0 x -∗
      ([∗ list] k ↦ y ∈ l, Φ (S k) y) -∗
      [∗ list] k ↦ y ∈ (x :: l), Φ k y.
    Lemma big_sepL_cons_2' (Φ : A → PROP) x l :
      Φ x -∗
      ([∗ list] y ∈ l, Φ y) -∗
      [∗ list] y ∈ (x :: l), Φ y.

    Lemma big_sepL_app_1 Φ l1 l2 :
      ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y) ⊢
        ([∗ list] k ↦ y ∈ l1, Φ k y) ∗
        ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
    Lemma big_sepL_app_2 Φ l1 l2 :
      ([∗ list] k ↦ y ∈ l1, Φ k y) -∗
      ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) -∗
      [∗ list] k ↦ y ∈ l1 ++ l2, Φ k y.

    Lemma big_sepL_snoc_1 Φ l x :
      ([∗ list] k ↦ y ∈ (l ++ [x]), Φ k y) ⊢
        ([∗ list] k ↦ y ∈ l, Φ k y) ∗
        Φ (length l) x.
    Lemma big_sepL_snoc_2 {Φ l} x :
      ([∗ list] k ↦ y ∈ l, Φ k y) -∗
      Φ (length l) x -∗
      ([∗ list] k ↦ y ∈ (l ++ [x]), Φ k y).

    Lemma big_sepL_prefix `{!BiAffine PROP} {Φ l1} l2 :
      l2 `prefix_of` l1 →
      ([∗ list] k ↦ x ∈ l1, Φ k x) ⊢
      ([∗ list] k ↦ x ∈ l2, Φ k x).

    Lemma big_sepL_suffix `{!BiAffine PROP} {Φ : A → PROP} {l1} l2 :
      l2 `suffix_of` l1 →
      ([∗ list] x ∈ l1, Φ x) ⊢
      ([∗ list] x ∈ l2, Φ x).

    Lemma big_sepL_impl_stronger `{!BiAffine PROP} {A1 A2} (Φ1 : nat → A1 → PROP) l1 (Φ2 : nat → A2 → PROP) l2 :
      length l1 = length l2 →
      ([∗ list] k ↦ x ∈ l1, Φ1 k x) -∗
      ( [∗ list] k ∈ seq 0 (length l1),
        ∀ x1 x2,
        ⌜l1 !! k = Some x1⌝ -∗
        ⌜l2 !! k = Some x2⌝ -∗
        Φ1 k x1 -∗
        Φ2 k x2
      ) -∗
      [∗ list] k ↦ x ∈ l2, Φ2 k x.
    Lemma big_sepL_impl_strong `{!BiAffine PROP} {A1 A2} (Φ1 : nat → A1 → PROP) (l1 : list A1) (Φ2 : nat → A2 → PROP) (l2 : list A2) :
      length l1 = length l2 →
      ([∗ list] k ↦ x ∈ l1, Φ1 k x) -∗
      □ (
        ∀ k x1 x2,
        ⌜l1 !! k = Some x1⌝ -∗
        ⌜l2 !! k = Some x2⌝ -∗
        Φ1 k x1 -∗
        Φ2 k x2
      ) -∗
      [∗ list] k ↦ x ∈ l2, Φ2 k x.

    Lemma big_sepL_impl_sepL2 `{!BiAffine PROP} {B1 B2} Φ1 l (Φ2 : nat → B1 → B2 → PROP) 𝑙1 𝑙2 :
      length l = length 𝑙1 →
      length l = length 𝑙2 →
      ([∗ list] k ↦ y ∈ l, Φ1 k y) -∗
      □ (
        ∀ k x 𝑥1 𝑥2,
        ⌜l !! k = Some x⌝ -∗
        ⌜𝑙1 !! k = Some 𝑥1⌝ -∗
        ⌜𝑙2 !! k = Some 𝑥2⌝ -∗
        Φ1 k x -∗
        Φ2 k 𝑥1 𝑥2
      ) -∗
      [∗ list] k ↦ y1; y2 ∈ 𝑙1; 𝑙2, Φ2 k y1 y2.

    Lemma big_sepL_insert `{!BiAffine PROP} {Φ l} i x :
      i < length l →
      ([∗ list] k ↦ y ∈ l, Φ k y) -∗
      Φ i x -∗
      [∗ list] k ↦ y ∈ <[i := x]> l, Φ k y.

    Lemma big_sepL_delete_1 Φ l i x :
      l !! i = Some x →
      ([∗ list] k ↦ y ∈ l, Φ k y) ⊢
        Φ i x ∗
        [∗ list] k ↦ y ∈ l, if decide (k = i) then emp else Φ k y.
    Lemma big_sepL_delete_2 Φ l i x :
      l !! i = Some x →
      Φ i x -∗
      ([∗ list] k ↦ y ∈ l, if decide (k = i) then emp else Φ k y) -∗
      [∗ list] k ↦ y ∈ l, Φ k y.
    Lemma big_sepL_delete'_1 `{!BiAffine PROP} Φ l i x :
      l !! i = Some x →
      ([∗ list] k ↦ y ∈ l, Φ k y) ⊢
        Φ i x ∗
        [∗ list] k ↦ y ∈ l, ⌜k ≠ i⌝ → Φ k y.
    Lemma big_sepL_delete'_2 `{!BiAffine PROP} Φ l i x :
      l !! i = Some x →
      Φ i x -∗
      ([∗ list] k ↦ y ∈ l, ⌜k ≠ i⌝ → Φ k y) -∗
      [∗ list] k ↦ y ∈ l, Φ k y.

    Lemma big_sepL_replicate `{!BiAffine PROP} Φ n x :
      ([∗ list] k ↦ y ∈ replicate n x, Φ k y) ⊣⊢
      [∗ list] k ∈ seq 0 n, Φ k x.
    Lemma big_sepL_replicate_1 `{!BiAffine PROP} Φ n x :
      ([∗ list] k ↦ y ∈ replicate n x, Φ k y) ⊢
      [∗ list] k ∈ seq 0 n, Φ k x.
    Lemma big_sepL_replicate_2 `{!BiAffine PROP} Φ n x :
      ([∗ list] k ∈ seq 0 n, Φ k x) ⊢
      [∗ list] k ↦ y ∈ replicate n x, Φ k y.

    Lemma big_sepL_or_l Ψ l Φ :
      ([∗ list] k ↦ x ∈ l, Φ k x) ⊢
      [∗ list] k ↦ x ∈ l, Ψ k x ∨ Φ k x.
    Lemma big_sepL_or_r Ψ l Φ :
      ([∗ list] k ↦ x ∈ l, Φ k x) ⊢
      [∗ list] k ↦ x ∈ l, Φ k x ∨ Ψ k x.

    Lemma big_sepL_exists `{!BiAffine PROP} {B} (Φ : nat → A → B → PROP) l :
      ([∗ list] k ↦ x ∈ l, ∃ y, Φ k x y) ⊢
        ∃ ys,
        ⌜length ys = length l⌝ ∗
        [∗ list] k ↦ x; y ∈ l; ys, Φ k x y.

    Lemma big_sepL_retract_index Φ l :
      ([∗ list] k ↦ x ∈ l, Φ k x) ⊢
      [∗ list] x ∈ l, ∃ k, Φ k x.

    Lemma big_sepL_impl_thread {Φ1} P Φ2 l :
      ([∗ list] k ↦ x ∈ l, Φ1 k x) -∗
      P -∗
      □ (
        ∀ k x,
        ⌜l !! k = Some x⌝ →
        Φ1 k x -∗
        P -∗
          Φ2 k x ∗
          P
      ) -∗
        ([∗ list] k ↦ x ∈ l, Φ2 k x) ∗
        P.
    Lemma big_sepL_impl_thread_fupd `{!BiFUpd PROP} {Φ1} P Φ2 l E :
      ([∗ list] k ↦ x ∈ l, Φ1 k x) -∗
      P -∗
      □ (
        ∀ k x,
        ⌜l !! k = Some x⌝ →
        Φ1 k x -∗
        P -∗
          |={E}=>
          Φ2 k x ∗
          P
      ) -∗
        |={E}=>
        ([∗ list] k ↦ x ∈ l, Φ2 k x) ∗
        P.

    Lemma big_sepL_Forall `{!BiPureForall PROP} (ϕ : A → Prop) l :
      ([∗ list] x ∈ l, ⌜ϕ x⌝) ⊢@{PROP}
      ⌜Forall ϕ l⌝.

    Lemma big_sepL_Foralli `{!BiPureForall PROP} (ϕ : nat → A → Prop) l :
      ([∗ list] k ↦ x ∈ l, ⌜ϕ k x⌝) ⊢@{PROP}
      ⌜Foralli ϕ l⌝.
  End big_sepL.
End bi.