Lemmas about List.take and List.drop.

take and drop

Further results on List.take and List.drop, which rely on stronger automation in Nat, are given in Init.Data.List.TakeDrop.

theorem List.take_cons {α : Type u_1} {n : Nat} {a : α} {l : List α} (h : 0 < n) : take n (a :: l) = a :: take (n - 1) l

@[simp]

theorem List.drop_one {α : Type u_1} (l : List α) : drop 1 l = l.tail

@[simp]

theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) : take n l ++ drop n l = l

@[simp]

theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) : (drop i l).length = l.length - i

theorem List.drop_of_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : drop i l = []

theorem List.length_lt_of_drop_ne_nil {α : Type u_1} {l : List α} {n : Nat} (h : drop n l ≠ []) : n < l.length

theorem List.take_of_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : take i l = l

theorem List.lt_length_of_take_ne_self {α : Type u_1} {l : List α} {n : Nat} (h : take n l ≠ l) : n < l.length

@[reducible, inline, deprecated List.drop_of_length_le (since := "2024-07-07")]

abbrev List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : drop i l = []

Equations

• @List.drop_length_le = @List.drop_of_length_le

@[reducible, inline, deprecated List.take_of_length_le (since := "2024-07-07")]

abbrev List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length ≤ i) : take i l = l

Equations

• @List.take_length_le = @List.take_of_length_le

@[simp]

theorem List.drop_length {α : Type u_1} (l : List α) : drop l.length l = []

@[simp]

theorem List.take_length {α : Type u_1} (l : List α) : take l.length l = l

@[simp]

theorem List.getElem_cons_drop {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : l[i] :: drop (i + 1) l = drop i l

@[deprecated List.getElem_cons_drop (since := "2024-06-12")]

theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin l.length) : l.get i :: drop (↑i + 1) l = drop (↑i) l

theorem List.drop_eq_getElem_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l

@[deprecated List.drop_eq_getElem_cons (since := "2024-06-12")]

theorem List.drop_eq_get_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : drop n l = l.get ⟨n, h⟩ :: drop (n + 1) l

@[simp]

theorem List.getElem?_take_of_lt {α : Type u_1} {l : List α} {n m : Nat} (h : m < n) : (take n l)[m]? = l[m]?

@[deprecated List.getElem?_take_of_lt (since := "2024-06-12")]

theorem List.get?_take {α : Type u_1} {l : List α} {n m : Nat} (h : m < n) : (take n l).get? m = l.get? m

theorem List.getElem?_take_of_succ {α : Type u_1} {l : List α} {n : Nat} : (take (n + 1) l)[n]? = l[n]?

@[simp]

theorem List.drop_drop {α : Type u_1} (n m : Nat) (l : List α) : drop n (drop m l) = drop (m + n) l

theorem List.take_drop {α : Type u_1} (m n : Nat) (l : List α) : take n (drop m l) = drop m (take (m + n) l)

@[deprecated List.drop_drop (since := "2024-06-15")]

theorem List.drop_add {α : Type u_1} (m n : Nat) (l : List α) : drop (m + n) l = drop n (drop m l)

@[simp]

theorem List.tail_drop {α : Type u_1} (l : List α) (n : Nat) : (drop n l).tail = drop (n + 1) l

@[simp]

theorem List.drop_tail {α : Type u_1} (l : List α) (n : Nat) : drop n l.tail = drop (n + 1) l

@[simp]

theorem List.drop_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} : drop k l = [] ↔ l.length ≤ k

@[reducible, inline, deprecated List.drop_eq_nil_iff (since := "2024-09-10")]

abbrev List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} : drop k l = [] ↔ l.length ≤ k

Equations

• @List.drop_eq_nil_iff_le = @List.drop_eq_nil_iff

@[simp]

theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} : take k l = [] ↔ k = 0 ∨ l = []

theorem List.drop_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} : as = [] → drop i as = []

theorem List.ne_nil_of_drop_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : drop i as ≠ []) : as ≠ []

