List.foldrIdx_eq_foldr_enum
theorem List.foldrIdx_eq_foldr_enum :
∀ {α : Type u} {β : Type v} (f : ℕ → α → β → β) (b : β) (as : List α),
List.foldrIdx f b as = List.foldr (Function.uncurry f) b as.enum
This theorem states that for any list of elements of type `α`, initial value of type `β`, and function `f` that takes an index of type `ℕ`, an element of type `α`, and an accumulator of type `β`, and returns a new accumulator of type `β`, the `List.foldrIdx` function, which applies the function `f` to every element in the list from right to left along with its index, is equivalent to `List.foldr` function (which also applies a function to each element in the list from right to left but without the index) paired with the `Function.uncurry` function (which interprets `f` as a function on pairs of indices and elements) applied to the enumeration (`List.enum`) of the list that pairs up each element with its index. In other words, folding a list with a binary function and an initial accumulator, while passing the index of each element to the binary function, yields the same result as folding over the enumerated list (which turns each element into a pair of its index and value) with the uncurried binary function.
More concisely: For any type `α`, initial value `β`, and function `f : ℕ × α → β → β`, the function `List.foldrIdx` applying `f` to a list `l` is equivalent to applying `Function.uncurry(List.foldr (λ x, λ _ acc => f _ x acc))` to the enumeration of `l`.
|
List.mapIdx_cons
theorem List.mapIdx_cons :
∀ {α : Type u_1} {β : Type u_2} (l : List α) (f : ℕ → α → β) (a : α),
List.mapIdx f (a :: l) = f 0 a :: List.mapIdx (fun i => f (i + 1)) l
The `List.mapIdx_cons` theorem states that for any list `l` of elements of some type `α`, a function `f` mapping from natural numbers and elements of `α` to another type `β`, and an element `a` of type `α`, if you apply the `List.mapIdx` function to `f` and a list formed by prepending `a` to `l` (expressed as `a :: l`), the result is a list that begins with `f` applied to 0 and `a`, and continues with `List.mapIdx` applied to a function equivalent to `f` but with its first argument incremented by 1, and the original list `l`. In other words, applying `List.mapIdx` to a prepended list is the same as applying `f` to the new first element and the remaining elements of the list with the index incremented.
More concisely: For any list `l` of length `n+1`, function `f : ℕ × α → β`, and element `a : α`, `List.mapIdx (λ i x, f (i+1) x)) (a :: l) = [f 0 a] ++ List.mapIdx f l`.
|
List.mapIdx_eq_enum_map
theorem List.mapIdx_eq_enum_map :
∀ {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β), List.mapIdx f l = List.map (Function.uncurry f) l.enum
This theorem states that for any list `l` of type `α` and a two-argument function `f` that takes a natural number and an element of type `α` and returns an element of type `β`, the function `List.mapIdx` applied to `f` and `l` is equal to the function `List.map` applied to the uncurried version of `f` and the enumerated version of `l`. In other words, mapping a function over the indices and elements of a list is the same as enumerating the list (pairing each element with its index) and then mapping the function over these pairs.
More concisely: For any list `l` of type `α` and two-argument function `f` from `Nat × α` to `β`, `List.mapIdx f l` equals `List.map (λ (i, x), f i x) (Enumerable.enumType l)`.
|