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.

@[simp]

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 {α : 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]

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 α) : List.take n (List.take m l) = List.take (min n m) l

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) : List.take n (List.replicate m a) = List.replicate (min n m) a

@[simp]

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

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

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

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

@[reducible, inline, deprecated List.map_eq_append_iff]

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

Equations

• @List.map_eq_append_split = @List.map_eq_append_iff

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

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

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

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.

@[simp]

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.mem_take_iff_getElem {α : Type u_1} {n : Nat} {l : List α} {a : α} : a ∈ List.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 ∈ List.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) : (List.drop n l).head? = l[n]?

@[simp]

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?

@[simp]

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

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

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

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

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

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

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

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

findIdx

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

@[simp]

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

@[simp]

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

@[simp]

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

takeWhile

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

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

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

• @List.zipWith_distrib_reverse = @List.reverse_zipWith

@[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)