theorem List.take_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} : as = [] → take i as = []

theorem List.ne_nil_of_take_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : take i as ≠ []) : as ≠ []

theorem List.set_take {α : Type u_1} {l : List α} {n m : Nat} {a : α} : take n (l.set m a) = (take n l).set m a

theorem List.drop_set {α : Type u_1} {l : List α} {n m : Nat} {a : α} : drop n (l.set m a) = if m < n then drop n l else (drop n l).set (m - n) a

theorem List.set_drop {α : Type u_1} {l : List α} {n m : Nat} {a : α} : (drop n l).set m a = drop n (l.set (n + m) a)

theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : (take i l).concat l[i] = take (i + 1) l

@[simp]

theorem List.take_append_getElem {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : take i l ++ [l[i]] = take (i + 1) l

@[simp]

theorem List.take_append_getLast {α : Type u_1} (l : List α) (h : l ≠ []) : take (l.length - 1) l ++ [l.getLast h] = l

@[simp]

theorem List.take_append_getLast? {α : Type u_1} (l : List α) : take (l.length - 1) l ++ l.getLast?.toList = l

@[deprecated List.take_succ_cons (since := "2024-07-25")]

theorem List.take_cons_succ {α✝ : Type u_1} {a : α✝} {as : List α✝} {i : Nat} : take (i + 1) (a :: as) = a :: take i as

@[deprecated List.take_of_length_le (since := "2024-07-25")]

theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length ≤ n) : take n l = l

theorem List.drop_left {α : Type u_1} (l₁ l₂ : List α) : drop l₁.length (l₁ ++ l₂) = l₂

@[simp]

theorem List.drop_left' {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (h : l₁.length = n) : drop n (l₁ ++ l₂) = l₂

theorem List.take_left {α : Type u_1} (l₁ l₂ : List α) : take l₁.length (l₁ ++ l₂) = l₁

@[simp]

theorem List.take_left' {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (h : l₁.length = n) : take n (l₁ ++ l₂) = l₁

theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} : take (n + 1) l = take n l ++ l[n]?.toList

@[deprecated "Deprecated without replacement." (since := "2024-07-25")]

theorem List.drop_sizeOf_le {α : Type u_1} [SizeOf α] (l : List α) (n : Nat) : sizeOf (drop n l) ≤ sizeOf l

theorem List.dropLast_eq_take {α : Type u_1} (l : List α) : l.dropLast = take (l.length - 1) l

@[simp]

