Take and Drop lemmas for lists

This file provides lemmas about List.take and List.drop and related functions.

take, drop

theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : ℕ} (h : n < l.length) : take 1 (drop n l) = [l.get ⟨n, h⟩]

@[simp]

theorem List.take_eq_self_iff {α : Type u} (x : List α) {n : ℕ} : take n x = x ↔ x.length ≤ n

@[simp]

theorem List.take_self_eq_iff {α : Type u} (x : List α) {n : ℕ} : x = take n x ↔ x.length ≤ n

@[simp]

theorem List.take_eq_left_iff {α : Type u} {x y : List α} {n : ℕ} : take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

@[simp]

theorem List.left_eq_take_iff {α : Type u} {x y : List α} {n : ℕ} : take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

@[simp]

theorem List.drop_take_append_drop {α : Type u} (x : List α) (m n : ℕ) : take n (drop m x) ++ drop (m + n) x = drop m x

@[simp]

theorem List.drop_take_append_drop' {α : Type u} (x : List α) (m n : ℕ) : take n (drop m x) ++ drop (n + m) x = drop m x

Compared to drop_take_append_drop, the order of summands is swapped.

theorem List.take_concat_get' {α : Type u} (l : List α) (i : ℕ) (h : i < l.length) : take i l ++ [l[i]] = take (i + 1) l

take_concat_get in simp normal form

theorem List.cons_getElem_drop_succ {α : Type u} {l : List α} {n : ℕ} {h : n < l.length} : l[n] :: drop (n + 1) l = drop n l

theorem List.cons_get_drop_succ {α : Type u} {l : List α} {n : Fin l.length} : l.get n :: drop (↑n + 1) l = drop (↑n) l

theorem List.drop_length_sub_one {α : Type u} {l : List α} (h : l ≠ []) : drop (l.length - 1) l = [l.getLast h]

theorem List.tail_iterate {α : Type u} (l : List α) (n : ℕ) : tail^[n] l = drop n l

Applying tail to a list n times is equivalent to dropping n elements.

@[simp]

theorem List.takeI_length {α : Type u} [Inhabited α] (n : ℕ) (l : List α) : (takeI n l).length = n

@[simp]

theorem List.takeI_nil {α : Type u} [Inhabited α] (n : ℕ) : takeI n [] = replicate n default

theorem List.takeI_eq_take {α : Type u} [Inhabited α] {n : ℕ} {l : List α} : n ≤ l.length → takeI n l = take n l

@[simp]

theorem List.takeI_left {α : Type u} [Inhabited α] (l₁ l₂ : List α) : takeI l₁.length (l₁ ++ l₂) = l₁

theorem List.takeI_left' {α : Type u} [Inhabited α] {l₁ l₂ : List α} {n : ℕ} (h : l₁.length = n) : takeI n (l₁ ++ l₂) = l₁

@[simp]

theorem List.takeD_length {α : Type u} (n : ℕ) (l : List α) (a : α) : (takeD n l a).length = n

theorem List.takeD_eq_take {α : Type u} {n : ℕ} {l : List α} (a : α) : n ≤ l.length → takeD n l a = take n l

@[simp]

theorem List.takeD_left {α : Type u} (l₁ l₂ : List α) (a : α) : takeD l₁.length (l₁ ++ l₂) a = l₁

theorem List.takeD_left' {α : Type u} {l₁ l₂ : List α} {n : ℕ} {a : α} (h : l₁.length = n) : takeD n (l₁ ++ l₂) a = l₁

filter

@[simp]

theorem List.span_eq_takeWhile_dropWhile {α : Type u} (p : α → Bool) (l : List α) : span p l = (takeWhile p l, dropWhile p l)

Miscellaneous lemmas

theorem List.dropSlice_eq {α : Type u} (xs : List α) (n m : ℕ) : dropSlice n m xs = take n xs ++ drop (n + m) xs

@[simp]

theorem List.length_dropSlice {α : Type u} (i j : ℕ) (xs : List α) : (dropSlice i j xs).length = xs.length - min j (xs.length - i)

theorem List.length_dropSlice_lt {α : Type u} (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) : (dropSlice i j xs).length < xs.length