Splitting a list to chunks of specified lengths

This file defines splitting a list to chunks of given lengths, and some proofs about that.

def List.splitLengths {α : Type u_1} : List ℕ → List α → List (List α)

Split a list to chunks of given lengths.

Equations

• [].splitLengths x✝ = []
• (n :: ns).splitLengths x✝ = match List.splitAt n x✝ with | (x0, x1) => x0 :: ns.splitLengths x1

@[simp]

theorem List.length_splitLengths {α : Type u_1} (l : List α) (sz : List ℕ) : (sz.splitLengths l).length = sz.length

@[simp]

theorem List.splitLengths_nil {α : Type u_1} (l : List α) : [].splitLengths l = []

@[simp]

theorem List.splitLengths_cons {α : Type u_1} (l : List α) (sz : List ℕ) (n : ℕ) : (n :: sz).splitLengths l = take n l :: sz.splitLengths (drop n l)

theorem List.take_splitLength {α : Type u_1} (l : List α) (sz : List ℕ) (i : ℕ) : take i (sz.splitLengths l) = (take i sz).splitLengths l

theorem List.length_splitLengths_getElem_le {α : Type u_1} (l : List α) (sz : List ℕ) {i : ℕ} {hi : i < (sz.splitLengths l).length} : (sz.splitLengths l)[i].length ≤ sz[i]

theorem List.flatten_splitLengths {α : Type u_1} (l : List α) (sz : List ℕ) (h : l.length ≤ sz.sum) : (sz.splitLengths l).flatten = l

theorem List.map_splitLengths_length {α : Type u_1} (l : List α) (sz : List ℕ) (h : sz.sum ≤ l.length) : map length (sz.splitLengths l) = sz

theorem List.length_splitLengths_getElem_eq {α : Type u_1} (l : List α) (sz : List ℕ) {i : ℕ} (hi : i < sz.length) (h : (take (i + 1) sz).sum ≤ l.length) : (sz.splitLengths l)[i].length = sz[i]

theorem List.splitLengths_length_getElem {α : Type u_2} (l : List α) (sz : List ℕ) (h : sz.sum ≤ l.length) (i : ℕ) (hi : i < (sz.splitLengths l).length) : (sz.splitLengths l)[i].length = sz[i]

theorem List.length_mem_splitLengths {α : Type u_2} (l : List α) (sz : List ℕ) (b : ℕ) (h : ∀ (n : ℕ), n ∈ sz → n ≤ b) (l₂ : List α) : l₂ ∈ sz.splitLengths l → l₂.length ≤ b