theorem List.map_take {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : map f (take i L) = take i (map f L)

@[simp]

theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : map f (drop i L) = drop i (map f L)

takeWhile and dropWhile

theorem List.takeWhile_cons {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : takeWhile p (a :: l) = if p a = true then a :: takeWhile p l else []

@[simp]

theorem List.takeWhile_cons_of_pos {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (h : p a = true) : takeWhile p (a :: l) = a :: takeWhile p l

@[simp]

theorem List.takeWhile_cons_of_neg {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (h : ¬p a = true) : takeWhile p (a :: l) = []

theorem List.dropWhile_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} : dropWhile p (x :: xs) = if p x = true then dropWhile p xs else x :: xs

@[simp]

theorem List.dropWhile_cons_of_pos {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (h : p a = true) : dropWhile p (a :: l) = dropWhile p l

@[simp]

theorem List.dropWhile_cons_of_neg {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (h : ¬p a = true) : dropWhile p (a :: l) = a :: l

theorem List.head?_takeWhile {α : Type u_1} (p : α → Bool) (l : List α) : (takeWhile p l).head? = Option.filter p l.head?

theorem List.head_takeWhile {α : Type u_1} (p : α → Bool) (l : List α) (w : takeWhile p l ≠ []) : (takeWhile p l).head w = l.head ⋯

theorem List.head?_dropWhile_not {α : Type u_1} (p : α → Bool) (l : List α) : match (dropWhile p l).head? with | some x => p x = false | none => True

theorem List.head_dropWhile_not {α : Type u_1} (p : α → Bool) (l : List α) (w : dropWhile p l ≠ []) : p ((dropWhile p l).head w) = false

theorem List.takeWhile_map {α : Type u_1} {β : Type u_2} (f : α → β) (p : β → Bool) (l : List α) : takeWhile p (map f l) = map f (takeWhile (p ∘ f) l)

theorem List.dropWhile_map {α : Type u_1} {β : Type u_2} (f : α → β) (p : β → Bool) (l : List α) : dropWhile p (map f l) = map f (dropWhile (p ∘ f) l)

theorem List.takeWhile_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Bool) (l : List α) : takeWhile p (filterMap f l) = filterMap f (takeWhile (fun (a : α) => Option.all p (f a)) l)

theorem List.dropWhile_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Bool) (l : List α) : dropWhile p (filterMap f l) = filterMap f (dropWhile (fun (a : α) => Option.all p (f a)) l)

theorem List.takeWhile_filter {α : Type u_1} (p q : α → Bool) (l : List α) : takeWhile q (filter p l) = filter p (takeWhile (fun (a : α) => !p a || q a) l)

theorem List.dropWhile_filter {α : Type u_1} (p q : α → Bool) (l : List α) : dropWhile q (filter p l) = filter p (dropWhile (fun (a : α) => !p a || q a) l)

@[simp]

theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) : takeWhile p l ++ dropWhile p l = l

theorem List.takeWhile_append {α : Type u_1} {p : α → Bool} {xs ys : List α} : takeWhile p (xs ++ ys) = if (takeWhile p xs).length = xs.length then xs ++ takeWhile p ys else takeWhile p xs

@[simp]

theorem List.takeWhile_append_of_pos {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : ∀ (a : α), a ∈ l₁ → p a = true) : takeWhile p (l₁ ++ l₂) = l₁ ++ takeWhile p l₂

theorem List.dropWhile_append {α : Type u_1} {p : α → Bool} {xs ys : List α} : dropWhile p (xs ++ ys) = if (dropWhile p xs).isEmpty = true then dropWhile p ys else dropWhile p xs ++ ys

@[simp]

theorem List.dropWhile_append_of_pos {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : ∀ (a : α), a ∈ l₁ → p a = true) : dropWhile p (l₁ ++ l₂) = dropWhile p l₂

@[simp]

theorem List.takeWhile_replicate_eq_filter {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : takeWhile p (replicate n a) = filter p (replicate n a)

theorem List.takeWhile_replicate {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : takeWhile p (replicate n a) = if p a = true then replicate n a else []

@[simp]

theorem List.dropWhile_replicate_eq_filter_not {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : dropWhile p (replicate n a) = filter (fun (a : α) => !p a) (replicate n a)

theorem List.dropWhile_replicate {α : Type u_1} {n : Nat} {a : α} (p : α → Bool) : dropWhile p (replicate n a) = if p a = true then [] else replicate n a

theorem List.take_takeWhile {α : Type u_1} {l : List α} (p : α → Bool) (n : Nat) : take n (takeWhile p l) = takeWhile p (take n l)

@[simp]

theorem List.all_takeWhile {α : Type u_1} {p : α → Bool} {l : List α} : (takeWhile p l).all p = true

@[simp]

theorem List.any_dropWhile {α : Type u_1} {p : α → Bool} {l : List α} : ((dropWhile p l).any fun (x : α) => !p x) = !l.all p

theorem List.replace_takeWhile {α : Type u_1} {a b : α} [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) : (takeWhile p l).replace a b = takeWhile p (l.replace a b)

splitAt

@[simp]

theorem List.splitAt_eq {α : Type u_1} (n : Nat) (l : List α) : splitAt n l = (take n l, drop n l)

rotateLeft

@[simp]

theorem List.rotateLeft_zero {α : Type u_1} (l : List α) : l.rotateLeft 0 = l

rotateRight

@[simp]

theorem List.rotateRight_zero {α : Type u_1} (l : List α) : l.rotateRight 0 = l