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.

take

@[reducible, inline]

abbrev List.take_succ_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

Equations

• @List.take_succ_cons = @List.take_cons_succ

@[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.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length ≤ n) : List.take n l = l

@[simp]

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

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_take {α : Type u_1} (n : Nat) (m : Nat) (l : List α) : List.take n (List.take m l) = List.take (min n m) l

theorem List.take_replicate {α : Type u_1} (a : α) (n : Nat) (m : Nat) : List.take n (List.replicate m a) = List.replicate (min n m) a

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

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₁.

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.

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.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.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.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

@[simp]

theorem List.nth_take_of_succ {α : Type u_1} {l : List α} {n : Nat} : (List.take (n + 1) l).get? n = l.get? n

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

@[simp]

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

@[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) : List.take (m + n) l = List.take m l ++ List.take n (List.drop m l)

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.dropLast_eq_take {α : Type u_1} (l : List α) : l.dropLast = List.take l.length.pred l

theorem List.dropLast_take {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : (List.take n l).dropLast = List.take n.pred 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

@[simp]

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

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.drop_sizeOf_le {α : Type u_1} [SizeOf α] (l : List α) (n : Nat) : sizeOf (List.drop n l) ≤ sizeOf l

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.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.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.get?_drop {α : Type u_1} (L : List α) (i : Nat) (j : Nat) : (List.drop i L).get? j = L.get? (i + j)

@[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 α) : List.take n (List.drop m l) = List.drop m (List.take (m + n) l)

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

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

theorem 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

@[simp]

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_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

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 ≠ []

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

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