Library zoo.iris.bi.big_op.big_sepL_seq

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

Section bi.
  Context {PROP : bi}.

  Section big_sepL_seq.
    Context {A : Type}.

    Implicit Types l : list A.
    Implicit Types Φ : 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 (S n), Φ k) ⊣⊢
        Φ i ∗
        ([∗ list] k ∈ seq (S i) n, Φ k).
    Lemma big_sepL_seq_cons_1 Φ i n :
      ([∗ list] k ∈ seq i (S n), Φ k) ⊢
        Φ i ∗
        ([∗ list] k ∈ seq (S i) n, Φ k).
    Lemma big_sepL_seq_cons_2 Φ i n :
      ([∗ list] k ∈ seq (S i) n, Φ k) -∗
      Φ i -∗
      [∗ list] k ∈ seq i (S n), Φ k.

    Lemma big_sepL_seq_snoc Φ i n :
      ([∗ list] k ∈ seq i (S n), Φ k) ⊣⊢
        ([∗ list] k ∈ seq i n, Φ k) ∗
        Φ (i + n).
    Lemma big_sepL_seq_snoc_1 Φ i n :
      ([∗ list] k ∈ seq i (S n), Φ k) ⊢
        ([∗ list] k ∈ seq i n, Φ k) ∗
        Φ (i + n).
    Lemma big_sepL_seq_snoc_2 Φ i n :
      ([∗ list] k ∈ seq i n, Φ k) -∗
      Φ (i + n) -∗
      [∗ list] k ∈ seq i (S 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_1 {Φ 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_2 Φ 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_1 `{!BiAffine PROP} {Φ} l i n :
      length l = n →
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      [∗ list] k ↦ _ ∈ l, Φ (i + k).
    Lemma big_sepL_seq_index_2 `{!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_1 `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq (i + j) n, Φ k) ⊢
      [∗ list] k ∈ seq i n, Φ (k + j).
    Lemma big_sepL_seq_shift_2 `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq i n, Φ (k + j)) ⊢
      [∗ list] k ∈ seq (i + j) n, Φ k.
    Lemma big_sepL_seq_shift_2' `{!BiAffine PROP} {Φ} j i n :
      ([∗ list] k ∈ seq i n, Φ k) ⊢
      [∗ list] k ∈ seq (i + j) n, Φ (k - j).

    Lemma big_sepL_seq_shift1 `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq (S i) n, Φ k) ⊣⊢
      [∗ list] k ∈ seq i n, Φ (S k).
    Lemma big_sepL_seq_shift1_1 `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq (S i) n, Φ k) ⊢
      [∗ list] k ∈ seq i n, Φ (S k).
    Lemma big_sepL_seq_shift1_2 `{!BiAffine PROP} Φ i n :
      ([∗ list] k ∈ seq i n, Φ (S k)) ⊢
      [∗ list] k ∈ seq (S i) n, Φ k.

    Lemma big_sepL_seq_exists `{!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.