Library zoo.iris.bi.big_op.big_sepL_seqZ

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

Section bi.
  Context {PROP : bi}.

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

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

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

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

    Lemma big_sepLｰseqZｰcons Φ i n :
      (0 < n)%Z →
      ([∗ list] k ∈ seqZ i n, Φ k) ⊣⊢
        Φ i ∗
        ([∗ list] k ∈ seqZ (Z.succ i) (Z.pred n), Φ k).
    Lemma big_sepLｰseqZｰcons₁ Φ i n :
      (0 < n)%Z →
      ([∗ list] k ∈ seqZ i n, Φ k) ⊢
        Φ i ∗
        ([∗ list] k ∈ seqZ (Z.succ i) (Z.pred n), Φ k).
    Lemma big_sepLｰseqZｰcons₂ Φ i n :
      (0 ≤ n)%Z →
      ([∗ list] k ∈ seqZ i n, Φ k) -∗
      Φ (Z.pred i) -∗
      [∗ list] k ∈ seqZ (Z.pred i) (Z.succ n), Φ k.

    Lemma big_sepLｰseqZｰsnoc Φ i n :
      (0 ≤ n)%Z →
      ([∗ list] k ∈ seqZ i (Z.succ n), Φ k) ⊣⊢
        ([∗ list] k ∈ seqZ i n, Φ k) ∗
        Φ (i + n)%Z.
    Lemma big_sepLｰseqZｰsnoc₁ Φ i n :
      (0 ≤ n)%Z →
      ([∗ list] k ∈ seqZ i (Z.succ n), Φ k) ⊢
        ([∗ list] k ∈ seqZ i n, Φ k) ∗
        Φ (i + n)%Z.
    Lemma big_sepLｰseqZｰsnoc₂ Φ i n :
      (0 ≤ n)%Z →
      ([∗ list] k ∈ seqZ i n, Φ k) -∗
      Φ (i + n)%Z -∗
      [∗ list] k ∈ seqZ i (Z.succ n), Φ k.

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

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

    Lemma big_sepLｰseqZｰlookup `{!BiAffine PROP} {Φ i1 n} i2 :
      (i1 ≤ i2 < i1 + n)%Z →
      ([∗ list] k ∈ seqZ i1 n, Φ k) ⊢
      Φ i2.
  End big_sepL۰seqZ.
End bi.