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} {n : Nat} {a : α} {l : List α} (h : 0 < n) :
List.take n (a :: l) = a :: List.take (n - 1) l
@[simp]
theorem List.drop_one {α : Type u_1} (l : List α) :
List.drop 1 l = l.tail
@[simp]
theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) :
@[simp]
theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) :
(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) :
List.drop i l = []
theorem List.length_lt_of_drop_ne_nil {α : Type u_1} {l : List α} {n : Nat} (h : List.drop n l []) :
n < l.length
theorem List.take_of_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
List.take i l = l
theorem List.lt_length_of_take_ne_self {α : Type u_1} {l : List α} {n : Nat} (h : List.take n l l) :
n < l.length
@[reducible, inline, deprecated List.drop_of_length_le]
abbrev List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
List.drop i l = []
Equations
Instances For
    @[reducible, inline, deprecated List.take_of_length_le]
    abbrev List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
    List.take i l = l
    Equations
    Instances For
      @[simp]
      theorem List.drop_length {α : Type u_1} (l : List α) :
      List.drop l.length l = []
      @[simp]
      theorem List.take_length {α : Type u_1} (l : List α) :
      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] :: List.drop (i + 1) l = List.drop i l
      @[deprecated List.getElem_cons_drop]
      theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin l.length) :
      l.get i :: List.drop (i + 1) l = List.drop (↑i) l
      theorem List.drop_eq_getElem_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) :
      List.drop n l = l[n] :: List.drop (n + 1) l
      @[deprecated List.drop_eq_getElem_cons]
      theorem List.drop_eq_get_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) :
      List.drop n l = l.get n, h :: List.drop (n + 1) l
      @[simp]
      theorem List.getElem?_take_of_lt {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) :
      (List.take n l)[m]? = l[m]?
      @[deprecated List.getElem?_take_of_lt]
      theorem List.get?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) :
      (List.take n l).get? m = l.get? m
      theorem List.getElem?_take_of_succ {α : Type u_1} {l : List α} {n : Nat} :
      (List.take (n + 1) l)[n]? = l[n]?
      @[simp]
      theorem List.drop_drop {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
      List.drop n (List.drop m l) = List.drop (n + m) l
      theorem List.take_drop {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
      @[deprecated List.drop_drop]
      theorem List.drop_add {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
      List.drop (m + n) l = List.drop m (List.drop n l)
      @[simp]
      theorem List.tail_drop {α : Type u_1} (l : List α) (n : Nat) :
      (List.drop n l).tail = List.drop (n + 1) l
      @[simp]
      theorem List.drop_tail {α : Type u_1} (l : List α) (n : Nat) :
      List.drop n l.tail = List.drop (n + 1) l
      @[simp]
      theorem List.drop_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} :
      List.drop k l = [] l.length k
      @[reducible, inline, deprecated List.drop_eq_nil_iff]
      abbrev List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} :
      List.drop k l = [] l.length k
      Equations
      Instances For
        @[simp]
        theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} :
        List.take k l = [] k = 0 l = []
        theorem List.drop_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
        as = []List.drop i as = []
        theorem List.ne_nil_of_drop_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.drop i as []) :
        as []
        theorem List.take_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
        as = []List.take i as = []
        theorem List.ne_nil_of_take_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.take i as []) :
        as []
        theorem List.set_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} {a : α} :
        List.take n (l.set m a) = (List.take n l).set m a
        theorem List.drop_set {α : Type u_1} {l : List α} {n : Nat} {m : Nat} {a : α} :
        List.drop n (l.set m a) = if m < n then List.drop n l else (List.drop n l).set (m - n) a
        theorem List.set_drop {α : Type u_1} {l : List α} {n : Nat} {m : Nat} {a : α} :
        (List.drop n l).set m a = List.drop n (l.set (n + m) a)
        theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
        (List.take i l).concat l[i] = List.take (i + 1) l
        @[deprecated List.take_succ_cons]
        theorem List.take_cons_succ :
        ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as
        @[deprecated List.take_of_length_le]
        theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length n) :
        List.take n l = l
        theorem List.drop_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
        List.drop l₁.length (l₁ ++ l₂) = l₂
        @[simp]
        theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) :
        List.drop n (l₁ ++ l₂) = l₂
        theorem List.take_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
        List.take l₁.length (l₁ ++ l₂) = l₁
        @[simp]
        theorem List.take_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) :
        List.take n (l₁ ++ l₂) = l₁
        theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} :
        List.take (n + 1) l = List.take n l ++ l[n]?.toList
        @[deprecated]
        theorem List.drop_sizeOf_le {α : Type u_1} [SizeOf α] (l : List α) (n : Nat) :
        theorem List.dropLast_eq_take {α : Type u_1} (l : List α) :
        l.dropLast = List.take (l.length - 1) l
        @[simp]
        theorem List.map_take {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :
        @[simp]
        theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :

        takeWhile and dropWhile #

        theorem List.takeWhile_cons {α : Type u_1} (p : αBool) (a : α) (l : List α) :
        List.takeWhile p (a :: l) = if p a = true then a :: List.takeWhile p l else []
        @[simp]
        theorem List.takeWhile_cons_of_pos {α : Type u_1} {p : αBool} {a : α} {l : List α} (h : p a = true) :
        @[simp]
        theorem List.takeWhile_cons_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (h : ¬p a = true) :
        List.takeWhile p (a :: l) = []
        theorem List.dropWhile_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
        List.dropWhile p (x :: xs) = if p x = true then List.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) :
        @[simp]
        theorem List.dropWhile_cons_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (h : ¬p a = true) :
        List.dropWhile p (a :: l) = a :: l
        theorem List.head?_takeWhile {α : Type u_1} (p : αBool) (l : List α) :
        (List.takeWhile p l).head? = Option.filter p l.head?
        theorem List.head_takeWhile {α : Type u_1} (p : αBool) (l : List α) (w : List.takeWhile p l []) :
        (List.takeWhile p l).head w = l.head
        theorem List.head?_dropWhile_not {α : Type u_1} (p : αBool) (l : List α) :
        match (List.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 : List.dropWhile p l []) :
        p ((List.dropWhile p l).head w) = false
        theorem List.takeWhile_map {α : Type u_1} {β : Type u_2} (f : αβ) (p : βBool) (l : List α) :
        theorem List.dropWhile_map {α : Type u_1} {β : Type u_2} (f : αβ) (p : βBool) (l : List α) :
        theorem List.takeWhile_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (p : βBool) (l : List α) :
        List.takeWhile p (List.filterMap f l) = List.filterMap f (List.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 α) :
        List.dropWhile p (List.filterMap f l) = List.filterMap f (List.dropWhile (fun (a : α) => Option.all p (f a)) l)
        theorem List.takeWhile_filter {α : Type u_1} (p : αBool) (q : αBool) (l : List α) :
        List.takeWhile q (List.filter p l) = List.filter p (List.takeWhile (fun (a : α) => !p a || q a) l)
        theorem List.dropWhile_filter {α : Type u_1} (p : αBool) (q : αBool) (l : List α) :
        List.dropWhile q (List.filter p l) = List.filter p (List.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 : List α} {ys : List α} :
        List.takeWhile p (xs ++ ys) = if (List.takeWhile p xs).length = xs.length then xs ++ List.takeWhile p ys else List.takeWhile p xs
        @[simp]
        theorem List.takeWhile_append_of_pos {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : ∀ (a : α), a l₁p a = true) :
        List.takeWhile p (l₁ ++ l₂) = l₁ ++ List.takeWhile p l₂
        theorem List.dropWhile_append {α : Type u_1} {p : αBool} {xs : List α} {ys : List α} :
        List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys
        @[simp]
        theorem List.dropWhile_append_of_pos {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : ∀ (a : α), a l₁p a = true) :
        List.dropWhile p (l₁ ++ l₂) = List.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) :
        List.takeWhile p (List.replicate n a) = if p a = true then List.replicate n a else []
        @[simp]
        theorem List.dropWhile_replicate_eq_filter_not {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
        List.dropWhile p (List.replicate n a) = List.filter (fun (a : α) => !p a) (List.replicate n a)
        theorem List.dropWhile_replicate {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
        List.dropWhile p (List.replicate n a) = if p a = true then [] else List.replicate n a
        theorem List.take_takeWhile {α : Type u_1} {l : List α} (p : αBool) (n : Nat) :
        @[simp]
        theorem List.all_takeWhile {α : Type u_1} {p : αBool} {l : List α} :
        (List.takeWhile p l).all p = true
        @[simp]
        theorem List.any_dropWhile {α : Type u_1} {p : αBool} {l : List α} :
        ((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) :
        (List.takeWhile p l).replace a b = List.takeWhile p (l.replace a b)

        splitAt #

        @[simp]
        theorem List.splitAt_eq {α : Type u_1} (n : Nat) (l : List α) :

        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