Documentation

Init.Data.List.Nat.TakeDrop

Further lemmas about List.take, List.drop, List.zip and List.zipWith. #

These are in a separate file from most of the list lemmas as they required importing more lemmas about natural numbers, and use omega.

take #

@[simp]
theorem List.length_take {α : Type u_1} (i : Nat) (l : List α) :
(List.take i l).length = min i l.length
theorem List.length_take_le {α : Type u_1} (n : Nat) (l : List α) :
(List.take n l).length n
theorem List.length_take_le' {α : Type u_1} (n : Nat) (l : List α) :
(List.take n l).length l.length
theorem List.length_take_of_le {n : Nat} :
∀ {α : Type u_1} {l : List α}, n l.length(List.take n l).length = n
theorem List.getElem_take {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (hi : i < L.length) (hj : i < j) :
L[i] = (List.take j L)[i]

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the big list to the small list.

theorem List.getElem_take' {α : Type u_1} (L : List α) {j : Nat} {i : Nat} {h : i < (List.take j L).length} :
(List.take j L)[i] = L[i]

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the small list to the big list.

@[deprecated List.getElem_take]
theorem List.get_take {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (hi : i < L.length) (hj : i < j) :
L.get i, hi = (List.take j L).get i,

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the big list to the small list.

@[deprecated List.getElem_take]
theorem List.get_take' {α : Type u_1} (L : List α) {j : Nat} {i : Fin (List.take j L).length} :
(List.take j L).get i = L.get i,

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the small list to the big list.

theorem List.getElem?_take_eq_none {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : n m) :
(List.take n l)[m]? = none
@[deprecated List.getElem?_take_eq_none]
theorem List.get?_take_eq_none {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : n m) :
(List.take n l).get? m = none
theorem List.getElem?_take_eq_if {α : Type u_1} {l : List α} {n : Nat} {m : Nat} :
(List.take n l)[m]? = if m < n then l[m]? else none
@[deprecated List.getElem?_take_eq_if]
theorem List.get?_take_eq_if {α : Type u_1} {l : List α} {n : Nat} {m : Nat} :
(List.take n l).get? m = if m < n then l.get? m else none
theorem List.head?_take {α : Type u_1} {l : List α} {n : Nat} :
(List.take n l).head? = if n = 0 then none else l.head?
theorem List.head_take {α : Type u_1} {l : List α} {n : Nat} (h : List.take n l []) :
(List.take n l).head h = l.head
theorem List.getLast?_take {α : Type u_1} {n : Nat} {l : List α} :
(List.take n l).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast?
theorem List.getLast_take {α : Type u_1} {n : Nat} {l : List α} (h : List.take n l []) :
(List.take n l).getLast h = l[n - 1]?.getD (l.getLast )
theorem List.take_take {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
theorem List.take_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (h : m < n) :
List.take m (l.set n a) = List.take m l
@[simp]
theorem List.take_replicate {α : Type u_1} (a : α) (n : Nat) (m : Nat) :
@[simp]
theorem List.drop_replicate {α : Type u_1} (a : α) (n : Nat) (m : Nat) :
theorem List.take_append_eq_append_take {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
List.take n (l₁ ++ l₂) = List.take n l₁ ++ List.take (n - l₁.length) l₂

Taking the first n elements in l₁ ++ l₂ is the same as appending the first n elements of l₁ to the first n - l₁.length elements of l₂.

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

Taking the first l₁.length + i elements in l₁ ++ l₂ is the same as appending the first i elements of l₂ to l₁.

@[simp]
theorem List.take_eq_take {α : Type u_1} {l : List α} {m : Nat} {n : Nat} :
List.take m l = List.take n l min m l.length = min n l.length
theorem List.take_add {α : Type u_1} (l : List α) (m : Nat) (n : Nat) :
theorem List.dropLast_take {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) :
(List.take n l).dropLast = List.take (n - 1) l
theorem List.map_eq_append_split {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {s₁ : List β} {s₂ : List β} (h : List.map f l = s₁ ++ s₂) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = s₁ List.map f l₂ = s₂

drop #

theorem List.lt_length_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < L.length) :
j < (List.drop i L).length
theorem List.getElem_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < L.length) :
L[i + j] = (List.drop i L)[j]

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the big list to the small list.

@[deprecated List.getElem_drop]
theorem List.get_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < L.length) :
L.get i + j, h = (List.drop i L).get j,

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the big list to the small list.

theorem List.getElem_drop' {α : Type u_1} (L : List α) {i : Nat} {j : Nat} {h : j < (List.drop i L).length} :
(List.drop i L)[j] = L[i + j]

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the small list to the big list.

@[deprecated List.getElem_drop']
theorem List.get_drop' {α : Type u_1} (L : List α) {i : Nat} {j : Fin (List.drop i L).length} :
(List.drop i L).get j = L.get i + j,

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the small list to the big list.

@[simp]
theorem List.getElem?_drop {α : Type u_1} (L : List α) (i : Nat) (j : Nat) :
(List.drop i L)[j]? = L[i + j]?
@[deprecated List.getElem?_drop]
theorem List.get?_drop {α : Type u_1} (L : List α) (i : Nat) (j : Nat) :
(List.drop i L).get? j = L.get? (i + j)
theorem List.head?_drop {α : Type u_1} (l : List α) (n : Nat) :
(List.drop n l).head? = l[n]?
theorem List.head_drop {α : Type u_1} {l : List α} {n : Nat} (h : List.drop n l []) :
(List.drop n l).head h = l[n]
theorem List.getLast?_drop {α : Type u_1} {n : Nat} {l : List α} :
(List.drop n l).getLast? = if l.length n then none else l.getLast?
theorem List.getLast_drop {α : Type u_1} {n : Nat} {l : List α} (h : List.drop n l []) :
(List.drop n l).getLast h = l.getLast
theorem List.drop_length_cons {α : Type u_1} {l : List α} (h : l []) (a : α) :
List.drop l.length (a :: l) = [l.getLast h]
theorem List.drop_append_eq_append_drop {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ List.drop (n - l₁.length) l₂

Dropping the elements up to n in l₁ ++ l₂ is the same as dropping the elements up to n in l₁, dropping the elements up to n - l₁.length in l₂, and appending them.

theorem List.drop_append_of_le_length {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : n l₁.length) :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ l₂
@[simp]
theorem List.drop_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (i : Nat) :
List.drop (l₁.length + i) (l₁ ++ l₂) = List.drop i l₂

Dropping the elements up to l₁.length + i in l₁ + l₂ is the same as dropping the elements up to i in l₂.

theorem List.set_eq_take_append_cons_drop {α : Type u_1} {l : List α} {n : Nat} {a : α} :
l.set n a = if n < l.length then List.take n l ++ a :: List.drop (n + 1) l else l
theorem List.exists_of_set {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l[n] :: l₂ l₁.length = n l.set n a' = l₁ ++ a' :: l₂
theorem List.drop_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (hnm : n < m) :
List.drop m (l.set n a) = List.drop m l
theorem List.drop_take {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
theorem List.take_reverse {α : Type u_1} {xs : List α} {n : Nat} (h : n xs.length) :
List.take n xs.reverse = (List.drop (xs.length - n) xs).reverse
@[reducible, inline, deprecated]
abbrev List.reverse_take {α : Type u_1} {xs : List α} {n : Nat} (h : n xs.length) :
List.take n xs.reverse = (List.drop (xs.length - n) xs).reverse
Equations
Instances For
    theorem List.drop_reverse {α : Type u_1} {xs : List α} {n : Nat} (h : n xs.length) :
    List.drop n xs.reverse = (List.take (xs.length - n) xs).reverse

    rotateLeft #

    @[simp]
    theorem List.rotateLeft_replicate {α : Type u_1} {m : Nat} (n : Nat) (a : α) :
    (List.replicate m a).rotateLeft n = List.replicate m a

    rotateRight #

    @[simp]
    theorem List.rotateRight_replicate {α : Type u_1} {m : Nat} (n : Nat) (a : α) :
    (List.replicate m a).rotateRight n = List.replicate m a

    zipWith #

    @[simp]
    theorem List.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (l₁ : List α) (l₂ : List β) :
    (List.zipWith f l₁ l₂).length = min l₁.length l₂.length
    theorem List.lt_length_left_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {i : Nat} {l : List α} {l' : List β} (h : i < (List.zipWith f l l').length) :
    i < l.length
    theorem List.lt_length_right_of_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {i : Nat} {l : List α} {l' : List β} (h : i < (List.zipWith f l l').length) :
    i < l'.length
    @[simp]
    theorem List.getElem_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {l : List α} {l' : List β} {i : Nat} {h : i < (List.zipWith f l l').length} :
    (List.zipWith f l l')[i] = f l[i] l'[i]
    theorem List.zipWith_eq_zipWith_take_min {α : Type u_1} {β : Type u_2} :
    ∀ {α_1 : Type u_3} {f : αβα_1} (l₁ : List α) (l₂ : List β), List.zipWith f l₁ l₂ = List.zipWith f (List.take (min l₁.length l₂.length) l₁) (List.take (min l₁.length l₂.length) l₂)
    theorem List.reverse_zipWith :
    ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1}, l.length = l'.length(List.zipWith f l l').reverse = List.zipWith f l.reverse l'.reverse
    @[reducible, inline, deprecated List.reverse_zipWith]
    abbrev List.zipWith_distrib_reverse :
    ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1}, l.length = l'.length(List.zipWith f l l').reverse = List.zipWith f l.reverse l'.reverse
    Equations
    Instances For
      @[simp]
      theorem List.zipWith_replicate {α : Type u_1} {β : Type u_2} :
      ∀ {α_1 : Type u_3} {f : αβα_1} {a : α} {b : β} {m n : Nat}, List.zipWith f (List.replicate m a) (List.replicate n b) = List.replicate (min m n) (f a b)

      zip #

      @[simp]
      theorem List.length_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
      (l₁.zip l₂).length = min l₁.length l₂.length
      theorem List.lt_length_left_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {l : List α} {l' : List β} (h : i < (l.zip l').length) :
      i < l.length
      theorem List.lt_length_right_of_zip {α : Type u_1} {β : Type u_2} {i : Nat} {l : List α} {l' : List β} (h : i < (l.zip l').length) :
      i < l'.length
      @[simp]
      theorem List.getElem_zip {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {i : Nat} {h : i < (l.zip l').length} :
      (l.zip l')[i] = (l[i], l'[i])
      theorem List.zip_eq_zip_take_min {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
      l₁.zip l₂ = (List.take (min l₁.length l₂.length) l₁).zip (List.take (min l₁.length l₂.length) l₂)
      @[simp]
      theorem List.zip_replicate {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m : Nat} {n : Nat} :
      (List.replicate m a).zip (List.replicate n b) = List.replicate (min m n) (a, b)