Library zoo.iris.bi.big_op.big_sepL

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

Section bi.
  Context {PROP : bi}.

  Section big_sepL.
    Context {A : Type}.

    Implicit Type Φ : 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ｰseqｰ0 `{!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 Type Φ : nat → A → PROP.

    Lemma big_sepLｰcons₁ Φ x l :
      ([∗ list] k ↦ y ∈ (x :: l), Φ k y) ⊢
        Φ 0 x ∗
        [∗ list] k ↦ y ∈ l, Φ ˖k y.
    Lemma big_sepLｰcons₂ Φ x l :
      Φ 0 x -∗
      ([∗ list] k ↦ y ∈ l, Φ ˖k y) -∗
      [∗ list] k ↦ y ∈ (x :: l), Φ k y.
    Lemma big_sepLｰcons₂' (Φ : A → PROP) x l :
      Φ x -∗
      ([∗ list] y ∈ l, Φ y) -∗
      [∗ list] y ∈ (x :: l), Φ y.

    Lemma big_sepLｰapp₁ Φ 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₂ Φ 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₁ Φ l x :
      ([∗ list] k ↦ y ∈ (l ++ [x]), Φ k y) ⊢
        ([∗ list] k ↦ y ∈ l, Φ k y) ∗
        Φ (length l) x.
    Lemma big_sepLｰsnoc₂ {Φ 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₁ Φ 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₂ Φ 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'₁ `{!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'₂ `{!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₁ `{!BiAffine PROP} Φ n x :
      ([∗ list] k ↦ y ∈ replicate n x, Φ k y) ⊢
      [∗ list] k ∈ seq 0 n, Φ k x.
    Lemma big_sepLｰreplicate₂ `{!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ｰ∃ `{!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.