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 α) : (take i l).length = min i l.length

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

theorem List.length_take_le' {α : Type u_1} (n : Nat) (l : List α) : (take n l).length ≤ l.length

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

theorem List.getElem_take' {α : Type u_1} (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : L[i] = (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.

@[simp]

theorem List.getElem_take {α : Type u_1} (L : List α) {j i : Nat} {h : i < (take j L).length} : (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.

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

theorem List.getElem?_take {α : Type u_1} {l : List α} {n m : Nat} : (take n l)[m]? = if m < n then l[m]? else none

theorem List.head?_take {α : Type u_1} {l : List α} {n : Nat} : (take n l).head? = if n = 0 then none else l.head?

theorem List.head_take {α : Type u_1} {l : List α} {n : Nat} (h : take n l ≠ []) : (take n l).head h = l.head ⋯

theorem List.getLast?_take {α : Type u_1} {n : Nat} {l : 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 : take n l ≠ []) : (take n l).getLast h = l[n - 1]?.getD (l.getLast ⋯)

theorem List.take_take {α : Type u_1} (n m : Nat) (l : List α) : take n (take m l) = take (min n m) l

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

@[simp]

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

@[simp]

theorem List.drop_replicate {α : Type u_1} (a : α) (n m : Nat) : drop n (replicate m a) = replicate (m - n) a

theorem List.take_append_eq_append_take {α : Type u_1} {l₁ l₂ : List α} {n : Nat} : take n (l₁ ++ l₂) = take n l₁ ++ 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₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) : take n (l₁ ++ l₂) = take n l₁

theorem List.take_append {α : Type u_1} {l₁ l₂ : List α} (i : Nat) : take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ 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 n : Nat} : take m l = take n l ↔ min m l.length = min n l.length

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

theorem List.take_one {α : Type u_1} {l : List α} : take 1 l = l.head?.toList

theorem List.dropLast_take {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : (take n l).dropLast = take (n - 1) l

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

abbrev List.map_eq_append_split {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → β} : map f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Equations

• @List.map_eq_append_split = @List.map_eq_append_iff

theorem List.take_eq_dropLast {α : Type u_1} {l : List α} {i : Nat} (h : i + 1 = l.length) : take i l = l.dropLast

theorem List.take_prefix_take_left {α : Type u_1} (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l

theorem List.take_sublist_take_left {α : Type u_1} (l : List α) {m n : Nat} (h : m ≤ n) : (take m l).Sublist (take n l)

theorem List.take_subset_take_left {α : Type u_1} (l : List α) {m n : Nat} (h : m ≤ n) : take m l ⊆ take n l

drop

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

theorem List.getElem_drop' {α : Type u_1} (L : List α) {i j : Nat} (h : i + j < L.length) : L[i + j] = (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.

@[simp]

theorem List.getElem_drop {α : Type u_1} (L : List α) {i j : Nat} {h : j < (drop i L).length} : (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.

@[simp]

theorem List.getElem?_drop {α : Type u_1} (L : List α) (i j : Nat) : (drop i L)[j]? = L[i + j]?

theorem List.mem_take_iff_getElem {α : Type u_1} {n : Nat} {l : List α} {a : α} : a ∈ take n l ↔ ∃ (i : Nat), ∃ (hm : i < min n l.length), l[i] = a

theorem List.mem_drop_iff_getElem {α : Type u_1} {n : Nat} {l : List α} {a : α} : a ∈ drop n l ↔ ∃ (i : Nat), ∃ (hm : i + n < l.length), l[n + i] = a

@[simp]

theorem List.head?_drop {α : Type u_1} (l : List α) (n : Nat) : (drop n l).head? = l[n]?

@[simp]

theorem List.head_drop {α : Type u_1} {l : List α} {n : Nat} (h : drop n l ≠ []) : (drop n l).head h = l[n]

theorem List.getLast?_drop {α : Type u_1} {n : Nat} {l : List α} : (drop n l).getLast? = if l.length ≤ n then none else l.getLast?

@[simp]

theorem List.getLast_drop {α : Type u_1} {n : Nat} {l : List α} (h : drop n l ≠ []) : (drop n l).getLast h = l.getLast ⋯

theorem List.drop_length_cons {α : Type u_1} {l : List α} (h : l ≠ []) (a : α) : drop l.length (a :: l) = [l.getLast h]

theorem List.drop_append_eq_append_drop {α : Type u_1} {l₁ l₂ : List α} {n : Nat} : drop n (l₁ ++ l₂) = drop n l₁ ++ 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₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) : drop n (l₁ ++ l₂) = drop n l₁ ++ l₂

@[simp]

theorem List.drop_append {α : Type u_1} {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l₁ ++ l₂) = 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 take n l ++ a :: 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 m : Nat} (l : List α) (hnm : n < m) : drop m (l.set n a) = drop m l

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

theorem List.take_reverse {α : Type u_1} {xs : List α} {n : Nat} : take n xs.reverse = (drop (xs.length - n) xs).reverse

theorem List.drop_reverse {α : Type u_1} {xs : List α} {n : Nat} : drop n xs.reverse = (take (xs.length - n) xs).reverse

theorem List.reverse_take {α : Type u_1} {l : List α} {n : Nat} : (take n l).reverse = drop (l.length - n) l.reverse

theorem List.reverse_drop {α : Type u_1} {l : List α} {n : Nat} : (drop n l).reverse = take (l.length - n) l.reverse

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

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

theorem List.drop_sub_one {α : Type u_1} {l : List α} {n : Nat} (h : 0 < n) : drop (n - 1) l = l[n - 1]?.toList ++ drop n l

findIdx

theorem List.false_of_mem_take_findIdx {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} (h : x ∈ take (findIdx p xs) xs) : p x = false

@[simp]

theorem List.findIdx_take {α : Type u_1} {xs : List α} {n : Nat} {p : α → Bool} : findIdx p (take n xs) = min n (findIdx p xs)

@[simp]

theorem List.findIdx?_take {α : Type u_1} {xs : List α} {n : Nat} {p : α → Bool} : findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun (i : Nat) => i < n)

