List.zipWith_same
theorem List.zipWith_same :
∀ {α : Type u} {δ : Type u_3} (f : α → α → δ) (l : List α), List.zipWith f l l = List.map (fun a => f a a) l := by
sorry
The theorem `List.zipWith_same` states that for any type `α` and a type `δ`, given any binary function `f` from `α` to `δ` and a list `l` of type `α`, applying the function `f` in a pairwise manner to the elements of the list `l` (essentially zipping the list `l` with itself using the function `f`) is equivalent to mapping the function `(fun a => f a a)` over the list `l`. In other words, zipping a list with itself using a function is the same as applying that function to each element of the list.
More concisely: For any type `α` and function `f` from `α` to a type `δ`, zipping `α` list `l` with `l` using `f` is equivalent to applying `f` element-wise to `l`.
|
List.map_uncurry_zip_eq_zipWith
theorem List.map_uncurry_zip_eq_zipWith :
∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : List α) (l' : List β),
List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'
The theorem `List.map_uncurry_zip_eq_zipWith` states that for any function `f` with two arguments from types `α` and `β` producing a result of type `γ`, and for any two lists `l` of type `α` and `l'` of type `β`, the result of mapping the uncurried version of `f` over the zipped version of `l` and `l'` is equivalent to zipping `l` and `l'` with the function `f`. In other words, it states that applying the function to each pair of elements from the zipped lists is the same as creating a new list of the results of applying the function to corresponding elements of the two lists.
More concisely: For any function $f : \alpha \times \beta \rightarrow \gamma$, the application of $f$ to the zipped lists $(x\_i, y\_i)_{i < length(l)} \text{ and } (x'\_i, y'_i)_{i < length(l')}$ is equal to the list obtained by applying $f$ to the corresponding elements of the lists $l$ and $l'$, i.e., $(f(x\_i, y\_i))_{i < length(l)} = \text{zipWith}(f)(l)(l')$.
|
List.unzip_zip
theorem List.unzip_zip :
∀ {α : Type u} {β : Type u_1} {l₁ : List α} {l₂ : List β}, l₁.length = l₂.length → (l₁.zip l₂).unzip = (l₁, l₂)
This theorem, `List.unzip_zip`, states that for any two lists `l₁` and `l₂` of arbitrary types `α` and `β` respectively, if `l₁` and `l₂` have the same length, then if we zip these two lists together to form a list of pairs and subsequently unzip it, we will get back the original lists `l₁` and `l₂`. In other words, the operations of zipping and unzipping are inverses of each other given the precondition that the lists being zipped have the same length.
More concisely: For any lists `l₁ : List α` and `l₂ : List β` of equal length, `List.zip (List.unzip (List.zip l₁ l₂)) = (l₁, l₂)` and `List.zip (List.unzip pairs) = pairs` for some `pairs : List (α × β)`.
|
List.lt_length_right_of_zipWith
theorem List.lt_length_right_of_zipWith :
∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β},
i < (List.zipWith f l l').length → i < l'.length
This theorem states that for any types `α`, `β`, and `γ`, a function `f` from `α` and `β` to `γ`, a natural number `i`, and lists `l` and `l'` of types `α` and `β`, respectively, if `i` is less than the length of the list resulting from applying `zipWith` to `f`, `l`, and `l'`, then `i` is also less than the length of list `l`.
In other words, an index `i` that is valid in the list created by `zipWith` function also implies that it is a valid index in the original list `l` of type `α`.
More concisely: For any functions `f` from `α × β` to `γ`, if the length of `zipWith f l1 l2` is greater than `i`, then the length of `l1` is also greater than `i`, where `l1` is a list of type `α` and `l2` is a list of type `β`.
|
List.lt_length_left_of_zipWith
theorem List.lt_length_left_of_zipWith :
∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β},
i < (List.zipWith f l l').length → i < l.length
The theorem `List.lt_length_left_of_zipWith` establishes that for any types `α`, `β`, and `γ`, a function `f` that takes an element of type `α` and an element of type `β` and returns an element of type `γ`, and lists `l` of type `α` and `l'` of type `β`, if an index `i` is less than the length of the list resulting from zipping `l` and `l'` using function `f` (i.e., `List.zipWith f l l'`), then `i` is also less than the length of list `l`.
More concisely: For any types `α`, `β`, and `γ`, and lists `l` of length `n` in `α` and `l'` of length `m` in `β`, if `i` is less than the length `(n + m)` of the list obtained by zipping `l` and `l'` with function `f : α × β → γ`, then `i` is less than the length `n` of `l`.
|
List.unzip_eq_map
theorem List.unzip_eq_map :
∀ {α : Type u} {β : Type u_1} (l : List (α × β)), l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
This theorem states that for any list of pairs, where the pairs are of types `α` and `β`, the operation of "unzipping" the list (separating it into two lists where one contains all the first elements of the pairs and the other contains the second elements) is equivalent to creating two new lists separately by mapping the `Prod.fst` operation (which extracts the first element of a pair) and `Prod.snd` operation (which extracts the second element of a pair) over the original list. In other words, for any list `l` of pairs, `List.unzip l` will produce the same result as `(List.map Prod.fst l, List.map Prod.snd l)`. In LaTeX mathematics, it can be expressed as:
For all lists \(l\) of pairs (with elements from types \(\alpha\) and \(\beta\)), the operation of unzipping \(l\) is equivalent to the operation of mapping the first and second projections over \(l\). That is,
\[
\text{{List.unzip}}(l) = (\text{{List.map Prod.fst}}(l), \text{{List.map Prod.snd}}(l))
\]
More concisely: For any list of pairs between types `α` and `β`, the operation of unzipping the list is equivalent to mapping `Prod.fst` and `Prod.snd` separately. That is, `List.unzip l = (List.map Prod.fst l, List.map Prod.snd l)`.
|