List.concat_eq_append
theorem List.concat_eq_append : ∀ {α : Type u} (as : List α) (a : α), as.concat a = as ++ [a]
The theorem `List.concat_eq_append` states that for any type `α`, any list `as` of type `List α`, and any element `a` of type `α`, concatenating the element `a` to the end of the list `as` using the `List.concat` function is equivalent to appending the singleton list containing `a` to the end of `as` using the append (`++`) operator. This means in both cases, the resulting list will be `as` followed by the element `a`.
More concisely: For any type `α` and list `as` of length `n` over `α`, `List.concat [a] (List.init as ++ [a]) = as`.
|
List.length_reverse
theorem List.length_reverse : ∀ {α : Type u} (as : List α), as.reverse.length = as.length
This theorem states that for any list of elements of any type, the length of the list remains the same even after it is reversed. More formally, for all types `α` and for any list `as` of type `α`, the length of the list `as` after it is reversed using the function `List.reverse` is equal to the original length of the list `as`. This is denoted in LaTeX as, for any list $\text{as}$, $\text{List.length}(\text{List.reverse(as)}) = \text{List.length(as)}$.
More concisely: For any list `as` of type `α`, the length of the reversed list `List.reverse as` is equal to the original length of `as`. In mathematical notation, `List.length (List.reverse as) = List.length as`.
|
List.reverse_cons
theorem List.reverse_cons : ∀ {α : Type u} (a : α) (as : List α), (a :: as).reverse = as.reverse ++ [a]
The theorem `List.reverse_cons` states that for any type `α` and any element `a` of type `α` and list `as` of type `List α`, the reverse of the list obtained by prepending `a` to `as` is equal to the concatenation of the reverse of `as` and the list containing `a` as its only element. In other words, reversing a list where an element is added at the beginning results in the reversed original list followed by the added element.
More concisely: For any type `α` and any element `a` of type `α` and list `as` of type `List α`, `List.reverse (a :: as) = List.reverse as ++ [a]`.
|
List.length_set
theorem List.length_set : ∀ {α : Type u} (as : List α) (i : ℕ) (a : α), (as.set i a).length = as.length
The theorem `List.length_set` states that for all types `α`, any list `as` of type `α`, any natural number `i`, and any element `a` of type `α`, the length of the list resulting from setting the `i`-th element of `as` to `a` is equal to the length of the original list `as`. In simpler terms, updating an element at a specific index in a list doesn't change the length of the list.
More concisely: For all types `α`, lists `as` of length `n` over `α`, natural numbers `i`, and elements `a` of `α`, updating the `i`-th element of `as` to `a` results in a list of length `n`.
|
List.mem_of_elem_eq_true
theorem List.mem_of_elem_eq_true :
∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {as : List α}, List.elem a as = true → a ∈ as := by
sorry
This theorem, `List.mem_of_elem_eq_true`, states that for any type `α` that has an equality test (`BEq α`) and respects the laws of equality (`LawfulBEq α`), and for any element `a` of type `α` and list `as` of elements of type `α`, if the function `List.elem` applied to `a` and `as` yields `true`, then `a` is indeed a member of list `as`. Essentially, it formalizes the intuitive idea that if `List.elem` tells you that an element is in a list, then that element really is in that list.
More concisely: For any type `α` with `BEq α` and `LawfulBEq α`, if `List.elem α a as = true`, then `a ∈ as`.
|
List.length_append
theorem List.length_append : ∀ {α : Type u} (as bs : List α), (as ++ bs).length = as.length + bs.length
This theorem states that for any type `α` and any two lists `as` and `bs` of that type, the length of the concatenated list `as ++ bs` is equal to the sum of the lengths of `as` and `bs`. In other words, it expresses the property that the length of the concatenation of two lists is the sum of the lengths of the individual lists.
More concisely: For any type `α` and lists `as : list α` and `bs : list α`, the length of their concatenation `as ++ bs` equals the sum of the lengths of `as` and `bs`. (In mathematical notation: `#as + #bs = #(as ++ bs)`, where `#` denotes list length.)
|
List.zipWithAll_nil_right
theorem List.zipWithAll_nil_right :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α},
List.zipWithAll f as [] = List.map (fun a => f (some a) none) as
The `List.zipWithAll_nil_right` theorem states that for any list `as` of type `List α` and a function `f` of type `(Option α → Option α_1 → α_2)`, applying `List.zipWithAll` with `f` to `as` and an empty list results in the same list as applying `List.map` to `as` with a function that applies `f` to `Some a` and `None` for each element `a` in `as`. In other words, if you try to 'zip together' a list with an empty list using a function that operates on optional elements, you'll get back a list that's been transformed by that function treating all elements of the original list as present (`Some a`) and all elements of the empty list as absent (`None`).
More concisely: For any list `as` of type `List α` and function `f` of type `Option α → Option α₁ → α₂`, `List.zipWithAll as [] f = List.map (λx => Some x >>= fun _ => Some (f (Some x) None)) as`.
|
List.length_replicate
theorem List.length_replicate : ∀ {α : Type u} (n : ℕ) (a : α), (List.replicate n a).length = n
The theorem `List.length_replicate` states that for any type `α`, any natural number `n`, and any element `a` of type `α`, the length of the list obtained by replicating `a` `n` times is exactly `n`. This means that if you create a list by repeating a certain element a certain number of times, the length of that list will be equal to the number of times you repeated the element.
More concisely: For any natural number `n` and element `a`, the length of the list obtained by repeating `a` `n` times is equal to `n`.
|
List.nil_append
theorem List.nil_append : ∀ {α : Type u} (as : List α), [] ++ as = as
This theorem states that for any type `α` and for any list `as` of type `α`, appending an empty list `[]` at the front of the list `as` results in the original list `as`. In mathematical terms, for all `α` and `as`, `[] ++ as = as`. This is essentially the property of the identity element in the operation of list concatenation.
More concisely: For all types `α` and lists `as` of type `α`, appending the empty list `[]` to the front of `as` results in the original list `as`, i.e., `[] ++ as = as`.
|
List.cons_append
theorem List.cons_append : ∀ {α : Type u} (a : α) (as bs : List α), a :: as ++ bs = a :: (as ++ bs)
This theorem, `List.cons_append`, states that for any type `α`, and for any element `a` of this type and any two lists `as` and `bs` of the same type, prepending `a` to the concatenation of `as` and `bs` is the same as prepending `a` to `as` and then concatenating the result with `bs`. In other words, in the context of list operations, the operation of prepending an element to a list is 'left distributive' over list concatenation.
More concisely: For any type `α` and lists `as : list α` and `bs : list α`, `a :: (as ++ bs) = a :: as ++ bs`, where `::` denotes list prepending and `++` list concatenation.
|
List.reverse_append
theorem List.reverse_append : ∀ {α : Type u} (as bs : List α), (as ++ bs).reverse = bs.reverse ++ as.reverse
The theorem `List.reverse_append` states that for any type `α` and for any two lists `as` and `bs` of type `α`, reversing the list obtained by appending `as` and `bs` (`as ++ bs`) is equivalent to appending the reversed list of `bs` and the reversed list of `as` (`List.reverse bs ++ List.reverse as`). In other words, reversing an appended list interchanges the order of the original lists and also reverses them individually.
More concisely: For all types `α` and lists `as` and `bs` of length `m` and `n` respectively, `List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as`.
|
List.length_map
theorem List.length_map : ∀ {α : Type u} {β : Type v} (as : List α) (f : α → β), (List.map f as).length = as.length
The theorem `List.length_map` states that for any list `as` of type `α` and any function `f` mapping from `α` to another type `β`, the length of the list obtained by applying `f` to each element of `as` (using the `List.map` function) is equal to the length of `as`. In other words, mapping a function over a list does not change its length. This is represented mathematically as: for all `as` in `List α` and all `f` in `α → β`, `List.length (List.map f as) = List.length as`.
More concisely: For any list `as` of type `α` and function `f` from `α` to another type `β`, the length of the list obtained by applying `f` to each element of `as` using `List.map` is equal to the length of `as`. In mathematical notation, `List.length (List.map f as) = List.length as`.
|
List.drop_nil
theorem List.drop_nil : ∀ {α : Type u} {i : ℕ}, List.drop i [] = []
The theorem `List.drop_nil` states that for any type `α` and any natural number `i`, if you attempt to drop `i` elements from an empty list, the result will always be an empty list. In other words, if there are no elements to be removed from the list, the operation of dropping elements will not change the list.
More concisely: For any type `α` and natural number `i`, `List.drop i [] = []`.
|
List.append_assoc
theorem List.append_assoc : ∀ {α : Type u} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)
This theorem, `List.append_assoc`, declares that for all types `α` and any three lists `as`, `bs`, and `cs` of this type, the operation of appending the lists together is associative. In other words, appending `as` with the result of appending `bs` and `cs` (`as ++ (bs ++ cs)`) is the same as appending the result of appending `as` and `bs` with `cs` (`(as ++ bs) ++ cs`). This mirrors the associative property in algebra where `(a+b)+c = a+(b+c)` for any numbers a, b, and c.
More concisely: For all types `α`, the operation of list concatenation `++` is associative, i.e., `(as ++ bs) ++ cs = as ++ (bs ++ cs)` for any lists `as`, `bs`, and `cs` of type `α`.
|
List.drop_eq_nil_of_le
theorem List.drop_eq_nil_of_le : ∀ {α : Type u} {as : List α} {i : ℕ}, as.length ≤ i → List.drop i as = []
The theorem `List.drop_eq_nil_of_le` states that for any type `α`, any list `as` of type `α`, and any natural number `i`, if the length of `as` is less than or equal to `i`, then dropping `i` elements from `as` results in an empty list. Essentially, this means if you try to drop more elements from a list than it contains (or exactly as many), you will end up with an empty list.
More concisely: For any type `α` and any list `as : List α` of length `l`, if `l ≤ i`, then `List.drop i as = ∅` (the empty list).
|
List.append_nil
theorem List.append_nil : ∀ {α : Type u} (as : List α), as ++ [] = as
This theorem, `List.append_nil`, states that for any type in Lean 4, denoted by `α`, and for any list of that type, `as`, appending an empty list to `as` will result in `as` itself. In other words, adding nothing to a list leaves the list unchanged. This theorem is a fundamental property of lists and holds for any type of list elements.
More concisely: For any type `α` and list `as` of length zero or more elements `α`, `as ++ [] = as` holds.
|
List.elem_eq_true_of_mem
theorem List.elem_eq_true_of_mem :
∀ {α : Type u} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {as : List α}, a ∈ as → List.elem a as = true := by
sorry
The theorem `List.elem_eq_true_of_mem` states that for any type `α` with a defined equality operation (`BEq α`), any lawful B equivalence relation (`LawfulBEq α`), and any element `a` of type `α` and list `as` of type `List α`, if the element `a` belongs to the list `as` (denoted by `a ∈ as`), then the function `List.elem a as` equals `true`. This describes that if an element is in a list, then the list's `elem` function will correctly identify that the element is present.
More concisely: For any type `α` with equality `BEq α` and lawful B equivalence relation `LawfulBEq α`, if `a ∈ as` then `List.elem a as = true`.
|
List.reverse_reverse
theorem List.reverse_reverse : ∀ {α : Type u} (as : List α), as.reverse.reverse = as
This theorem states that for all types α and for any list of type α, the double reverse of the list equals the original list. In other words, if you reverse a list twice, you will get back the original list. This property is akin to the mathematical principle that the double negation of a statement is equivalent to the original statement.
More concisely: For all types α and lists l of length n over α, the reversed list (reverse (reverse l)) equals the original list l.
|
List.zipWithAll_nil_left
theorem List.zipWithAll_nil_left :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1},
List.zipWithAll f [] bs = List.map (fun b => f none (some b)) bs
The theorem `List.zipWithAll_nil_left` states that for any types `α`, `α_1`, and `α_2`, and any function `f` from `Option α` and `Option α_1` to `α_2`, and any list `bs` of type `List α_1`, when the first list in the `zipWithAll` function is an empty list, the result is equivalent to mapping the function `f` (with the first argument being `none` and the second argument being each element of `bs` wrapped in `some`) over the list `bs`. In other words, it's as if we're pairing each element of `bs` with `none` and then applying the function `f` to these pairs.
More concisely: For any types `α`, `α_1`, and `α_2`, and any function `f` from `Option α × Option α_1` to `α_2`, `List.zipWithAll f [] bs = List.map (x => some x) bs |>. map (λ x => some x) |>. map (λ x => f (none, x))` where `bs` is a list of type `List α_1`.
|