@[simp]

theorem List.min_findIdx_findIdx {α : Type u_1} {xs : List α} {p q : α → Bool} : min (findIdx p xs) (findIdx q xs) = findIdx (fun (a : α) => p a || q a) xs

takeWhile

theorem List.takeWhile_eq_take_findIdx_not {α : Type u_1} {xs : List α} {p : α → Bool} : takeWhile p xs = take (findIdx (fun (a : α) => !p a) xs) xs

theorem List.dropWhile_eq_drop_findIdx_not {α : Type u_1} {xs : List α} {p : α → Bool} : dropWhile p xs = drop (findIdx (fun (a : α) => !p a) xs) xs

rotateLeft

@[simp]

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

rotateRight

@[simp]

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

zipWith

@[simp]

theorem List.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l₁ : List α) (l₂ : 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 < (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 < (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 < (zipWith f l l').length} : (zipWith f l l')[i] = f l[i] l'[i]

theorem List.zipWith_eq_zipWith_take_min {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} (l₁ : List α) (l₂ : List β) : zipWith f l₁ l₂ = zipWith f (take (min l₁.length l₂.length) l₁) (take (min l₁.length l₂.length) l₂)

theorem List.reverse_zipWith {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} (h : l.length = l'.length) : (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

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

abbrev List.zipWith_distrib_reverse {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : α✝ → α✝¹ → α✝²} {l : List α✝} {l' : List α✝¹} (h : l.length = l'.length) : (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Equations

• @List.zipWith_distrib_reverse = @List.reverse_zipWith

@[simp]

theorem List.zipWith_replicate {α : Type u_1} {β : Type u_2} {α✝ : Type u_3} {f : α → β → α✝} {a : α} {b : β} {m n : Nat} : zipWith f (replicate m a) (replicate n b) = 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₂ = (take (min l₁.length l₂.length) l₁).zip (take (min l₁.length l₂.length) l₂)

@[simp]

theorem List.zip_replicate {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : Nat} : (replicate m a).zip (replicate n b) = replicate (min m n) (a, b)