Documentation

Init.Data.List.TakeDrop

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} {i : Nat} {a : α} {l : List α} (h : 0 < i) :
take i (a :: l) = a :: take (i - 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} (i : Nat) (l : List α) :
take i l ++ drop i 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 α} {i : Nat} (h : drop i l []) :
i < 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 α} {i : Nat} (h : take i l l) :
i < l.length
@[simp]
theorem List.drop_length {α : Type u_1} {l : List α} :
@[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
theorem List.drop_eq_getElem_cons {α : Type u_1} {i : Nat} {l : List α} (h : i < l.length) :
drop i l = l[i] :: drop (i + 1) l
@[simp]
theorem List.getElem?_take_of_lt {α : Type u_1} {l : List α} {i j : Nat} (h : i < j) :
(take j l)[i]? = l[i]?
theorem List.getElem?_take_of_succ {α : Type u_1} {l : List α} {i : Nat} :
(take (i + 1) l)[i]? = l[i]?
@[simp]
theorem List.drop_drop {α : Type u_1} {i j : Nat} {l : List α} :
drop i (drop j l) = drop (j + i) l
theorem List.drop_add_one_eq_tail_drop {α : Type u_1} {i : Nat} {l : List α} :
drop (i + 1) l = (drop i l).tail
theorem List.take_drop {α : Type u_1} {i j : Nat} {l : List α} :
take i (drop j l) = drop j (take (j + i) l)
@[simp]
theorem List.tail_drop {α : Type u_1} {l : List α} {i : Nat} :
(drop i l).tail = drop (i + 1) l
@[simp]
theorem List.drop_tail {α : Type u_1} {l : List α} {i : Nat} :
drop i l.tail = drop (i + 1) l
@[simp]
theorem List.drop_eq_nil_iff {α : Type u_1} {l : List α} {i : Nat} :
drop i l = [] l.length i
@[reducible, inline, deprecated List.drop_eq_nil_iff (since := "2024-09-10")]
abbrev List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {i : Nat} :
drop i l = [] l.length i
Equations
Instances For
    @[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.take_set {α : Type u_1} {l : List α} {i j : Nat} {a : α} :
    take i (l.set j a) = (take i l).set j a
    @[reducible, inline, deprecated List.take_set (since := "2025-02-17")]
    abbrev List.set_take {α : Type u_1} {l : List α} {i j : Nat} {a : α} :
    take i (l.set j a) = (take i l).set j a
    Equations
    Instances For
      theorem List.drop_set {α : Type u_1} {l : List α} {i j : Nat} {a : α} :
      drop i (l.set j a) = if j < i then drop i l else (drop i l).set (j - i) a
      theorem List.set_drop {α : Type u_1} {l : List α} {i j : Nat} {a : α} :
      (drop i l).set j a = drop i (l.set (i + j) 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
      theorem List.take_succ_eq_append_getElem {α : Type u_1} {i : Nat} {l : List α} (h : i < l.length) :
      take (i + 1) l = take i l ++ [l[i]]
      @[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 α) :
      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 α} {i : Nat} (h : l₁.length = i) :
      drop i (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 α} {i : Nat} (h : l₁.length = i) :
      take i (l₁ ++ l₂) = l₁
      theorem List.take_succ {α : Type u_1} {l : List α} {i : Nat} :
      take (i + 1) l = take i l ++ l[i]?.toList
      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 α} :
      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 α} :
      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} :
      theorem List.takeWhile_replicate {α : Type u_1} {n : Nat} {a : α} {p : αBool} :
      @[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} :
      theorem List.take_takeWhile {α : Type u_1} {i : Nat} {l : List α} {p : αBool} :
      take i (takeWhile p l) = takeWhile p (take i l)
      @[simp]
      theorem List.all_takeWhile {α : Type u_1} {p : αBool} {l : List α} :
      @[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} {i : Nat} {l : List α} :
      splitAt i l = (take i l, drop i l)

      rotateLeft #

      @[simp]
      theorem List.rotateLeft_zero {α : Type u_1} {l : List α} :

      rotateRight #

      @[simp]
      theorem List.rotateRight_zero {α : Type u_1} {l : List α} :