Library zoo.iris.bi.big_op.big_sepL_seq

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

Section bi.
  Context {PROP : bi}.

  Section big_sepL۰seq.
    Context {A : Type}.

    Implicit Type l : list A.
    Implicit Type Φ : nat → PROP.

    Lemma big_sepLｰseqｰintro Φ i n :
      □ (
        ∀ k,
        ⌜i ≤ k < i + n⌝ -∗
        Φ k
      ) ⊢
      [∗ list] k ∈ seq i n, Φ k.

    Lemma big_sepLｰseqｰimpl Φ1 Φ2 i n :
      ([∗ list] k ∈ seq i n, Φ1 k) -∗
      □ (
        ∀ k,
        ⌜i ≤ k < i + n⌝ -∗
        Φ1 k -∗
        Φ2 k
      ) -∗
      [∗ list] k ∈ seq i n, Φ2 k.

    Lemma big_sepLｰseqｰcons Φ i n :
      ([∗ list] k ∈ seq i ˖n, Φ k) ⊣⊢
        Φ i ∗
        ([∗ list] k ∈ seq ˖i n, Φ k).
    Lemma big_sepLｰseqｰcons₁ Φ i n :
      ([∗ list] k ∈ seq i ˖n, Φ k) ⊢
        Φ i ∗
        ([∗ list] k ∈ seq ˖i n, Φ k).
    Lemma big_sepLｰseqｰcons₂ Φ i n :
      ([∗ list] k ∈ seq ˖i n, Φ k) -∗
      Φ i -∗
      [∗ list] k ∈ seq i ˖n, Φ k.

    Lemma big_sepLｰseqｰsnoc Φ i n :
      ([∗ list] k ∈ seq i ˖n, Φ k) ⊣⊢
        ([∗ list] k ∈ seq i n, Φ k) ∗
        Φ (i + n).
    Lemma big_sepLｰseqｰsnoc₁ Φ i n :
      ([∗ list] k ∈ seq i ˖n, Φ k) ⊢
        ([∗ list] k ∈ seq i n, Φ k) ∗
        Φ (i + n).
    Lemma big_sepLｰseqｰsnoc₂ Φ i n :
      ([∗ list] k ∈ seq i n, Φ k) -∗
      Φ (i + n) -∗
      [∗ list] k ∈ seq i ˖n, Φ k.

    Lemma big_sepLｰseqｰapp Φ i n1 n2 :
      ([∗ list] k ∈ seq i (n1 + n2), Φ k) ⊣⊢
        ([∗ list] k ∈ seq i n1, Φ k) ∗
        ([∗ list] k ∈ seq (i + n1) n2, Φ k).
    Lemma big_sepLｰseqｰapp₁ {Φ i n} n1 n2 :
      n = n1 + n2 →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
        ([∗ list] k ∈ seq i n1, Φ k) ∗
        ([∗ list] k ∈ seq (i + n1) n2, Φ k).
    Lemma big_sepLｰseqｰapp₂ Φ i1 n1 i2 n2 :
      i2 = i1 + n1 →
      ([∗ list] k ∈ seq i1 n1, Φ k) -∗
      ([∗ list] k ∈ seq i2 n2, Φ k) -∗
      [∗ list] k ∈ seq i1 (n1 + n2), Φ k.

    Lemma big_sepLｰseqｰlookupｰacc {Φ i n} j :
      j < n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
        Φ (i + j) ∗
        ( Φ (i + j) -∗
          [∗ list] k ∈ seq i n, Φ k
        ).
    Lemma big_sepLｰseqｰlookupｰacc' {Φ i n} j :
      i ≤ j < i + n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
        Φ j ∗
        ( Φ j -∗
          [∗ list] k ∈ seq i n, Φ k
        ).
    Lemma big_sepLｰseqｰlookup `{!BiAffine PROP} {Φ i n} j :
      j < n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      Φ (i + j).
    Lemma big_sepLｰseqｰlookup' `{!BiAffine PROP} {Φ i n} j :
      i ≤ j < i + n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      Φ j.

    Lemma big_sepLｰseqｰindex `{!BiAffine PROP} {Φ} l i n :
      length l = n →
      ([∗ list] k ∈ seq i n, Φ k) ⊣⊢
      [∗ list] k ↦ _ ∈ l, Φ (i + k).
    Lemma big_sepLｰseqｰindex₁ `{!BiAffine PROP} {Φ} l i n :
      length l = n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      [∗ list] k ↦ _ ∈ l, Φ (i + k).
    Lemma big_sepLｰseqｰindex₂ `{!BiAffine PROP} {Φ l} n :
      length l = n →
      ([∗ list] k ↦ _ ∈ l, Φ k) ⊢
      [∗ list] k ∈ seq 0 n, Φ k.

    Lemma big_sepLｰseqｰshift `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq (i + j) n, Φ k) ⊣⊢
      [∗ list] k ∈ seq i n, Φ (k + j).
    Lemma big_sepLｰseqｰshift' `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq (i + j) n, Φ (k - j)) ⊣⊢
      [∗ list] k ∈ seq i n, Φ k.
    Lemma big_sepLｰseqｰshift₁ `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq (i + j) n, Φ k) ⊢
      [∗ list] k ∈ seq i n, Φ (k + j).
    Lemma big_sepLｰseqｰshift₂ `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq i n, Φ (k + j)) ⊢
      [∗ list] k ∈ seq (i + j) n, Φ k.
    Lemma big_sepLｰseqｰshift₂' `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      [∗ list] k ∈ seq (i + j) n, Φ (k - j).

    Lemma big_sepLｰseqｰshiftｰ1 `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq ˖i n, Φ k) ⊣⊢
      [∗ list] k ∈ seq i n, Φ ˖k.
    Lemma big_sepLｰseqｰshiftｰ1₁ `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq ˖i n, Φ k) ⊢
      [∗ list] k ∈ seq i n, Φ ˖k.
    Lemma big_sepLｰseqｰshiftｰ1₂ `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq i n, Φ ˖k) ⊢
      [∗ list] k ∈ seq ˖i n, Φ k.

    Lemma big_sepLｰseqｰ∃ `{!BiAffine PROP} `(Φ : nat → A → PROP) i n :
      ([∗ list] k ∈ seq i n, ∃ x, Φ k x) ⊢
        ∃ xs,
        ⌜length xs = n⌝ ∗
        [∗ list] k ↦ x ∈ xs, Φ (i + k) x.

    Lemma big_sepLｰseqｰtoｰseqZ `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      [∗ list] k ∈ seqZ ⁺i ⁺n, Φ ₊k.
    Lemma big_sepLｰseqｰtoｰseqZ' `{!BiAffine PROP} Φ i n :
      (0 ≤ i)%Z →
      (0 ≤ n)%Z →
      ([∗ list] k ∈ seq ₊i ₊n, Φ k) ⊢
      [∗ list] k ∈ seqZ i n, Φ ₊k.
  End big_sepL۰seq.
End bi.