List.mem_iff_get
theorem List.mem_iff_get : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ n, l.get n = a
This theorem states that for any given type `α`, an element `a` of type `α`, and a list `l` of elements of type `α`, `a` is a member of `l` if and only if there exists an index `n` such that the `n`-th element of the list `l` is `a`. Essentially, this theorem connects list membership with the existence of a specific index where the element can be found in the list.
More concisely: For any type `α`, list `l` of length `n` in `α`, and element `a` in `α`, `a ∈ l` if and only if there exists an index `i` in `{0, 1, ..., n-1}` such that `l(i) = a`.
|
List.map_map
theorem List.map_map :
∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} (g : β → γ) (f : α → β) (l : List α),
List.map g (List.map f l) = List.map (g ∘ f) l
The theorem `List.map_map` states that for any list `l` of elements of some type `α`, and any two functions `f : α → β` and `g : β → γ`, applying `f` to each element in `l` using `List.map` and then applying `g` to the result using `List.map` is equivalent to applying the function `g ∘ f` to each element in `l` using `List.map`. This is an example of function composition in the context of lists.
More concisely: For any lists `l` of elements from type `α`, and functions `f : α → β` and `g : β → γ`, `List.map (g ∘ f) l` is equivalent to `(List.map g (List.map f l))`.
|
List.mem_map
theorem List.mem_map :
∀ {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α}, b ∈ List.map f l ↔ ∃ a ∈ l, f a = b
This theorem, `List.mem_map`, states that for any two types `α` and `β`, a function `f` from `α` to `β`, a list `l` of type `α`, and an element `b` of type `β`, `b` is an element of the list obtained by applying `f` to each element of `l` if and only if there exists an element `a` in the original list `l` such that `f a` equals `b`. In other words, `b` is in the mapped list if there is an element in the original list that is mapped to `b` by the function `f`.
More concisely: For any function `f` from type `α` to type `β`, list `l` of type `α`, and element `b` of type `β`, `b` is in the image of `l` under `f` if and only if there exists an element `a` in `l` such that `f(a) = b`.
|
List.foldl_append
theorem List.foldl_append :
∀ {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (l l' : List α),
List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'
The theorem `List.foldl_append` states that for all types `α` and `β`, and for any function `f` of type `β → α → β`, any element `b` of type `β`, and any two lists `l` and `l'` of type `List α`, folding `f` over the concatenation of `l` and `l'` starting with `b`, is equivalent to folding `f` over `l'`, but starting with the result of folding `f` over `l` starting with `b`. In mathematical terms, `foldl f b (l ++ l') = foldl f (foldl f b l) l'`. This is a property of how folding a function over a list interacts with list concatenation.
More concisely: For all types `α` and `β` and functions `f` of type `β → α → β`, the composition of folding `f` over list `l` starting with `b` and then concatenating list `l'`, is equivalent to folding `f` over list `l'` starting with the result of folding `f` over `l` starting with `b`. In mathematical notation: `(∀ α β, (∀ (f : β → α → β), foldl f b (l ++ l') = foldl f (foldl f b l) l')`.
|
List.mem_filter
theorem List.mem_filter :
∀ {α : Type u_1} {x : α} {p : α → Bool} {as : List α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true
The theorem `List.mem_filter` states that for any type `α`, any element `x` of type `α`, any boolean function `p` from `α`, and any list `as` of type `α`, `x` is an element of the list obtained by filtering `as` with the function `p` if and only if `x` is an element of `as` and `p(x)` is true. In other words, an item is in the filtered list precisely when it is in the original list and it satisfies the filtering condition.
More concisely: For any type `α`, list `as` of `α`, element `x` of `α`, and boolean function `p` on `α`, `x ∈ List.filter p as` if and only if `x ∈ as` and `p(x) = true`.
|
List.map_append
theorem List.map_append :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ l₂ : List α),
List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
The theorem `List.map_append` states that for any two lists `l₁` and `l₂` of the same type `α`, and any function `f` from `α` to another type `β`, applying the `map` function with `f` to the append operation of `l₁` and `l₂` is the same as appending the results of applying `map` with `f` to `l₁` and `l₂` separately. That is, the mapping function distributes over the append operation for lists. In mathematical notation, this can be expressed as `map(f, l₁ ++ l₂) = map(f, l₁) ++ map(f, l₂)`.
More concisely: For any lists `l₁`, `l₂` of type `α` and function `f` from `α` to `β`, `map(f, l₁ ++ l₂) = map(f, l₁) ++ map(f, l₂)`.
|
List.get_of_mem
theorem List.get_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ n, l.get n = a
This theorem, `List.get_of_mem`, states that for any type `α`, any element `a` of this type, and any list `l` of elements of this type, if `a` is an element of `l` (denoted by `a ∈ l`), then there exists an index `n` such that the element at the `n`th index of `l` (denoted by `List.get l n`) is `a`. Essentially, it asserts that if an element is in a list, then we can find its position within the list.
More concisely: For any type `α`, list `l` of length `n` over `α`, and element `a` in `l`, there exists an index `i` in `{0, 1, ..., n-1}` such that `a = List.get l i`.
|
List.foldr_map
theorem List.foldr_map :
∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β),
List.foldr g init (List.map f l) = List.foldr (fun x y => g (f x) y) init l
The theorem `List.foldr_map` states that for any types `α₁`, `α₂`, and `β`, any function `f` from `α₁` to `α₂`, any function `g` from `α₂` to `β → β`, any list `l` of elements of type `α₁`, and any initial value `init` of type `β`, the process of first mapping `f` over the list `l` and then folding the list from right to left using `g` and `init`, is the same as folding `l` from right to left using a function that applies `f` to the element and then `g` to the result, using `init`. In mathematical terms, if we denote the foldr operation as $\text{foldr}_{g, init}(l)$ and the map operation as $\text{map}_f(l)$, this theorem states that $\text{foldr}_{g, init}(\text{map}_f(l)) = \text{foldr}_{\lambda x, y. g(f(x), y), init}(l)$.
More concisely: For any types `α₁`, `α₂`, and `β`, functions `f : α₁ → α₂` and `g : α₂ → β → β`, list `l : List α₁`, and initial value `init : β`, the theorem asserts that `foldr g (map f l) init` equals `foldr (λ x, λ y, g (f x) y) l init`.
|
List.foldr_self_append
theorem List.foldr_self_append : ∀ {α : Type u_1} {l' : List α} (l : List α), List.foldr List.cons l' l = l ++ l' := by
sorry
The theorem `List.foldr_self_append` states that for all types `α` and for any two lists `l` and `l'` of type `α`, applying the `List.foldr` function on `l` with the `List.cons` function and `l'` as the initial value, results in the same list as appending `l` to `l'`. In other words, folding a list using the `cons` operation is the same as appending the two lists. This is written in mathematical notation as follows: for all `l` and `l'` in Lists of `α`, we have `List.foldr List.cons l' l = l ++ l'`.
More concisely: For all types `α` and lists `l` and `l'` of type `List α`, `List.foldr List.cons l' l = l ++ l'`.
|
List.getLast_eq_get
theorem List.getLast_eq_get : ∀ {α : Type u_1} (l : List α) (h : l ≠ []), l.getLast h = l.get ⟨l.length - 1, ⋯⟩ := by
sorry
The theorem `List.getLast_eq_get` states that for any non-empty list `l` of elements of an arbitrary type `α`, the last element of `l` obtained using `List.getLast` is the same as the element obtained using `List.get` at the index `List.length l - 1`. Here, `List.length l - 1` is the index of the last element of the list, and we use a proof `isLt` that this index is indeed a valid index in the list.
More concisely: For any non-empty list `l` of length `n` over an arbitrary type `α`, `List.getLast l` equals `List.get l (n - 1)`.
|
List.foldl_map
theorem List.foldl_map :
∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α),
List.foldl g init (List.map f l) = List.foldl (fun x y => g x (f y)) init l
The theorem `List.foldl_map` states that for all types `β₁`, `β₂`, and `α`, a function `f` from `β₁` to `β₂`, a function `g` from `α` and `β₂` to `α`, a list `l` of type `β₁`, and an initial value `init` of type `α`, the process of first mapping the function `f` over the list `l` and then folding the list from the left using the function `g` and initial value `init` is equivalent to folding the list from the left using a function that applies `f` to the second argument of `g`, with the same initial value.
In other words, the order of the map and fold operations can be swapped without changing the result, as long as the function used in the fold operation is adjusted accordingly. This can be stated more formally as:
\[ \text{foldl}\ g\ \text{init}\ (\text{map}\ f\ l) = \text{foldl}\ (\lambda x, y.\ g\ x\ (f\ y))\ \text{init}\ l \]
More concisely: The theorem asserts that for any type `α`, functions `f : β₁ -> β₂` and `g : α -> β₂ -> α`, lists `l : β₁` and initial value `init : α`, the left fold-map operation `foldl g init (map f l)` is equivalent to the left fold operation `foldl (λ x, y => g x (f y)) init l`.
|
List.ext_get
theorem List.ext_get :
∀ {α : Type u_1} {l₁ l₂ : List α},
l₁.length = l₂.length →
(∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) → l₁ = l₂
The theorem `List.ext_get` states that for any two lists `l₁` and `l₂` of the same type `α`, if the length of `l₁` is equal to the length of `l₂` and for every natural number `n` less than the length of `l₁` and `l₂`, the `n`-th element of `l₁` is equal to the `n`-th element of `l₂`, then `l₁` is equal to `l₂`. In other words, two lists are considered equal if they have the same length and their corresponding elements are equal.
More concisely: If two lists of the same type have the same length and agree in their elements up to every position, then they are equal.
|
List.filter_cons_of_neg
theorem List.filter_cons_of_neg :
∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.filter p (a :: l) = List.filter p l := by
sorry
The theorem `List.filter_cons_of_neg` states that for any type `α`, any predicate function `p` of type `α → Bool`, any element `a` of type `α`, and any list `l` of type `List α`, if `p a` is not true, then the result of filtering the list `a :: l` (the list `l` with `a` added at the front) with the predicate `p` is the same as filtering the list `l` with `p`. This essentially shows that if an element doesn't satisfy a given predicate, then filtering a list with or without that element will yield the same result.
More concisely: If `p(a)` is false, then filtering list `a :: l` with predicate `p` equals filtering list `l` with `p`.
|
List.length_drop
theorem List.length_drop : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.drop i l).length = l.length - i
The theorem `List.length_drop` states that for any list `l` of elements of some type `α`, and for any natural number `i`, the length of the list obtained by dropping the first `i` elements from `l` is equal to the length of the original list `l` minus `i`. This applies to all types and lists, and it reflects the intuitive idea that dropping elements from a list reduces its length by the number of elements dropped.
More concisely: For any list `l` of length `n` and any natural number `i`, the length of `l.drop i` equals `n - i`.
|
List.mem_cons_of_mem
theorem List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
This theorem states that for any type `α`, and any element `a` of that type in a list `l` of elements of type `α`, if `a` is an element in `l`, then `a` is also an element in the list formed by prepending any element `y` of type `α` to `l`. In other words, if an element exists in a list, it will also exist in any list that is a superset of the original list.
More concisely: If `l` is a list and `a` is an element of `l`, then `a` is also an element of the list `[y :: l]`. (Here, `::` denotes list cons, i.e., the operation of prepending an element to a list.)
|
List.get?_eq_some
theorem List.get?_eq_some :
∀ {α : Type u_1} {a : α} {l : List α} {n : ℕ}, l.get? n = some a ↔ ∃ (h : n < l.length), l.get ⟨n, h⟩ = a := by
sorry
This theorem states that for any type `α`, any element `a` of type `α`, any list `l` of elements of type `α`, and any natural number `n`, the function `List.get?` applied to the list `l` and the number `n` results in `some a` if and only if there exists a natural number `h` such that `n` is less than the length of the list `l` and the function `List.get` applied to the list `l` and the number `n` (with proof that `n` is less than the length of `l`) results in `a`. In other words, the theorem establishes a correspondence between the successful retrieval of an element at a specified index in a list using the `get?` function and the existence of a valid index within the bounds of the list length.
More concisely: For any type `α`, list `l` of length `n` in `α`, and natural number `i` less than `n`, `List.get? l i = some a` if and only if `List.get l i = a`.
|
List.get?_len_le
theorem List.get?_len_le : ∀ {α : Type u_1} {l : List α} {n : ℕ}, l.length ≤ n → l.get? n = none
This theorem states that for any type `α`, any list `l` of type `α`, and any natural number `n`, if the length of the list `l` is less than or equal to `n`, then the `n`th element of list `l` does not exist. In essence, you can't retrieve an element `n` positions into the list if `n` is not less than the length of the list. This result is also consistent with the zero-indexing convention in most programming languages, including Lean 4.
More concisely: For any type `α`, list `l` of length `m` in `α`, and natural number `n` with `n > m`, the `n`th element of `l` does not exist.
|
List.mem_cons
theorem List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
This theorem, `List.mem_cons`, states that for any type `α` and any elements `a` and `b` of that type and any list `l` of type `α`, the proposition that `a` is an element of the list composed of `b` followed by `l` is equivalent to the disjunction of the propositions that `a` equals `b` or `a` is an element of `l`. In other words, an element `a` is in the list formed by prepending `b` to `l` if and only if `a` is equal to `b` or `a` is in the list `l`.
More concisely: For any type `α`, list `l` of length `≥ 1` over `α`, and elements `a` and `b` of `α`, `a ∈ list.cons b l` if and only if `a = b` or `a ∈ l`.
|
List.foldr_eq_foldrM
theorem List.foldr_eq_foldrM :
∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : List α), List.foldr f b l = List.foldrM f b l := by
sorry
This theorem states that for any types `α` and `β`, for any function `f` of type `α → β → β`, for any `β`-type variable `b`, and for any list `l` of `α`-type elements, the right-to-left fold operation (`List.foldr`) and the monadic right-to-left fold operation (`List.foldrM`) are equivalent. In other words, applying function `f` to each element of the list `l` with the initial value `b` using `List.foldr` yields the same result as using `List.foldrM`.
More concisely: For any types `α` and `β`, any function `f : α -> β -> β`, any `β`-valued `b`, and any list `l` of `α`-elements, `List.foldr f b l` is equal to `List.foldrM (λ x acc => some (f x acc)) [] l`.
|
List.reverse_map
theorem List.reverse_map :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α), (List.map f l).reverse = List.map f l.reverse
The theorem `List.reverse_map` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and any list `l` of elements of type `α`, the reverse of the list obtained by mapping `f` over `l` is equal to the list obtained by first reversing `l` and then mapping `f` over the result. In other words, reversing a list after applying a function to its elements is the same as applying the function to the elements of the reversed list. This property can be described in mathematical notation as: for any function `f: α → β` and any list `l: List α`, we have `reverse(map(f, l)) = map(f, reverse(l))`.
More concisely: For all types `α` and `β`, and for any function `f` from `α` to `β`, the application of `reverse` to the list obtained by mapping `f` over a list `l` is equal to the list obtained by reversing `l` and then mapping `f` over its elements. In mathematical notation: `reverse(map(f, l)) = map(f, reverse(l))`.
|
List.filter_cons_of_pos
theorem List.filter_cons_of_pos :
∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.filter p (a :: l) = a :: List.filter p l
The theorem `List.filter_cons_of_pos` states that for any type `α`, any boolean function `p` on `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, if `p` returns `true` when applied to `a`, then the list obtained by filtering the list that results from prepending `a` to `l` with `p` is the same as the list obtained by prepending `a` to the list that results from filtering `l` with `p`. In other words, if an element satisfies a filter condition, it maintains its position when we apply the filter to the list it belongs to.
More concisely: If `a` is an element of list `l` such that `p(a)` holds, then `a` : List.filter p (a :: l) = a :: List.filter p l`.
|
List.get_append
theorem List.get_append :
∀ {α : Type u_1} {l₁ l₂ : List α} (n : ℕ) (h : n < l₁.length), (l₁ ++ l₂).get ⟨n, ⋯⟩ = l₁.get ⟨n, h⟩
The theorem `List.get_append` states that for any type `α`, any two lists `l₁` and `l₂` of this type, and any natural number `n` such that `n` is less than the length of `l₁`, the `n`-th element of the list obtained by appending `l₂` to `l₁` (i.e., `l₁ ++ l₂`) is the same as the `n`-th element of `l₁`. This essentially means that appending a list to another list does not affect the retrieval of elements from the original list at indices less than its length.
More concisely: For any type `α`, lists `l₁` and `l₂` of length `|l₁| > n`, and natural number `n`, the `n`-th element of `l₁ ++ l₂` equals the `n`-th element of `l₁`.
|
List.not_mem_nil
theorem List.not_mem_nil : ∀ {α : Type u_1} (a : α), a ∉ []
This theorem states that for any type `α` and any element `a` of type `α`, `a` is not in the empty list. In other words, no matter what type and element we have, it cannot be a member of an empty list. This is a general property of the empty list.
More concisely: For any type `α` and any element `a`: `a ∉ [] : Prop` (In other words, no element is in the empty list.)
|
List.map_id'
theorem List.map_id' : ∀ {α : Type u_1} (l : List α), List.map (fun a => a) l = l
The theorem `List.map_id'` states that for any list `l` of a certain type `α`, mapping the identity function `(fun a => a)` over `l` returns `l` itself. This means applying the identity function to each element of the list leaves the list unchanged. In mathematical terms, it's saying for each element `a` in list `l`, the list resulting from applying the identity function is equal to the original list `l`.
More concisely: For any list `l` of type `α`, the application of the identity function to each element of `l` results in the same list `l`. In mathematical notation: `List.map (fun a => a) l = l` for all `l` of type `α list`.
|
List.foldr_cons
theorem List.foldr_cons :
∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1} (l : List α),
List.foldr f b (a :: l) = f a (List.foldr f b l)
The theorem `List.foldr_cons` states that for any types `α` and `α_1`, any function `f` of type `α → α_1 → α_1`, any value `b` of type `α_1`, and any list `l` of type `List α`, the operation of folding `f` over the list formed by prepending an element `a` of type `α` to the list `l` (expressed as `a :: l`), starting with the initial value `b`, is equivalent to applying `f` to `a` and the result of folding `f` over the list `l` starting with the same initial value `b`. In other words, the fold operation distributes over the `cons` operation in the list.
More concisely: For any types `α` and `α_1`, any function `f : α → α_1 → α_1`, any value `b : α_1`, and any list `l : List α`, the operation of folding `f` over the list `a :: l` starting with `b` is equal to applying `f` to `a` and the result of folding `f` over `l` starting with `b`.
|
List.take_length
theorem List.take_length : ∀ {α : Type u_1} (l : List α), List.take l.length l = l
The theorem `List.take_length` states that, for all types `α` and any list `l` of type `α`, taking the first `n` elements of `l`, where `n` is the length of `l`, results in `l` itself. In other words, if you try to take as many elements from a list as the list's length itself, you will get the original list.
More concisely: For all types α and lists l of length n in α, List.take n l = l.
Or, more succinctly: The take operation with argument equal to a list's length returns the original list.
|
List.forall_mem_cons
theorem List.forall_mem_cons :
∀ {α : Type u_1} {p : α → Prop} {a : α} {l : List α}, (∀ x ∈ a :: l, p x) ↔ p a ∧ ∀ x ∈ l, p x
This theorem, `List.forall_mem_cons`, states that for all types `α`, predicates `p` over `α`, elements `a` of type `α`, and lists `l` of type `α`, the predicate `p` holds for all elements in the list created by prepending `a` to `l` if and only if `p` holds for `a` and `p` holds for all elements in `l`. In mathematical terms, it's expressing that ∀x ∈ (a :: l), p(x) is equivalent to p(a) ∧ ∀x ∈ l, p(x).
More concisely: For any type `α`, predicate `p` over `α`, element `a` of type `α`, and list `l` of type `α`, the list `a :: l` has all elements satisfying `p` if and only if `a` satisfies `p` and the list `l` has all elements satisfying `p`. In symbols, `(∀x ∈ a :: l) p(x) ↔ (p(a) ∧ ∀x ∈ l) p(x)`.
|
List.get?_eq_get
theorem List.get?_eq_get : ∀ {α : Type u_1} {l : List α} {n : ℕ} (h : n < l.length), l.get? n = some (l.get ⟨n, h⟩)
This theorem states that for any type `α`, any list `l` of type `α`, and any natural number `n`, if `n` is less than the length of the list `l`, then retrieving the `n`-th element of `l` using the function `List.get?` returns the same value as using the function `List.get` with `n` and the proof of `n < length l`. In other words, the two functions `List.get?` and `List.get` are equivalent in retrieving the `n`-th element of a list, provided `n` is a valid index within the list.
More concisely: For any type `α`, list `l` of length `m` over `α`, and natural number `n` with `n < m`, `List.get? l n = List.get l n`.
|
List.get?_eq_none
theorem List.get?_eq_none : ∀ {α : Type u_1} {l : List α} {n : ℕ}, l.get? n = none ↔ l.length ≤ n
The theorem `List.get?_eq_none` states that for any type `α`, any list `l` of `α`, and any natural number `n`, the function `List.get? l n` will return `none` if and only if the length of the list `l` is less than or equal to `n`. This means that you cannot access an element at an index in the list that is greater than or equal to the length of the list.
More concisely: For any type α, list l of length n in α, and natural number m, if m > n then List.get? l m equals none.
|
List.length_eq_zero
theorem List.length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 ↔ l = []
This theorem states that for any list `l` of elements of an arbitrary type `α`, the length of `l` is equal to zero if and only if `l` is an empty list. In other words, it provides a condition to check if a list is empty: a list is empty if and only if its length is zero. This theorem applies to lists of any type of elements.
More concisely: The length of a list equals zero if and only if the list is empty.
|
List.cons_bind
theorem List.cons_bind :
∀ {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : α → List β), (x :: xs).bind f = f x ++ xs.bind f := by
sorry
This theorem, `List.cons_bind`, states that for any types `α` and `β`, an element `x` of type `α`, a list `xs` of type `α`, and a function `f` from `α` to a list of `β`, the result of using the `bind` operation on the list that starts with `x` and continues with `xs`, with the function `f`, is the same as concatenating the result of applying `f` to `x` and the result of using the `bind` operation on `xs` with the function `f`. Essentially, it is stating a property about how the `bind` operation distributes over list concatenation.
More concisely: For any types `α` and `β`, given an element `x` of type `α`, a list `xs` of type `List α`, and a function `f : α → List β`, the laws `(x :: xs).bind(f) = f x @ (xs.bind(f))` and `(xs.bind(λ x => x :: List.nil)).bind(f) = xs.bind(f)` hold.
|
List.nil_bind
theorem List.nil_bind : ∀ {α : Type u_1} {β : Type u_2} (f : α → List β), [].bind f = []
The theorem `List.nil_bind` states that for all types `α` and `β`, and for any function `f` from `α` to List `β`, binding an empty list (`[]`) with `f` results in an empty list. In essence, this means that if you have an empty list and try to apply a list transformation function to it, you will simply get an empty list back. This is a basic property of the list monad's bind operation.
More concisely: For all types `α` and `β`, `List.bind (λx. [], f) [] = []`.
|
List.foldlM_cons
theorem List.foldlM_cons :
∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (b : β) (a : α)
(l : List α),
List.foldlM f b (a :: l) = do
let init ← f b a
List.foldlM f init l
The theorem `List.foldlM_cons` states that for any monad `m`, any types `β` and `α`, any function `f : β → α → m β`, any initial value `b : β`, any value `a : α`, and any list `l : List α`, applying the monadic fold operation `List.foldlM` on the list that has `a` at its head and `l` as its tail, with `f` as the folding function and `b` as the initial accumulator, is equivalent to applying the function `f` on `b` and `a` to get a new initial value, and then applying `List.foldlM` on the rest of the list `l` with this new initial value. This is a generalization of the property of associativity of reduce/fold operations to the context of monadic operations.
More concisely: For any monad `m`, any types `β` and `α`, and any function `f : β → α → m β`, the monadic fold operation `List.foldlM` of a list `l : List α` with `f` as the folding function, `b : β` as the initial accumulator, and `a : α` as the head of the list, is equivalent to applying `f` to `b` and `a` to get a new initial value, and then performing the monadic fold operation on the remaining list `l` with the new initial value.
|
List.foldl_cons
theorem List.foldl_cons :
∀ {α : Type u_1} {β : Type u_2} {a : α} {f : β → α → β} (l : List α) (b : β),
List.foldl f b (a :: l) = List.foldl f (f b a) l
The theorem `List.foldl_cons` states that for any types `α` and `β`, any value `a` of type `α`, any function `f` of type `β → α → β`, any list `l` of elements of type `α`, and any value `b` of type `β`, the result of folding the function `f` over the list obtained by prepending `a` to `l`, starting with `b`, is equal to the result of folding the function `f` over the list `l`, starting with `f b a`. This essentially means that the first operation in the fold of the extended list is applying `f` to `b` and `a`.
More concisely: For any types `α` and `β`, the result of appending an element `a` of type `α` to a list `l` of length `n` and folding a function `f : β → α → β` over the extended list starting with `b` of type `β`, is equal to the result of folding `f` over the original list `l` starting with `f(b, a)`.
|
List.foldlM_append
theorem List.foldlM_append :
∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [inst_1 : LawfulMonad m]
(f : β → α → m β) (b : β) (l l' : List α),
List.foldlM f b (l ++ l') = do
let init ← List.foldlM f b l
List.foldlM f init l'
The theorem `List.foldlM_append` states that for any monad `m`, any types `β` and `α`, any lawful monad instance of `m`, a function `f` from `β` to `α` to `m β`, a value `b` of type `β`, and lists `l` and `l'` of type `List α`, the result of folding `f` over the concatenation of `l` and `l'` starting with `b` is equivalent to folding `f` over `l` starting with `b` to get an intermediate result, and then folding `f` over `l'` starting with this intermediate result. In other words, it demonstrates the associative property of the monadic fold operation on lists.
More concisely: For any monad `m`, any types `β` and `α`, and lawful monad instance of `m`, the result of `List.foldlM f b (l ++ l')` is equal to `List.foldlM (λ x acc. f x acc) b l` then `List.foldlM f acc l'`.
|
List.drop_length
theorem List.drop_length : ∀ {α : Type u_1} (l : List α), List.drop l.length l = []
This theorem states that for any list `l` of elements of any type `α`, if we drop as many elements from the start of the list as the length of the list itself, we will get an empty list. In other words, if you have a list of `n` elements and you drop `n` elements from it, you will be left with no elements, i.e., an empty list.
More concisely: For any list `l` of length `n` over type `α`, dropping the first `n` elements results in an empty list.
|
List.map_id
theorem List.map_id : ∀ {α : Type u_1} (l : List α), List.map id l = l
The theorem `List.map_id` states that for all types `α` and for any list `l` of type `α`, applying the `List.map` function with the identity function `id` to `l` leaves the list unchanged. In other words, mapping the identity function over any list is equivalent to the original list itself. This can be interpreted as the property of `List.map` function to preserve identity – which is a fundamental property in many mathematical structures.
More concisely: For all types `α` and lists `l` of type `α`, `List.map id l` equals `l`.
|
List.foldl_eq_foldlM
theorem List.foldl_eq_foldlM :
∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (l : List α), List.foldl f b l = List.foldlM f b l := by
sorry
The theorem `List.foldl_eq_foldlM` states that for any types `β` and `α`, any function `f` from `β` and `α` to `β`, any value `b` of type `β`, and any list `l` of type `List α`, the result of `List.foldl` (which folds a function over a list from the left) applied to `f`, `b` and `l` is equal to the result of `List.foldlM` (which is a monadic version of foldl) applied to the same arguments. Essentially, this theorem demonstrates that the traditional and the monadic version of left fold on a list are equivalent.
More concisely: For any type `β`, function `f` from `β` x `α` to `β`, value `b` of type `β`, and list `l` of type `List α`, `List.foldl f b l` equals `List.foldlM (fun x acc => f x acc) b l`.
|
List.take_nil
theorem List.take_nil : ∀ {α : Type u_1} {i : ℕ}, List.take i [] = []
This theorem states that for any type `α` and any natural number `i`, when you try to take `i` elements from an empty list of type `α`, the result will always be an empty list. This hold regardless of what `i` is, because there are no elements to take from an empty list.
More concisely: For any type `α` and natural number `i`, the `nth` element of an empty list of type `α` is an empty list.
|
List.map_cons
theorem List.map_cons :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (l : List α), List.map f (a :: l) = f a :: List.map f l := by
sorry
The theorem `List.map_cons` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, any element `a` of type `α`, and any list `l` of type `List α`, the operation of mapping the function `f` over the list that results from appending `a` to the start of `l`, is the same as appending the function `f` applied to `a` to the start of the list that results from mapping `f` over `l`. In other words, the function `f` can be applied before or after appending an element to a list, and the result will be the same.
More concisely: For all types `α` and `β`, and for any function `f` from `α` to `β`, the operation of appending `f(a)` to the front of `List.map f l` is equal to applying `f` to `a` and then appending the result to the front of `l`.
|
List.get_map
theorem List.get_map :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.map f l).length},
(List.map f l).get n = f (l.get ⟨↑n, ⋯⟩)
This theorem states that for any function `f` mapping elements of type `α` to type `β`, and any list `l` of type `α`, if we have a valid index `n` into the list obtained by mapping `f` over `l`, then fetching the `n`-th element of the mapped list is equivalent to first fetching the `n`-th element of the original list `l`, and then applying the function `f` to it. The index `n` is a natural number less than the length of the list obtained by applying `f` to each element of the list `l`.
More concisely: For any function `f` and list `l`, if `n` is a valid index for the list obtained by applying `f` to each element of `l`, then the `n`-th element of the mapped list equals `f` applied to the `n`-th element of the original list.
|
List.foldr_append
theorem List.foldr_append :
∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l l' : List α),
List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l
The theorem `List.foldr_append` states that for any types `α` and `β`, any function `f` of type `α → β → β`, any value `b` of type `β`, and any two lists `l` and `l'` of type `List α`, the result of applying `List.foldr` with function `f` and initial value `b` to the append of `l` and `l'` (`l ++ l'`) is equal to the result of applying `List.foldr` with function `f` to list `l` with the initial value being the result of applying `List.foldr` with function `f` and initial value `b` to list `l'`. In other words, it is expressing the property of distributivity of the `foldr` function over list concatenation.
More concisely: For any types `α` and `β`, functions `f : α → β → β`, initial value `b : β`, and lists `l, l' : List α`, `List.foldr (λ x xs => f x xs) b (l ++ l')` is equal to `List.foldr (λ x xs => f x (List.foldr (λ y ys => f y ys) b xs)) b l`.
|
List.get?_map
theorem List.get?_map :
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (n : ℕ), (List.map f l).get? n = Option.map f (l.get? n)
The `List.get?_map` theorem states that for any type `α` and `β`, a function `f` from `α` to `β`, a list `l` of type `α`, and a natural number `n`, getting the nth element of the list obtained by mapping the function `f` over the list `l` is the same as mapping the function `f` over the nth element of the list `l`. In other words, the order in which you map a function over a list and get an element from the list does not matter.
More concisely: For any type `α`, function `f` from `α` to `β`, list `l` of type `α`, and natural number `n`, `(get_n (List.map f l)) = (List.map f (get_n l))`.
|
List.mem_map_of_mem
theorem List.mem_map_of_mem :
∀ {α : Type u_1} {β : Type u_2} {a : α} {l : List α} (f : α → β), a ∈ l → f a ∈ List.map f l
This theorem states that for any type `α` and `β`, any element `a` of type `α`, any list `l` of elements of type `α`, and any function `f` from `α` to `β`, if `a` is an element of the list `l`, then `f(a)`, the result of applying the function `f` to `a`, is an element of the list obtained by applying the function `f` to each element of the list `l`. This is a statement about list transformation: elements in the original list maintain their membership in the transformed list when a function is applied to them.
More concisely: If `a` is an element of list `l` of type `α`, then `f(a)` is an element of the list `map f l` of type `β`, where `map f l` is the list obtained by applying the function `f` to each element of `l`.
|
List.singleton_append
theorem List.singleton_append : ∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l
This theorem, `List.singleton_append`, states that for any type of object `α`, any object `x` of type `α`, and any list `l` of objects of type `α`, appending the list `l` to the singleton list that contains `x` (`[x] ++ l`) is equal to the list obtained by prepending `x` to `l` (`x :: l`). In other words, joining a list to a single-item list is the same as adding that item to the front of the list.
More concisely: For any type `α` and objects `x` of type `α` and `l` of type `list α`, the singleton list `[x]` appended to list `l` is equal to the cons list `x :: l`.
|
List.eq_nil_iff_forall_not_mem
theorem List.eq_nil_iff_forall_not_mem : ∀ {α : Type u_1} {l : List α}, l = [] ↔ ∀ (a : α), a ∉ l
This theorem states that for all types `α` and all lists `l` of type `α`, the list `l` is empty if and only if for every element `a` of type `α`, `a` is not a member of `l`. In other words, a list is empty if it does not contain any elements. The theorem is expressed in Lean 4 using universal quantifiers and bi-conditional (`↔`) logical connector, associating the emptiness of a list with the non-membership of any element in it.
More concisely: A list of type `α` is empty if and only if no element of type `α` belongs to the list.
|
List.get_set_eq
theorem List.get_set_eq :
∀ {α : Type u_1} (l : List α) (i : ℕ) (a : α) (h : i < (l.set i a).length), (l.set i a).get ⟨i, h⟩ = a
The theorem `List.get_set_eq` states that for any type `α`, any list `l` of type `α`, any natural number `i`, and any element `a` of type `α`, given the condition that `i` is less than the length of the list obtained from replacing the `i`-th element of `l` with `a`, retrieving the `i`-th element of this new list will yield `a`. In essence, this theorem asserts that setting an element at a particular index in a list and then getting the element at the same index returns the element we initially set.
More concisely: For any type `α`, list `l` of length `n` over `α`, natural number `i` < `n`, and element `a` of `α`, if list `l'` is obtained from `l` by setting its `i`-th element to `a`, then `l'.nth i = a`.
|
List.get?_append_right
theorem List.get?_append_right :
∀ {α : Type u_1} {l₁ l₂ : List α} {n : ℕ}, l₁.length ≤ n → (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
The theorem `List.get?_append_right` states that for any two lists `l₁` and `l₂` of type `α` and a non-negative integer `n`, if the length of `l₁` is less than or equal to `n`, then fetching the `n`th element of the concatenated list `l₁ ++ l₂` is equivalent to fetching the `(n - length of l₁)`th element of `l₂`. In other words, if `n` is beyond the range of the first list, the `n`th element in the combined list is dependent on the second list `l₂` only.
More concisely: For any lists `l₁` and `l₂` of length `m` and `n` respectively, and non-negative integer `n`, if `m <= n`, then the `n`-th element of `l₁ ++ l₂` is equal to the `(n - m)`-th element of `l₂`.
|
List.get_mem
theorem List.get_mem : ∀ {α : Type u_1} (l : List α) (n : ℕ) (h : n < l.length), l.get ⟨n, h⟩ ∈ l
This theorem, `List.get_mem`, asserts that for any list `l` of elements of some arbitrary type `α` and any natural number `n`, if `n` is less than the length of list `l`, then the `n`-th element of `l` (obtained using `List.get` function with `n` as the index) is indeed an element of the list `l`.
More concisely: For any list `l` of length `n+1` and natural number `n`, the `n`-th element of `l` belongs to `l`.
|
List.mem_cons_self
theorem List.mem_cons_self : ∀ {α : Type u_1} (a : α) (l : List α), a ∈ a :: l
This theorem, `List.mem_cons_self`, states that for any type of data `α` and for any element `a` of this type and any list `l` of elements of this type, `a` is an element of the list that results from prepending `a` to `l`. In other words, an element is always a member of the list obtained by adding it to the front of any other list.
More concisely: For any type `α` and any `α` element `a` and list `l` of length `n+1` elements of type `α`, `a` is in the list `[a] :: l` if and only if `a` is in `l`.
|
List.append_eq_nil
theorem List.append_eq_nil : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []
This theorem states that for any type `α` and any two lists `p` and `q` of type `α`, the append operation `p ++ q` equals the empty list if and only if both `p` and `q` are empty. In other words, it's not possible to append two non-empty lists and end up with an empty list.
More concisely: For any type `α`, lists `p` and `q` of type `α`, the condition `p ++ q = []` if and only if both `p` and `q` are empty.
|
List.append_bind
theorem List.append_bind :
∀ {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : α → List β), (xs ++ ys).bind f = xs.bind f ++ ys.bind f := by
sorry
The theorem `List.append_bind` states that for any types `α` and `β`, any two lists of type `α` (denoted as `xs` and `ys`), and any function `f` from `α` to a list of `β`, the bind operation on the concatenation of the lists `xs` and `ys` using the function `f` is equal to the concatenation of the bind operation on `xs` using `f` and the bind operation on `ys` using `f`. In more mathematical terms, this is the property that `List.bind (xs ++ ys) f = List.bind xs f ++ List.bind ys f`, showing an important property of the bind operation in the list monad related to list concatenation.
More concisely: For any types `α` and `β`, and lists `xs` and `ys` of type `α`, the bind operation `List.bind` over the concatenation `xs ++ ys` of `xs` and `ys` using a function `f` from `α` to lists of `β` is equal to the concatenation of the bind operations on `xs` and `ys` using `f`. That is, `List.bind (xs ++ ys) f = List.bind xs f ++ List.bind ys f`.
|
List.foldr_reverse
theorem List.foldr_reverse :
∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → β) (b : β),
List.foldr f b l.reverse = List.foldl (fun x y => f y x) b l
The theorem `List.foldr_reverse` states that for any list `l` of type `List α`, for any function `f` of type `α → β → β`, and for any element `b` of type `β`, applying the `foldr` function with `f` and `b` on the reverse of `l` yields the same result as applying the `foldl` function with `f` flipped and `b` on `l`. In other words, reversing a list and then performing a right fold with a certain function and base point is identical to performing a left fold with the same function (but with arguments flipped) and base point on the original list.
More concisely: For any list `l` of type `List α`, any function `f` of type `α → β → β`, and any element `b` of type `β`, `List.foldr (λ x acc, acc ~<~ f x) b (reverse l) = List.foldl (λ acc x, f x acc) b l`.
|
List.foldrM_cons
theorem List.foldrM_cons :
∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m] (a : α)
(l : List α) (f : α → β → m β) (b : β), List.foldrM f b (a :: l) = List.foldrM f b l >>= f a
The theorem `List.foldrM_cons` states that for any two types `m` and `α`, where `m` is a type constructor that takes a type and returns another type, and for any type `β`, given that `m` forms a Monad and a LawfulMonad, for any `a` of type `α`, any list `l` of elements of type `α`, a function `f` from type `α` and `β` to `m β`, and any `b` of type `β`, the fold right monadic operation on the list that consists of `a` followed by the list `l`, with function `f` and initial value `b`, is the same as performing the fold right monadic operation on the list `l` with the same function `f` and initial value `b`, and then binding the result with the function `f` applied to `a`. This theorem is essentially a property about how the fold right monadic operation distributes over the cons operator (i.e., list constructor).
More concisely: For any monad and lawful monad `m`, type `α`, list `l` of type `α`, function `f : α → m β`, initial value `b` of type `β`, and element `a` of type `α`, the monadic fold right operation on the list `[a] @ l` using `f` and `b` is equivalent to binding the result of the monadic fold right operation on list `l` with `f(a)`.
|
List.append_inj
theorem List.append_inj :
∀ {α : Type u_1} {s₁ s₂ t₁ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂
The theorem `List.append_inj` states that for any type `α` and any lists `s₁`, `s₂`, `t₁`, `t₂` of type `α`, if the list obtained by appending `t₁` to `s₁` is the same as the list obtained by appending `t₂` to `s₂`, and if the lengths of `s₁` and `s₂` are equal, then `s₁` is equal to `s₂` and `t₁` is equal to `t₂`. In other words, two pairs of lists with equal concatenated results and initial list lengths imply that the original lists were also equal.
More concisely: If two lists `s₁` and `s₂` of the same length, and `t₁` and `t₂` are such that `s₁ ++ t₁ = s₂ ++ t₂` in Lean's list append `(++)` notation, then `s₁ = s₂` and `t₁ = t₂`.
|
List.map_nil
theorem List.map_nil : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, List.map f [] = []
This theorem, `List.map_nil`, states that for any types `α` and `β` and any function `f` mapping from `α` to `β`, the list obtained by mapping `f` over an empty list of type `α` is also an empty list. In other words, given any function, applying this function to each element of an empty list results in another empty list.
More concisely: For any types `α` and `β` and function `f` from `α` to `β`, the map of the empty list of type `α` using `f` is the empty list of type `β`. Or, more mathematically, `List.map ∅ f = ∅`.
|
List.zip_nil_right
theorem List.zip_nil_right : ∀ {α : Type u_1} {l : List α} {β : Type u_2}, l.zip [] = []
The theorem `List.zip_nil_right` states that for any type `α` and any list `l` of type `α`, and for any type `β`, when the `zip` function is applied to the list `l` and an empty list of type `β`, the result is always an empty list. This means that zipping any list with an empty list results in an empty list, irrespective of the types and contents of the lists.
More concisely: For any types `α` and `β`, the zip of a list `l` of type `α` with an empty list of type `β` is an empty list.
|
List.filter_eq_nil
theorem List.filter_eq_nil :
∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ a ∈ l, ¬p a = true
This theorem is named `List.filter_eq_nil` and states that for any type `α`, any Boolean-valued function `p` on `α`, and any list `l` of elements of type `α`, the function `List.filter p l` returns an empty list if and only if for every element `a` in the list `l`, the function `p(a)` is not true. In other words, the filtering operation results in an empty list precisely when no elements of the original list satisfy the condition defined by the function `p`.
More concisely: For any type `α`, list `l` of `α`, and Boolean-valued function `p` on `α`, `List.filter p l` is the empty list if and only if for all `a` in `l`, `p(a)` is false.
|
List.eq_nil_of_length_eq_zero
theorem List.eq_nil_of_length_eq_zero : ∀ {α : Type u_1} {l : List α}, l.length = 0 → l = []
This theorem states that for any type `α` and any list `l` of elements of type `α`, if the length of the list `l` is zero, then `l` must be the empty list. In other words, the only list of type `α` with a length of zero is the empty list. This theorem is a formalization of the intuitive notion that a list without any elements is the empty list.
More concisely: For any type `α`, the empty list is the only list of length zero.
|
List.take_append_drop
theorem List.take_append_drop : ∀ {α : Type u_1} (n : ℕ) (l : List α), List.take n l ++ List.drop n l = l
The theorem `List.take_append_drop` states that for any type `α`, any natural number `n`, and any list `l` of type `α`, if you take the first `n` elements from the list `l` and concatenate (`++`) it with the result of dropping the first `n` elements from the list `l`, you will get the original list `l` back. This theorem asserts that splitting a list into a "taken" part and a "dropped" part and then appending them together gives you back the original list.
More concisely: For any type `α` and natural number `n`, the list `take n l ++ drop n l` equals `l`, where `take n` and `drop n` are the functions that return the first `n` elements and remaining elements of a list `l` respectively.
|
List.zipWith_nil_right
theorem List.zipWith_nil_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → β → γ}, List.zipWith f l [] = []
This theorem states that for any list `l` of elements of type `α` and any function `f` which takes as input an element of type `α` and an element of type `β` and returns an element of type `γ`, when we apply the `zipWith` function to `l` and an empty list of type `β`, we always get an empty list. In other words, if you try to zip any list with an empty list using any function, the result will always be an empty list.
More concisely: For any list `l` of type `α` and any function `f : α → β → γ`, `zipWith f l [] = []`.
|