List.ext_nthLe
theorem List.ext_nthLe :
∀ {α : Type u} {l₁ l₂ : List α},
l₁.length = l₂.length →
(∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nthLe n h₁ = l₂.nthLe n h₂) → l₁ = l₂
The theorem `List.ext_nthLe` states that for any two lists `l₁` and `l₂` of the same type `α`, if the lengths of the two lists are equal, and for every natural number `n` less than the length of the lists, the `n`th element of `l₁` and `n`th element of `l₂` are equal, then the two lists `l₁` and `l₂` are the same. This theorem essentially asserts that two lists are equal if they have the same length and their corresponding elements are identical.
More concisely: If two lists of the same type have equal lengths and agree in their first `n` elements for all `n < length`, then they are equal.
|
List.lookmap_map_eq
theorem List.lookmap_map_eq :
∀ {α : Type u} {β : Type v} (f : α → Option α) (g : α → β),
(∀ (a b : α), b ∈ f a → g a = g b) → ∀ (l : List α), List.map g (List.lookmap f l) = List.map g l
This theorem states that for any types `α` and `β`, and any two functions `f : α → Option α` and `g : α → β`, if for every pair of `α` elements `a` and `b` such that `b` is in the option returned by `f(a)`, `g(a)` equals `g(b)`, then for any list `l` of elements of type `α`, the result of applying `g` to each element of the list obtained by applying `lookmap` with `f` to `l` is equal to the result of directly applying `g` to each element of `l`. Essentially, this theorem asserts the preservation of the mapping `g` on a list even after a `lookmap` operation with `f` on the list, under certain conditions on `f` and `g`.
More concisely: If `f : α -> Option α` and `g : α -> β` are functions such that `g(a) = g(b)` whenever `b` is in the option returned by `f(a)`, then `map (lookmap f) l = map g l`.
|
List.Sublist.map
theorem List.Sublist.map :
∀ {α : Type u} {β : Type v} (f : α → β) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.map f l₁).Sublist (List.map f l₂)
The theorem `List.Sublist.map` states that for any two lists `l₁` and `l₂` of type `α` and a function `f` from `α` to `β`, if `l₁` is a sublist of `l₂`, then the list obtained by mapping `f` over `l₁` is a sublist of the list obtained by mapping `f` over `l₂`. In other words, if `l₁` is a sublist of `l₂`, then applying the same function to each element of both lists preserves the sublist relationship.
More concisely: If `l₁` is a sublist of `l₂`, then `map f l₁` is a sublist of `map f l₂` for any function `f` from `α` to `β`.
|
List.map_const
theorem List.map_const :
∀ {α : Type u} {β : Type v} (l : List α) (b : β), List.map (Function.const α b) l = List.replicate l.length b := by
sorry
The theorem `List.map_const` states that for any list `l` of type `α` and any element `b` of type `β`, if you map a function that is a constant `b` over the list `l`, you get an equally long list filled solely with the element `b`. In other words, applying the constant function `b` to each element of `l` produces a list that is equivalent to replicating `b` for the length of `l`.
More concisely: For any list `l` and constant `b`, the application of the function `map (λ x => b) l` equals the list `repeat b (length l)`.
|
Function.LeftInverse.list_map
theorem Function.LeftInverse.list_map :
∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
Function.LeftInverse f g → Function.LeftInverse (List.map f) (List.map g)
The theorem `Function.LeftInverse.list_map` states that for any two types `α` and `β`, and any two functions `f : α → β` and `g : β → α`, if `g` is a left inverse to `f`, then `List.map g` is a left inverse to `List.map f`. In other words, if applying `g` after `f` returns the original input (i.e., `g ∘ f = id`), then applying `List.map g` after `List.map f` on any list will return the original list.
More concisely: If functions `f : α → β` and `g : β → α` satisfy `g ∘ f = id_{\alpha}`, then `List.map g ∘ List.map f = id_{List α}`.
|
List.Sublist.antisymm
theorem List.Sublist.antisymm : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.Sublist l₁ → l₁ = l₂
This theorem, `List.Sublist.antisymm`, states that for all types `α` and any pair of lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂` and `l₂` is a sublist of `l₁`, then `l₁` must be equal to `l₂`. In other words, the sublist relation on lists of any given type is antisymmetric: it cannot be the case that two different lists are sublists of each other.
More concisely: If `l₁` is a sublist of `l₂` and `l₂` is a sublist of `l₁`, then `l₁` = `l₂`.
|
List.splitAt_eq_take_drop
theorem List.splitAt_eq_take_drop :
∀ {α : Type u} (n : ℕ) (l : List α), List.splitAt n l = (List.take n l, List.drop n l)
The theorem `List.splitAt_eq_take_drop` states that for any list `l` of a certain type `α` and any natural number `n`, splitting the list `l` at the index `n` is equivalent to creating a pair of lists where the first list is the result of taking the first `n` elements of `l` and the second list is the result of dropping the first `n` elements from `l`. In other words, the theorem describes how splitting a list at a certain position can be viewed as taking and dropping elements from the list.
More concisely: For any list `l` of type `α` and natural number `n`, `List.splitAt n l = (take n l, drop n l)`.
|
List.dropLast_append_getLast
theorem List.dropLast_append_getLast : ∀ {α : Type u} {l : List α} (h : l ≠ []), l.dropLast ++ [l.getLast h] = l := by
sorry
This theorem states that for any non-empty list `l` of elements of an arbitrary type `α`, if you remove the last element of `l` and then append the last element of `l` back, you will get back the original list `l`. In mathematical terms, if $l$ is a non-empty list, then $dropLast(l) ++ [getLast(l)] = l$, where $dropLast$ removes the last element from the list, $getLast$ fetches the last element from the list, and $++$ denotes concatenation of lists.
More concisely: For any non-empty list `l` of type `α`, the list obtained by removing the last element and the list obtained by appending the last element to the result of removing the last element are equal: `dropLast (l) ++ [getLast (l)] = l`.
|
List.indexOf_lt_length
theorem List.indexOf_lt_length :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, List.indexOf a l < l.length ↔ a ∈ l
This theorem, `List.indexOf_lt_length`, states that for any type `α` with decidable equality, any element `a` of type `α`, and any list `l` of elements of type `α`, the index of the first occurrence of `a` in `l` is less than the length of `l` if and only if `a` is an element of `l`. In other words, if `a` is in the list `l`, then its index should be a valid index within the list, and conversely, if the index of `a` is a valid index within the list, then `a` must be in the list.
More concisely: For any type `α` with decidable equality, list `l` of length `n` over `α`, and element `a` of `α`, if `a` is in list `l`, then its index in `l` is less than `n`, and conversely.
|
List.ne_nil_of_length_pos
theorem List.ne_nil_of_length_pos : ∀ {α : Type u_1} {l : List α}, 0 < l.length → l ≠ []
This theorem, `List.ne_nil_of_length_pos`, is an alias for the forward direction of `List.length_pos`. It states that for any list `l` of any type `α`, if the length of `l` is greater than 0, then `l` cannot be an empty list. In other words, no list whose length is positive can be empty.
More concisely: If a list `l` of type `α` has positive length, then `l` is not the empty list.
|
List.sublist_nil_iff_eq_nil
theorem List.sublist_nil_iff_eq_nil : ∀ {α : Type u_1} {l : List α}, l.Sublist [] ↔ l = []
This theorem, `List.sublist_nil_iff_eq_nil`, states that for any list `l` of a certain type `α`, `l` is a sublist of an empty list if and only if `l` itself is an empty list. In other words, a list is a sublist of the empty list only when it is also an empty list.
More concisely: A list of type α is a sublist of the empty list if and only if it is an empty list.
|
List.indexOf_get
theorem List.indexOf_get :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α} (h : List.indexOf a l < l.length),
l.get ⟨List.indexOf a l, h⟩ = a
This theorem, `List.indexOf_get`, states that for any type `α` with decidable equality and any element `a` of type `α` in a list `l` of elements of type `α`, if the index of `a` in the list `l` is less than the length of the list `l`, then getting the element at the index of `a` in the list `l` returns `a`. In other words, if `a` is present in `l`, then the element at the position returned by the `indexOf` function is `a` itself.
More concisely: For any type `α` with decidable equality and any list `l` of length `n` and element `a` in `α` present at index `i` in `l` with `i < n`, we have `l.get i = a`.
|
List.map_congr
theorem List.map_congr :
∀ {α : Type u} {β : Type v} {f g : α → β} {l : List α}, (∀ x ∈ l, f x = g x) → List.map f l = List.map g l := by
sorry
The theorem `List.map_congr` states that for any two functions `f` and `g` from type `α` to type `β`, and for any list `l` of type `α`, if `f` and `g` give the same result for all elements in `l`, then the result of mapping `f` over `l` is the same as the result of mapping `g` over `l`. In other words, if two functions agree on the elements of a list, then their map over the list also agrees.
More concisely: If two functions agree on every element of a list, then applying them with `List.map` yields the same output.
|
List.splitOnP_eq_single
theorem List.splitOnP_eq_single :
∀ {α : Type u} (p : α → Bool) (xs : List α), (∀ x ∈ xs, ¬p x = true) → List.splitOnP p xs = [xs]
The theorem `List.splitOnP_eq_single` states that for any given list `xs` of elements of an arbitrary type `α` and a predicate `p` of type `α → Bool`, if no element in the list `xs` satisfies the predicate `p` (i.e., `p x` is not true for any `x` in `xs`), then the result of the function `List.splitOnP p xs` will be a list consisting of the original list `xs` as its only element. In other words, if none of the elements in the list cause the function `p` to return true, the list is not split and is returned as is within a list.
More concisely: If `p` does not hold for any element in list `xs`, then `List.splitOnP p xs` equals `[xs]`.
|
List.of_mem_filter
theorem List.of_mem_filter : ∀ {α : Type u} {p : α → Bool} {a : α} {l : List α}, a ∈ List.filter p l → p a = true := by
sorry
The theorem `List.of_mem_filter` states that for any type `α`, any predicate function `p` from `α` to Boolean, any element `a` of type `α` and any list `l` of type `α`, if `a` is an element of the list obtained by filtering `l` with the predicate `p`, then the predicate `p` applied to `a` must be true. In other words, any element present in the filtered list must satisfy the condition laid out by the filtering function.
More concisely: For any type `α`, list `l` of `α`, element `a` in the filtered list `l|p`, the predicate `p(a)` holds true.
|
List.reverse_injective
theorem List.reverse_injective : ∀ {α : Type u}, Function.Injective List.reverse
The theorem `List.reverse_injective` states that for any type `α`, the function `List.reverse`, which reverses a list, is injective. In other words, if `List.reverse` of two lists are equal, then the two original lists must be identical. This injectiveness property ensures that no information is lost when a list is reversed, and each reversed list has a unique original list that it came from.
More concisely: For any type α, the function List.reverse from lists of α to lists of α is an injection.
|
List.splitOnP_spec
theorem List.splitOnP_spec :
∀ {α : Type u} (p : α → Bool) (as : List α),
(List.zipWith (fun x x_1 => x ++ x_1) (List.splitOnP p as)
(List.map (fun x => [x]) (List.filter p as) ++ [[]])).join =
as
This theorem, `List.splitOnP_spec`, states that for any list of elements `as` of some type `α` and any predicate `p` that returns a boolean value when applied to elements of the list, the original list `as` can be reconstructed. The reconstruction is done by first applying `splitOnP p` to `as` to split the list at every element satisfying the predicate `p`. The elements satisfying `p` are then filtered out from `as` and each is put in its own list using `List.map`. An empty list is appended to this list of lists. This modified filtered list is then combined with the list of split lists using `List.zipWith` to concatenate corresponding pairs of lists. Finally, all the lists are joined using `List.join`. Hence, the theorem shows that the process of splitting a list on a predicate and filtering elements satisfying the same predicate is reversible.
More concisely: Given a list `as` of length `n` and a predicate `p`, the function `List.splitOnP p` followed by `List.map` and filtering elements satisfying `p`, and finally `List.join` and concatenation of the resulting lists, is the inverse operation of the original list partitioning using the same predicate.
|
List.nthLe_map_rev
theorem List.nthLe_map_rev :
∀ {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} (H : n < l.length),
f (l.nthLe n H) = (List.map f l).nthLe n ⋯
This theorem, `List.nthLe_map_rev`, establishes an important property about mapping a function over a list in Lean 4. For any function `f` from type `α` to type `β`, and any list `l` of elements of type `α`, and a natural number `n` such that `n` is less than the length of the list `l`, applying the function `f` to the `n`th element of the list `l` (as given by the `nthLe` function) is equivalent to first mapping the function `f` over all elements of the list `l` and then taking the `n`th element of the resultant list. In effect, this theorem states that the order of mapping and taking the `n`th element doesn't matter.
More concisely: For any function `f` and natural number `n`, the `n`th element of the list obtained by applying `f` to each element of another list is equal to applying `f` to the `n`th element of the original list.
|
List.mem_split
theorem List.mem_split : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ s t, l = s ++ a :: t
This theorem, `List.mem_split`, states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, if `a` is an element of `l`, then there exist two lists `s` and `t` such that `l` can be expressed as the concatenation of `s`, the singleton list containing `a`, and `t`. In other words, if an element is in a list, then the list can be split into two parts: one part before the occurrence of the element and one part after.
More concisely: If `α` is a type, `a` is an element of list `l` of type `α`, then `l` can be expressed as `s :: [a] :: t` for some lists `s` and `t`.
|
List.cons_head!_tail
theorem List.cons_head!_tail : ∀ {α : Type u} [inst : Inhabited α] {l : List α}, l ≠ [] → l.head! :: l.tail = l := by
sorry
The theorem `List.cons_head!_tail` states that for any type `α` and any inhabited list `l` of type `α` that is not empty, the list obtained by prepending the head of `l` (using the `List.head!` function) to the tail of `l` (using the `List.tail` function) is equal to `l` itself. Essentially, it asserts that taking apart a non-empty list into its head and tail and then putting them back together results in the original list.
More concisely: For any non-empty list `l` of type `α`, `List.cons (List.head! l) (List.tail l) = l`.
|
List.append_cons_inj_of_not_mem
theorem List.append_cons_inj_of_not_mem :
∀ {α : Type u} {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α},
a₂ ∉ x₁ → a₂ ∉ z₁ → (x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂)
This theorem states that for any two lists, `l₁` and `l₂`, each containing a specific element `a₁` and `a₂` respectively in their midst: `l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`. If the specific element `a₂` is not present in either `x₁` or `z₁`, then the two lists `l₁` and `l₂` are equal if and only if the respective parts of the lists are equal, i.e., (`x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂`). In simpler terms, if the specific element from the second list is not found in the first list's parts, then the two lists are identical if the pieces from which they are composed are identical.
More concisely: Given lists `l₁ = x₁ ++ [a₁] ++ z₁` and `l₂ = x₂ ++ [a₂] ++ z₂`, if `a₂ ∉ x₁ ∪ z₁`, then `l₁ = l₂` if and only if `x₁ = x₂`, `a₁ = a₂`, and `z₁ = z₂`.
|
List.mem_pmap
theorem List.mem_pmap :
∀ {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a} {b : β},
b ∈ List.pmap f l H ↔ ∃ a, ∃ (h : a ∈ l), f a ⋯ = b
This theorem, `List.mem_pmap`, states that for any two types `α` and `β`, a predicate `p` over `α`, a function `f` from `α` and a proof of `p a` to `β`, a list `l` of type `α`, a proof `H` that for all `a` in `l`, `p a` holds, and a value `b` of type `β`, `b` is in the list produced by applying `f` to each element of `l` (along with the proof that the predicate holds for that element), if and only if there exists an `a` in `l` such that `f` applied to `a` and the proof that `p a` holds is equal to `b`. In other words, `b` is an element of the `pmap` of `f` over `l` if and only if `b` is the result of `f` applied to some `a` in `l`.
More concisely: For any types `α` and `β`, predicate `p` over `α`, function `f` from `α` to `β`, list `l` of type `α`, proof `H` that `p a` holds for all `a` in `l`, and value `b` of type `β`, `b` is in the image of `pmap(f)(l)` if and only if there exists an `a` in `l` such that `b = f(a) * p(a)`.
|
List.map_const'
theorem List.map_const' :
∀ {α : Type u} {β : Type v} (l : List α) (b : β), List.map (fun x => b) l = List.replicate l.length b
The theorem `List.map_const'` states that for any list `l` of type `α` and any element `b` of type `β`, if we map over the list `l` and replace each element with `b`, we will get a new list that is the same as replicating the element `b` for the length of the original list `l`. This means that replacing each element in a list with a constant value is equivalent to creating a new list filled with that constant, with the same length as the original list.
More concisely: For any list `l` of length `n` and any element `b`, the list obtained by applying the map function with constant argument `b` to `l` is equal to the list of length `n` consisting only of `b`.
|
List.splitOn_intercalate
theorem List.splitOn_intercalate :
∀ {α : Type u} (ls : List (List α)) [inst : DecidableEq α] (x : α),
(∀ l ∈ ls, x ∉ l) → ls ≠ [] → List.splitOn x ([x].intercalate ls) = ls
The theorem `List.splitOn_intercalate` states that for any type `α` with decidable equality, any non-empty list `ls` of lists of `α` and any element `x` of `α`, as long as `x` does not appear in any of the lists in `ls`, the function `splitOn x` acts as the left inverse of `intercalate [x]`. In other words, if we first intercalate `ls` with `x` (insert `x` between each pair of adjacent lists in `ls`) and then split the result on `x`, we get back `ls`.
More concisely: For any type `α` with decidable equality, if `xs` is a non-empty list of lists of `α` with no occurrence of `x` in any sublist, then `splitOn x (intercalate [x] xs) = xs`.
|
List.nthLe_map'
theorem List.nthLe_map' :
∀ {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} (H : n < (List.map f l).length),
(List.map f l).nthLe n H = f (l.nthLe n ⋯)
The theorem `List.nthLe_map'` states that for any types `α` and `β`, given a function `f` from `α` to `β`, a list `l` of type `α`, and an integer `n` with the condition that `n` is less than the length of the list obtained by applying `f` to each element of `l`, the `n`-th element of the mapped list is equal to the result of applying `f` to the `n`-th element of the original list. This theorem describes a property of the `map` function in the context of accessing elements at specific locations in the list.
More concisely: For any types `α` and `β`, function `f` from `α` to `β`, list `l` of length `n+1` over `α`, and integer `n`, if `0 ≤ n`, then `(List.map f l).nth n = f (l.nth n)`.
|
List.mem_map_of_injective
theorem List.mem_map_of_injective :
∀ {α : Type u} {β : Type v} {f : α → β},
Function.Injective f → ∀ {a : α} {l : List α}, f a ∈ List.map f l ↔ a ∈ l
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, if `f` is injective (i.e., if for any two elements `x` and `y` from `α`, `f(x) = f(y)` implies `x = y`), and for any element `a` from `α` and any list `l` of elements from `α`, then `f(a)` is an element of the list obtained by applying `f` to each element of `l` if and only if `a` is an element of `l`. In other words, under the condition that `f` is injective, an element `a` is in the list `l` if and only if its image under `f` is in the image of the list under the mapping `f`.
More concisely: For any injective function `f` from type `α` to type `β`, and for any list `l` of elements from `α`, an element `a` from `α` is in `l` if and only if `f(a)` is in the image of `l` under `f`.
|
List.append_left_cancel
theorem List.append_left_cancel : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = as ++ cs → bs = cs
This theorem, `List.append_left_cancel`, states that for any type `α` and any lists `as`, `bs`, and `cs` of this type, if the concatenation of `as` and `bs` is equal to the concatenation of `as` and `cs`, then `bs` must be equal to `cs`. In other words, if the left parts of two concatenated lists are the same, then the right parts of these lists must also be the same.
More concisely: If `as` is a list and `bs` and `cs` are lists such that `as ++ bs` = `as ++ cs`, then `bs` = `cs`.
|
List.intercalate_splitOn
theorem List.intercalate_splitOn :
∀ {α : Type u} (xs : List α) (x : α) [inst : DecidableEq α], [x].intercalate (List.splitOn x xs) = xs
The theorem `List.intercalate_splitOn` states that for any given list `xs` of elements of an arbitrary type `α` and an element `x` of the same type `α`, where `α` is equipped with a procedure for deciding equality between its elements (`DecidableEq α`), the operation of splitting the list `xs` at every occurrence of the element `x` using the `splitOn x` function and then subsequently joining the resulting lists together with `x` in-between them using the `intercalate [x]` function, will result in the original list `xs`. Simply put, `intercalate [x]` is the left inverse operation of `splitOn x` on lists.
More concisely: For any list `xs` of equal elements `α` with decidable equality, the operation of splitting `xs` at every occurrence of an element `x` using `splitOn x` and then intercalating `x` between the resulting lists using `intercalate [x]` results in the original list `xs`. In other words, `list.intercalate (list.map (list.cons x) (list.init (splitOn x xs))) (list.tail (splitOn x xs)) = xs`.
|
Mathlib.Data.List.Basic._auxLemma.22
theorem Mathlib.Data.List.Basic._auxLemma.22 : ∀ {α : Type u} {l : List α}, (l.getLast?.isSome = true) = (l ≠ []) := by
sorry
This theorem states that for any type `α`, the `List.reverse` function, which reverses a list, is injective. This means that if the reversed lists are equal, i.e., `List.reverse(as1) = List.reverse(as2)`, then the original lists must have been equal, i.e., `as1 = as2`, thus asserting the uniqueness of the input to the `List.reverse` function based on its output.
More concisely: If `as1` and `as2` are lists of the same type `α`, then `List.reverse as1 = List.reverse as2` implies `as1 = as2`.
|
List.eq_nil_of_subset_nil
theorem List.eq_nil_of_subset_nil : ∀ {α : Type u_1} {l : List α}, l ⊆ [] → l = []
This theorem, known as "List.eq_nil_of_subset_nil", states that for any type `α` and list `l` of type `α`, if `l` is a subset of an empty list, then `l` must be an empty list itself. It's an alias for the forward direction of the `List.subset_nil` theorem in Lean 4.
More concisely: If `l` is a list of type `α` and `l` is a subset of the empty list `[]`, then `l` is equal to the empty list `[]`.
|
List.length_pos_of_ne_nil
theorem List.length_pos_of_ne_nil : ∀ {α : Type u_1} {l : List α}, l ≠ [] → 0 < l.length
This theorem, referred to as "Alias of the reverse direction of `List.length_pos`", states that for any type `α` and any list `l` of type `α`, if `l` is not an empty list (i.e., `l ≠ []`), then the length of `l` (denoted by `List.length l`) is greater than 0 (i.e., `0 < List.length l`). This is just another way of saying that any non-empty list has a positive length.
More concisely: For any list `l` of type `α` in Lean, if `l` is non-empty (`l ≠ []`), then `0 < List.length l`.
|
List.splitOnP_first
theorem List.splitOnP_first :
∀ {α : Type u} (p : α → Bool) (xs : List α),
(∀ x ∈ xs, ¬p x = true) →
∀ (sep : α), p sep = true → ∀ (as : List α), List.splitOnP p (xs ++ sep :: as) = xs :: List.splitOnP p as
The theorem `List.splitOnP_first` states that for any type `α`, given a predicate function `p` of type `α → Bool`, a list `xs` of type `List α`, and an element `sep` of type `α`, if none of the elements in `xs` satisfy the predicate `p` (i.e., `p x` is not `true` for any `x` in `xs`), and `sep` does satisfy `p` (i.e., `p sep` equals `true`), then for any list `as` of type `List α`, when we split the concatenated list `xs ++ sep :: as` on `p`, the result is `xs` followed by the result of splitting `as` on `p`. In other words, splitting a list at a certain element ignores the elements before the separator that don't satisfy the predicate.
More concisely: For any list `xs` of type `List α`, element `sep` of type `α`, and predicate `p` of type `α → Bool`, if `p x` is false for all `x` in `xs` and `p sep` is true, then splitting `xs ++ [sep]` at `p` yields `xs` followed by the sublist of elements in the split of `[sep] :: as` at `p`, where `as` is the remaining part of the original list.
|
List.map_comp_map
theorem List.map_comp_map :
∀ {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β), List.map g ∘ List.map f = List.map (g ∘ f) := by
sorry
The theorem `List.map_comp_map` states that for any three types `α`, `β`, and `γ`, and for any two functions `g : β → γ` and `f : α → β`, the composition of mapping function `g` after mapping function `f` over a list is equivalent to a single map operation using the composed function `(g ∘ f)`. This is essentially expressing the property of the function composition in the context of list mapping operations.
More concisely: For any functions `f : α → β` and `g : β → γ`, and any list `xs : List α`, `List.map (g ∘ f) xs` is equal to `List.map g (List.map f xs)`.
|
List.length_pmap
theorem List.length_pmap :
∀ {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a},
(List.pmap f l H).length = l.length
The theorem `List.length_pmap` states that for any types `α` and `β`, any property `p` of elements of type `α`, and any function `f` from elements of type `α` satisfying the property `p` to elements of type `β`, and any list `l` of elements of type `α` such that each element in `l` satisfies the property `p`, the length of the list obtained by applying the function `f` to each element of `l` (given by `List.pmap f l H`) is the same as the length of the original list `l`. This means that applying the function `f` to each element of `l` using `List.pmap` does not change the length of the list.
More concisely: For any type `α`, property `p` on `α`, function `f : α → β` preserving `p`, and list `l : List α` of elements satisfying `p`, the length of `List.pmap f l` equals the length of `l`.
|
List.pmap_eq_map_attach
theorem List.pmap_eq_map_attach :
∀ {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ a ∈ l, p a),
List.pmap f l H = List.map (fun x => f ↑x ⋯) l.attach
This theorem, `List.pmap_eq_map_attach`, states that for any types `α` and `β`, a predicate `p : α → Prop`, a function `f : (a : α) → p a → β`, a list `l` of type `List α`, and a proof `H` that for all elements `a` in `l`, `p a` holds, the process of applying `f` to every element in `l` along with the proof `H` (i.e., `List.pmap f l H`) is equivalent to first attaching each element of `l` to its proof that it belongs to `l` (i.e., `List.attach l`) and then applying `f` to these pairs. The latter process involves applying `f` to the elements and "unpacking" them from the subtype `{x // x ∈ l}` back to the original type `α` using the coercion function `↑x`.
More concisely: For any type `α`, predicate `p : α → Prop`, function `f : (a : α) → p a → β`, list `l : List α`, and proof `H : ∀ a ∈ l, p a`, `List.pmap f l H` is equivalent to `List.attach l ▸ List.map (λ x ▸ (x, rfl)) (List.map p l) ▸ List.map (λ x, f x rfl) (List.map (λ x, ⟨x, rfl⟩) l)`.
|
List.reverse_involutive
theorem List.reverse_involutive : ∀ {α : Type u}, Function.Involutive List.reverse
The theorem `List.reverse_involutive` states that the `List.reverse` function is involutive for any type `α`. In other words, for any list of elements from type `α`, applying `List.reverse` twice returns the original list. The term "involutive" here refers to a function that is its own inverse, i.e., applying the function twice to any argument yields the original argument. This property is often written as `f(f(x)) = x` for all `x` in the domain of `f`. In this case, `f` is the `List.reverse` function.
More concisely: For any list `l` of type `α`, `List.reverse (List.reverse l)` equals `l`.
|
List.attach_map_coe'
theorem List.attach_map_coe' :
∀ {α : Type u} {β : Type v} (l : List α) (f : α → β), List.map (fun i => f ↑i) l.attach = List.map f l
This theorem states that for any list of elements of type `α` (denoted `l`) and any function `f` from `α` to `β`, mapping the function `f` over the attached version of `l` (where each element is paired with a proof that it belongs to `l`) and then taking the underlying value (using `↑i`) gives the same result as directly mapping `f` over `l`. In other words, attaching proofs of membership to the elements of `l` does not change the result of mapping `f` over `l`.
More concisely: For any list `l` of elements of type `α` and any function `f` from `α` to `β`, the application of `f` to the underlying values of the paired elements in the attached version of `l` is equal to the direct application of `f` to `l`.
|
List.foldl_assoc
theorem List.foldl_assoc :
∀ {α : Type u} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α},
List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)
The theorem `List.foldl_assoc` states that for any type `α`, any binary operation `op` on `α` which is associative, any list `l` of type `α`, and any two elements `a₁` and `a₂` of type `α`, the result of folding the list `l` from the left using `op` with initial accumulator `op a₁ a₂` is the same as applying `op` to `a₁` and the result of folding the list `l` from the left using `op` with initial accumulator `a₂`. This essentially says that the fold operation commutes with the associative operation `op`.
More concisely: For any associative binary operation `op` on type `α`, and any lists `l` of type `α` and elements `a₁, a₂` of type `α`, `List.foldl op a₁ (a₂ :: l) = op a₁ (List.foldl op a₂ l)`.
|
List.replicate_add
theorem List.replicate_add :
∀ {α : Type u} (m n : ℕ) (a : α), List.replicate (m + n) a = List.replicate m a ++ List.replicate n a
The theorem `List.replicate_add` states that for any type `α`, given two natural numbers `m` and `n`, and an element `a` of type `α`, if we replicate `a` `(m + n)` times, it will result in the same list as if we first replicate `a` `m` times, and then replicate `a` `n` times, and finally concatenate these two lists. In other words, replicating `a` by the sum of two numbers is equivalent to replicating `a` by each of these numbers separately and then concatenating the results.
More concisely: For any type `α` and natural numbers `m` and `n`, `List.replicate m (List.replicate n a) = List.replicate (m + n) a`.
|
List.map_pmap
theorem List.map_pmap :
∀ {α : Type u} {β : Type v} {γ : Type w} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (l : List α)
(H : ∀ a ∈ l, p a), List.map g (List.pmap f l H) = List.pmap (fun a h => g (f a h)) l H
The theorem `List.map_pmap` states that for any types `α`, `β`, and `γ`, a predicate `p : α → Prop`, a function `g : β → γ`, a function `f : (a : α) → p a → β`, a list `l : List α`, and a proof `H` that the predicate `p` holds for every element in list `l`, the operation of mapping function `g` over the result of partially mapping function `f` over list `l` (given by `List.pmap f l H`) is equivalent to partially mapping the composition of `g` and `f` over list `l` (given by `List.pmap (fun a h => g (f a h)) l H`). In simpler terms, this theorem shows the commutativity of the operations of mapping and partial mapping under certain conditions.
More concisely: For any types `α`, `β`, and `γ`, and functions `f : α → β → β`, `g : β → γ`, `p : α → Prop`, given a list `l : List α` and a proof `H` that `p` holds for every element in `l`, `List.pmap_map l H (f ∘ g)` is equivalent to `List.pmap (λ a h, g (f a h)) l H`.
|
List.nthLe_of_mem
theorem List.nthLe_of_mem : ∀ {α : Type u} {a : α} {l : List α}, a ∈ l → ∃ n, ∃ (h : n < l.length), l.nthLe n h = a
This theorem states that for any list `l` of elements of some type `α`, and any element `a` of the same type, if `a` is an element of `l` (denoted as `a ∈ l`), then there exists an index `n` such that `n` is less than the length of the list, and the `n`-th element of the list (obtained using the `List.nthLe` function) is `a`. In essence, the theorem provides a guarantee that if an element is in the list, then we can find its position within the list.
More concisely: For any list `l` of length `n+1` over type `α`, and any `a ∈ α`, there exists an index `i` < `n` such that `l.get! i = a`. (Here, `get!` is the function provided by Lean's standard library to access an element of a list by index.)
|
List.map_replicate
theorem List.map_replicate :
∀ {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (a : α), List.map f (List.replicate n a) = List.replicate n (f a)
The theorem `List.map_replicate` states that for any types `α` and `β`, a function `f` from `α` to `β`, a natural number `n` and a value `a` of type `α`, applying `f` to each element of a list that consists of `n` copies of `a` results in a new list that consists of `n` copies of `f(a)`. In other terms, it is saying that mapping a function over a list that has been created by replicating a value `n` times is the same as replicating the function applied to the value `n` times.
More concisely: For any types `α` and `β`, function `f` from `α` to `β`, natural number `n`, and value `a` of type `α`, `List.map (λ x => f x) (List.repeat a n) = List.repeat (f a) n`.
|
List.disjoint_pmap
theorem List.disjoint_pmap :
∀ {α : Type u_2} {β : Type u_3} {p : α → Prop} {f : (a : α) → p a → β} {s t : List α} (hs : ∀ a ∈ s, p a)
(ht : ∀ a ∈ t, p a),
(∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') →
s.Disjoint t → (List.pmap f s hs).Disjoint (List.pmap f t ht)
The theorem `List.disjoint_pmap` states that for any given types `α` and `β`, a predicate `p` on `α`, a function `f` from `α` to `β` that is only defined when `p a` is true, and two lists `s` and `t` of type `α`, if for every element `a` in `s` and `t`, `p a` is true, and if for any two elements `a` and `a'` where `p a` and `p a'` are true, `f a ha` being equal to `f a' ha'` implies `a = a'`, then if the lists `s` and `t` are disjoint, the lists obtained by applying the function `f` via partial mapping (pmap) to the lists `s` and `t` are also disjoint. In other words, the disjointness property is preserved under the partial mapping operation with function `f`.
More concisely: If two lists of the same type, when restricted to elements satisfying a given predicate, are disjoint and for any equal elements, the image under a function defined only on those elements is equal, then the image lists obtained by applying the function via partial mapping are also disjoint.
|
List.pmap_eq_map
theorem List.pmap_eq_map :
∀ {α : Type u} {β : Type v} (p : α → Prop) (f : α → β) (l : List α) (H : ∀ a ∈ l, p a),
List.pmap (fun a x => f a) l H = List.map f l
The theorem `List.pmap_eq_map` states that for any types `α` and `β`, a predicate `p` on `α`, a function `f` from `α` to `β`, and a list `l` of type `α` with the property that the predicate `p` holds for every element in the list `l`, the `pmap` function of the list `l`, which applies the function `f` to each element in `l` (using a proof that the predicate `p` holds for each element), is equal to the `map` function of the list `l`, where `f` is applied to each element. In other words, if we know that every element of a list satisfies a certain property, then applying a function to each element of the list while simultaneously proving the property is equivalent to simply applying the function to each element of the list.
More concisely: For any types `α` and `β`, if `l` is a list of `α` such that `p(x)` holds for all `x` in `l`, then `List.pmap f l` equals `List.map f l`, where `p` is a predicate on `α` and `f` is a function from `α` to `β`.
|
Mathlib.Data.List.Basic._auxLemma.24
theorem Mathlib.Data.List.Basic._auxLemma.24 : ∀ {α : Type u_1} {a b : α}, (some a = some b) = (a = b)
This theorem, `Mathlib.Data.List.Basic._auxLemma.24`, states that for all types `α` and all lists `l` of type `α`, the function `Option.isNone` applied to the result of the function `List.getLast?` on `l` is equal to `true` if and only if the list `l` is empty. In other words, the last element of a list cannot be retrieved (and the retrieval results in `none`) if and only if the list is empty.
More concisely: The theorem `Mathlib.Data.List.Basic._auxLemma.24` in Lean 4 states that the last element of an empty list is `none` (i.e., `Option.isNone (List.getLast? l)` holds if and only if `l` is empty.
|
List.disjoint_map
theorem List.disjoint_map :
∀ {α : Type u_2} {β : Type u_3} {f : α → β} {s t : List α},
Function.Injective f → s.Disjoint t → (List.map f s).Disjoint (List.map f t)
The theorem `List.disjoint_map` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any lists `s` and `t` of type `α`, if `f` is an injective function (that is, a function where each input has a unique output) and `s` and `t` are disjoint lists (that is, their intersection is the empty list), then the lists obtained by applying `f` to each element of `s` and `t` are also disjoint. This is a generalization of the property that the image of disjoint sets under an injective function are disjoint.
More concisely: If `f` is an injective function from type `α` to type `β` and lists `s` and `t` of type `α` are disjoint, then the images of `s` and `t` under `f` are also disjoint lists.
|
Mathlib.Data.List.Basic._auxLemma.5
theorem Mathlib.Data.List.Basic._auxLemma.5 :
∀ {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α}, (b ∈ l.bind f) = ∃ a ∈ l, b ∈ f a
The theorem `Mathlib.Data.List.Basic._auxLemma.5` states that for any types `α` and `β`, any function `f` from `α` to a list of `β`, any element `b` of type `β`, and any list `l` of type `α`, the condition that `b` is an element of the result of applying the `bind` operation on `l` with `f` is equivalent to the existence of an element `a` in `l` such that `b` is an element of the list produced by applying `f` to `a`. Essentially, it is stating that an element is in the list produced by binding `f` over `l` if and only if it exists in a list produced by applying `f` to some element in `l`.
More concisely: For any types `α` and `β`, and functions `f : α → list β`, element `b : β`, and list `l : list α`, the element `b ∈ bind f l` if and only if there exists `a ∈ l` such that `b ∈ f a`.
|
List.nthLe_of_eq
theorem List.nthLe_of_eq :
∀ {α : Type u} {L L' : List α} (h : L = L') {i : ℕ} (hi : i < L.length), L.nthLe i hi = L'.nthLe i ⋯
This theorem is about list manipulation in the context of Lean's mathematical logic. Specifically, it says that if you have a reference to the ith element of a list `L` in a formula, and you have a proof `h` that `L` is equal to another list `L'`, you cannot directly rewrite `L` to `L'` in the formula using `rw h`. This is because the original proof `hi` demonstrates that `i` is less than the length of `L`, not `L'`. However, you can utilize the lemma `nth_le_of_eq` to perform this rewrite, by using `rw (nth_le_of_eq h)`. The theorem proves that under these circumstances, the ith element of `L` and `L'` are indeed the same.
More concisely: The theorem states that when proving an equality of lists `L = L'` in Lean, you cannot directly replace `L` with `L'` when `L` appears as a reference to the ith element of the list, but you can use the `nth_le_of_eq` lemma to establish the equality of the ith elements instead.
|
List.length_attach
theorem List.length_attach : ∀ {α : Type u} (L : List α), L.attach.length = L.length
This theorem, named `List.length_attach`, asserts that for any list `L` of type `α`, the length of the list obtained by attaching to each element of `L` the proof that it belongs to `L` (i.e., the list `List.attach L`) is equal to the length of `L` itself. In other terms, attaching proofs of membership to the elements of a list does not change the length of the list.
More concisely: The length of `List.attach` a list `L` of type `α` is equal to the length of `L`.
|
List.isEmpty_iff_eq_nil
theorem List.isEmpty_iff_eq_nil : ∀ {α : Type u} {l : List α}, l.isEmpty = true ↔ l = []
This theorem, `List.isEmpty_iff_eq_nil`, states that for any type `α` and for any list `l` of `α`, the function `List.isEmpty` returns `true` if and only if the list `l` is an empty list. In other words, it establishes a bi-directional relationship between the list being empty and the `List.isEmpty` function returning `true`.
More concisely: For any type α, List.isEmpty (l : List α) if and only if l is an empty list.
|
List.indexOf_cons_ne
theorem List.indexOf_cons_ne :
∀ {α : Type u} [inst : DecidableEq α] {a b : α} (l : List α),
b ≠ a → List.indexOf a (b :: l) = (List.indexOf a l).succ
This theorem, `List.indexOf_cons_ne`, asserts that for any type `α` with decidable equality, and any two elements `a` and `b` of this type, as well as any list `l` of elements of type `α`, if `b` is not equal to `a`, then the index of `a` in the list that starts with `b` followed by `l` is one more than the index of `a` in the list `l`. In simpler terms, if you have a list and the first element is not the one you're looking for, the index of the element you're seeking in the whole list is one more than the index in the rest of the list.
More concisely: For any type `α` with decidable equality, if `b ≠ a` and `l` is a list of length `n+1` over `α` with `b` as its head, then the index of `a` in `l` is `n` if it is in `l`, and `n+1` otherwise.
|
List.mem_of_mem_filter
theorem List.mem_of_mem_filter : ∀ {α : Type u} {p : α → Bool} {a : α} {l : List α}, a ∈ List.filter p l → a ∈ l := by
sorry
The theorem `List.mem_of_mem_filter` states that for any type `α`, any boolean function `p` from `α` to `Bool`, any element `a` of type `α`, and any list `l` of elements of type `α`, if the element `a` is a member of the list obtained by filtering `l` with the function `p`, then `a` is also a member of the original list `l`. In other words, filtering a list does not introduce any new elements into the list.
More concisely: If `a` is in the list obtained by filtering `l` with `p`, then `a` is in `l`.
|
List.attach_map_val
theorem List.attach_map_val : ∀ {α : Type u} (l : List α), List.map Subtype.val l.attach = l
The theorem `List.attach_map_val` states that for any list `l` of any type `α`, when we "attach" to each element of `l` the proof that it belongs to `l` to produce a new list (using `List.attach`), and then apply the function `Subtype.val` (which retrieves the underlying element in the base type) to each element of this new list (using `List.map`), we recover the original list `l`. In other words, attaching and then retrieving the underlying elements is an identity operation on lists.
More concisely: For any list `l` of type `α`, the application of `List.map (Subtype.val)` to `List.attach l id` equals `l`, where `id` is the identity function.
|
List.eq_replicate_length
theorem List.eq_replicate_length :
∀ {α : Type u} {a : α} {l : List α}, l = List.replicate l.length a ↔ ∀ b ∈ l, b = a
This theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, the list `l` equals the list obtained by replicating the element `a` for the length of the list `l` if and only if every element `b` in the list `l` is equal to `a`. In other words, a list is identical to a list made by repeating a single element for the length of the list if and only if every element in the original list is that single element.
More concisely: For any type `α`, list `l` of length `n` over `α`, and element `a` of `α`, the list `l` equals the repeated list `[a | _ | _ ... | a]` of length `n` if and only if `l` equals the list `[a] ^ n`, where `^` denotes list repetition.
|
List.sublist_cons_of_sublist
theorem List.sublist_cons_of_sublist : ∀ {α : Type u} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → l₁.Sublist (a :: l₂)
This theorem states that for any type `α`, given an element `a` of type `α` and two lists `l₁` and `l₂` of type `List α`, if `l₁` is a sublist of `l₂`, then `l₁` is also a sublist of the list formed by prepending `a` to `l₂`. Essentially, adding an element to the start of a list doesn't affect its sublists.
More concisely: If `l₁` is a sublist of `l₂`, then `a :: l₁` is a sublist of `a :: l₂`, where `::` denotes list cons.
|
List.get_map_rev
theorem List.get_map_rev :
∀ {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : Fin l.length}, f (l.get n) = (List.map f l).get ⟨↑n, ⋯⟩
This theorem, `List.get_map_rev`, states that for any function `f` from type `α` to type `β`, a list `l` of type `α`, and a valid index `n` into the list, applying `f` to the `n`th element of `l` is the same as first transforming `l` using `f` and then getting the `n`th element. In other words, for a list `l` and a function `f`, the operation of first applying `f` and then picking out an element is identical to first picking out an element and then applying `f`.
More concisely: For any list `l` of length `n+1` and function `f` from type `α` to type `β`, `(get (n) (map f l)) = (map f (get (n) l))`.
|
List.singleton_injective
theorem List.singleton_injective : ∀ {α : Type u}, Function.Injective fun a => [a]
The theorem `List.singleton_injective` states that for all types `α`, the function which takes an element `a` of type `α` and maps it to a singleton list containing `a` is injective. In other words, if two singleton lists are equal, then their elements must also be equal. This is a property of the singleton list function: no two distinct values can map to the same list, ensuring the function's injectivity.
More concisely: For any type α, the function mapping each element to the singleton list containing that element is an injection.
|
List.map_join
theorem List.map_join :
∀ {α : Type u} {β : Type v} (f : α → β) (L : List (List α)), List.map f L.join = (List.map (List.map f) L).join
The theorem `List.map_join` states that for any type α and β, and any function `f` from α to β, if `L` is a list of lists of type α, then mapping `f` over the joined list `L` is the same as first mapping `f` over each individual list in `L`, and then joining the resulting lists. In essence, this theorem captures the property that the order of joining the lists and applying the function does not matter - the result will be the same. This is a property of the `map` and `join` functions in functional programming, similar to the distributive law in algebra.
More concisely: For any type α and β, and any function f from α to β, the mapping of f over the joined list of lists L of type α is equal to the joined lists of the mappings of f over each individual list in L.
|
List.map_injective_iff
theorem List.map_injective_iff :
∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (List.map f) ↔ Function.Injective f
This theorem states that for all types `α` and `β`, and a given function `f` from `α` to `β`, the function `List.map f`, which applies `f` to each element of a list, is injective if and only if the function `f` itself is injective. In other words, if applying `f` to each element of a list doesn't change the relative uniqueness of elements (if two different elements in the list give two different results when passed through `f`), then `f` must also have this property when applied to any individual elements of `α`. Similarly, if `f` is injective, then so is `List.map f`.
More concisely: For all types `α` and `β`, and functions `f : α → β`, the function `List.map f` is an injection if and only if `f` is an injection.
|
List.append_right_cancel
theorem List.append_right_cancel : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = cs ++ bs → as = cs
This theorem, `List.append_right_cancel`, is an alias of `List.append_cancel_right` and states that for any type `α` and any lists `as`, `bs`, and `cs` of type `α`, if the result of appending list `bs` to `as` is equal to the result of appending `bs` to `cs`, then `as` must be equal to `cs`. In other words, if two lists become equal after appending the same list to both, the two original lists must have been equal.
More concisely: If for lists `as`, `bs`, and `cs` of type `α`, `as ++ bs` = `cs ++ bs` implies `as` = `cs`, then.
|
List.Sublist.cons_cons
theorem List.Sublist.cons_cons : ∀ {α : Type u} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)
This theorem states that for any type `α`, any two lists `l₁` and `l₂` of type `α`, and any element `a` of type `α`, if `l₁` is a sublist of `l₂`, then the list obtained by consing `a` onto `l₁` is a sublist of the list obtained by consing `a` onto `l₂`. In other words, prepending the same element to both the sublist and the larger list preserves the sublist relationship.
More concisely: If `l₁` is a sublist of `l₂` in type `α`, then consing `a` to `l₁` results in a sublist of consing `a` to `l₂`. In mathematical notation, `l₁ ⊆ l₂` implies `a :: l₁ ⊆ a :: l₂`.
|
List.map_reverse
theorem List.map_reverse :
∀ {α : Type u} {β : Type v} (f : α → β) (l : List α), List.map f l.reverse = (List.map f l).reverse
This theorem states that for any function 'f' from type 'α' to type 'β' and any list 'l' of type 'α', mapping 'f' over the reverse of 'l' yields the same result as reversing the list obtained by mapping 'f' over 'l'. In simple terms, it says that reversing a list and then applying a function to each element is the same as applying the function first and then reversing the list.
More concisely: For any function f from type α to type β and any list l of type α, the list obtained by applying f to the reverse of l is the reverse of the list obtained by applying f to each element of l.
|
List.pmap_congr
theorem List.pmap_congr :
∀ {α : Type u} {β : Type v} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (l : List α)
{H₁ : ∀ a ∈ l, p a} {H₂ : ∀ a ∈ l, q a},
(∀ a ∈ l, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → List.pmap f l H₁ = List.pmap g l H₂
This theorem establishes that for any two functions `f` and `g` from an element of a list `l` and a proof that it satisfies a property `p` or `q` respectively to a type `β`, if for each element in the list `l`, `f` applied to this element and a proof that it satisfies `p` is equivalent to `g` applied to this element and a proof that it satisfies `q`, then the lists resulting from applying `List.pmap` with `f` and `g` to `l` are equal. `List.pmap` is a function that applies a function to each element of a list along with a proof that this element satisfies a certain property.
More concisely: If for all `x : α` and proofs `p` and `q` that `x` satisfies `p` and `q` respectively, `f x p ≡ g x q` implies `List.pmap f (List.filter p l) = List.pmap g (List.filter q l)`, where `f : α → β`, `g : α → β`, `l : list α`, and `List.filter`, `List.pmap`, `≡` denote the filtering, pointwise mapping, and equality operations on lists and functions, respectively.
|
List.sublist_of_cons_sublist_cons
theorem List.sublist_of_cons_sublist_cons :
∀ {α : Type u} {l₁ l₂ : List α} {a : α}, (a :: l₁).Sublist (a :: l₂) → l₁.Sublist l₂
This theorem states that for any type `α` and any lists `l₁` and `l₂` of type `α`, along with any element `a` of type `α`, if `l₁` with `a` prepended is a sublist of `l₂` with `a` prepended, then `l₁` is a sublist of `l₂`. In other words, if prepending the same element does not change the sublist relationship between two lists, then the original lists had the same relationship without the prepended element.
More concisely: If `l₁` is a sublist of `l₂` implies that `a :: l₁` is a sublist of `a :: l₂`, where `::` denotes list prepending and `α` is any type.
|
List.head!_mem_self
theorem List.head!_mem_self : ∀ {α : Type u} [inst : Inhabited α] {l : List α}, l ≠ [] → l.head! ∈ l
The theorem `List.head!_mem_self` states that for all types `α` that are inhabited, and for any list `l` of type `α`, if `l` is not an empty list, then the head of the list (obtained by `List.head! l`) is an element of `l`. This means we can always retrieve the first element from a non-empty list and that element will certainly be a part of the list.
More concisely: For all inhabited types `α` and non-empty lists `l` of `α`, the head element of `l` is an element of `l`.
|
List.map_bind
theorem List.map_bind :
∀ {α : Type u} {β : Type v} {γ : Type w} (g : β → List γ) (f : α → β) (l : List α),
(List.map f l).bind g = l.bind fun a => g (f a)
The theorem `List.map_bind` states that for any types `α`, `β`, and `γ`, and for any functions `g` from `β` to `List γ` and `f` from `α` to `β`, and for any list `l` of type `List α`, the operation of first mapping `f` over the list `l` and then binding the result with `g` is equivalent to the operation of binding the list `l` with the function that applies `f` to an element and then applies `g` to the result. This theorem is a property of the `List` monad and is analogous to the monad law of associativity.
More concisely: For any types `α`, `β`, and `γ`, and functions `f: α → β` and `g: β → List γ`, the application of `List.map` with `f` followed by `List.bind` with `g` on a list `l` of type `List α` is equal to the application of `List.bind` with the composite function `x ↦ f x >> g` on list `l`.
|
List.comp_map
theorem List.comp_map :
∀ {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α),
List.map (h ∘ g) l = List.map h (List.map g l)
This theorem, called `List.comp_map`, states that for any list `l` of elements of some type `α`, and any two functions `g` mapping from `α` to another type `β`, and `h` mapping from `β` to a third type `γ`, the operation of first mapping `l` through `g`, then mapping the result through `h` (i.e., `List.map h (List.map g l)`) is the same as first composing `h` and `g` and then mapping `l` through the resulting function `h ∘ g` (i.e., `List.map (h ∘ g) l`). This is essentially a statement about the commutativity of function composition and mapping over a list.
More concisely: For any list `l` of elements from type `α`, and functions `g : α → β` and `h : β → γ`, `List.map (h ∘ g) l` is equal to `List.map h (List.map g l)`.
|
List.splitOnP_cons
theorem List.splitOnP_cons :
∀ {α : Type u} (p : α → Bool) (x : α) (xs : List α),
List.splitOnP p (x :: xs) =
if p x = true then [] :: List.splitOnP p xs else List.modifyHead (List.cons x) (List.splitOnP p xs)
This theorem, `List.splitOnP_cons`, is about splitting a list based on a certain condition in Lean 4. It takes a type variable `α`, a Boolean function `p` applied to elements of type `α`, an element `x` of type `α`, and a list `xs` of elements of type `α`.
The theorem states that if we call the function `List.splitOnP` on a list that starts with the element `x` and then contains the elements of `xs`, the result depends on the evaluation of the function `p` on `x`. If `p x` is true, then the list will be split at `x` (which is excluded from the resulting sublists), and the function is then recursively applied to the rest of the list `xs`. If `p x` is not true, `x` is added to the head of each of the sublists resulting from splitting the rest of the list `xs` based on the condition `p`.
More concisely: Given a type `α` and a Boolean function `p` on `α`, the list `xs` split at `x` using `List.splitOnP` in Lean 4 results in sublists where `x` is excluded if `p x` is true, and `x` is added to each sublist if `p x` is false.
|
List.getLast_cons
theorem List.getLast_cons : ∀ {α : Type u} {a : α} {l : List α} (h : l ≠ []), (a :: l).getLast ⋯ = l.getLast h := by
sorry
The `List.getLast_cons` theorem states that for any type `α`, any element `a` of type `α`, and any list `l` of type `α` that is not empty, the last element of the list formed by prepending `a` to `l` is the same as the last element of `l`. In other words, adding an element to the beginning of a non-empty list does not change what the last element of the list is.
More concisely: For any type `α` and non-empty list `l` of type `α`, appending an element `a` to the front of `l` does not change the last element of the list. In symbols, `last (a :: l) = last l`.
|
Mathlib.Data.List.Basic._auxLemma.33
theorem Mathlib.Data.List.Basic._auxLemma.33 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem asserts the principle of symmetry in equality for any sort of object. Specifically, it states that for any sort of object `α` and any two instances `a` and `b` of that sort, the proposition that `a` equals `b` is identical to the proposition that `b` equals `a`. In other words, equality is commutative; it doesn't matter in which order we compare two instances of a sort, the result will be the same.
More concisely: For any type `α` and elements `a` and `b` of type `α`, the equality `a = b` is equivalent to `b = a`.
|
List.indexOf_nthLe
theorem List.indexOf_nthLe :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α} (h : List.indexOf a l < l.length),
l.nthLe (List.indexOf a l) h = a
This theorem states that for any given type `α` with decidable equality and any given list `l` of type `α`, if the index of an element `a` in `l` is less than the length of `l`, then the nth element of `l` at this index is `a`. In other words, if we obtain the index of an element `a` in `l` and it is a valid index (i.e., less than the length of `l`), then fetching the element at this index from `l` will give us `a` back.
More concisely: For any decidably equal type `α` and list `l` of length `n` over `α`, if `i` is a valid index (i.e., `0 ≤ i < n`), then `l.get! i = a` where `a` is the element at index `i` in `l`.
|