Vector.mapAccumr₂_unused_input_left
theorem Vector.mapAccumr₂_unused_input_left :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} {s : σ} [inst : Inhabited α]
(f : α → β → σ → σ × γ),
(∀ (a : α) (b : β) (s : σ), f default b s = f a b s) →
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr (fun b s => f default b s) ys s
This theorem states that given a function `f` of type `α → β → σ → σ × γ` and vectors `xs : Vector α n` and `ys : Vector β n`, if `f` returns the same output and next state for every value of its first argument, then `xs` can be ignored. As a result, the function `Vector.mapAccumr₂` can be rewritten as `Vector.mapAccumr` that takes as input `f`, `ys`, and an initial state `s`, where `f` is now a function that uses the default value of `α` as its first argument. This theorem is stated for all types `α`, `β`, `σ`, and `γ`, an integer `n`, and an initial state `s` of type `σ`. The type `α` is assumed to be inhabited, which means that there is at least one value of type `α`.
More concisely: Given a commutative function `f : α -> β -> σ -> σ × γ`, if `f (x i) (y j) = (g i, h j)` for all `i, j`, then `Vector.mapAccumr₂ f xs ys` is equivalent to `Vector.mapAccumr (λ _ y, (id, y)) ys` for any `Vector α n` `xs` and `Vector β n` `ys`.
|
Vector.mapAccumr₂_eq_map₂
theorem Vector.mapAccumr₂_eq_map₂ :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} {f : α → β → σ → σ × γ} {s₀ : σ}
(S : Set σ),
s₀ ∈ S →
(∀ (a : α) (b : β), ∀ s ∈ S, (f a b s).1 ∈ S) →
(∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) →
(Vector.mapAccumr₂ f xs ys s₀).2 = Vector.map₂ (fun x x_1 => (f x x_1 s₀).2) xs ys
The theorem `Vector.mapAccumr₂_eq_map₂` states that given certain conditions, we can simplify the complex operation of mapping across two vectors with `Vector.mapAccumr₂`, which involves an accumulating function `f` and an initial state `s₀`, to simply using `Vector.map₂`. The conditions required are:
1. We have a set `S` of states, which includes our initial state `s₀`.
2. This set `S` is closed under the function `f`, meaning that applying `f` to any elements of the set produces an output that is still within the set.
3. The output `γ` of `f` is the same for all states in `S`, regardless of the state used in the calculation.
Under these conditions, the theorem says that the second component of the output from `Vector.mapAccumr₂` is identical to the output from `Vector.map₂`, where the function used is the second component of `f`, ignoring the state.
More concisely: If `S` is a set containing the initial state `s₀` and is closed under the function `f` such that for all states `s` in `S`, `f s` has the same output `γ`, then `Vector.mapAccumr₂ f s₀` equals `Vector.map₂ (snd ∘ f)`.
|
Vector.mapAccumr₂_eq_map₂_of_constant_state
theorem Vector.mapAccumr₂_eq_map₂_of_constant_state :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} (f : α → β → σ → σ × γ) (s : σ),
(∀ (a : α) (b : β), (f a b s).1 = s) →
Vector.mapAccumr₂ f xs ys s = (s, Vector.map₂ (fun x y => (f x y s).2) xs ys)
This theorem asserts that for any accumulation function `f` operating on elements of types `α` and `β` and producing a state of type `σ` and a result of type `γ`, along with an initial state `s` of type `σ`, a vector `xs` of elements of type `α` and a vector `ys` of elements of type `β`, if `f` always returns the same state `s` for any inputs `(a, b)`, where `a` is an element of `α` and `b` is an element of `β`, then applying the accumulation function `f` on the vectors `xs` and `ys` starting with the state `s` is equivalent to just mapping over the vectors `xs` and `ys` with a function that uses `f` but discards the state.
More concisely: Given an accumulation function `f` from types `α × β` to `σ × γ`, an initial state `s` of type `σ`, and vectors `xs` and `ys` of length `n` from types `α` and `β` respectively, if `f` is stateful but functional in its arguments, i.e., `f(a, b) = (s', r)` implies `s' = s` for all `a : α` and `b : β`, then evaluating `f` on pairs of elements from `xs` and `ys` is equivalent to mapping `f` over `xs` and `ys` and discarding the state. In mathematical notation: `(∀ i, f (xs!i, ys!i) = (s, r)) ⟹ (∀ i, r) = (⋈j, f xs!j ys!j)` where `xs!i`, `ys!i`, and `f xs!j ys!j` denote the `i`-th elements of `xs`, `ys`, and the application of `f` to the `i`-th pair of elements from `xs` and `ys`, respectively.
|
Vector.mapAccumr_eq_map
theorem Vector.mapAccumr_eq_map :
∀ {α : Type u_2} {n : ℕ} {β : Type u_1} {xs : Vector α n} {σ : Type} {f : α → σ → σ × β} {s₀ : σ} (S : Set σ),
s₀ ∈ S →
(∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S) →
(∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) →
(Vector.mapAccumr f xs s₀).2 = Vector.map (fun x => (f x s₀).2) xs
This theorem states that if there is a set of states (`S`) which is closed under a function `f` and the output of `f` is identical for all states in `S`, then the state is not needed. In this situation, the `Vector.mapAccumr` function can be rewritten as just `Vector.map`.
Practically, this means given any predetermined initial state `s₀` in set `S`, and a vector `xs` of arbitrary length `n`, the function `f` that maps a value `α` and a state `σ` to a new state and a value `β`, behaves in such a way that:
1) Every state resulting from applying `f` to any `a` of type `α` and any state `s` in `S` always stays in `S`.
2) The second component of the output of `f`, when applied to any `a` of type `α` and any two states `s` and `s'` both in `S`, is always the same.
If these conditions hold, then the output vector of applying `Vector.mapAccumr` with `f` over `xs` starting with state `s₀` is equivalent to that of `Vector.map` directly using the second component output of applying `f` to `x` in `xs` and the initial state `s₀` over `xs`.
More concisely: If a function `f` maps a set `S` of states closed under `f` to new states such that the output value is constant for all pairs of states in `S`, then applying `Vector.mapAccumr` with `f` is equivalent to applying `Vector.map` with the output value of `f` on each element of a vector.
|
Vector.mapAccumr₂_eq_map₂_of_unused_state
theorem Vector.mapAccumr₂_eq_map₂_of_unused_state :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} (f : α → β → σ → σ × γ) (s : σ),
(∀ (a : α) (b : β) (s s' : σ), (f a b s).2 = (f a b s').2) →
(Vector.mapAccumr₂ f xs ys s).2 = Vector.map₂ (fun x y => (f x y s).2) xs ys
This theorem states that if an accumulation function 'f' always produces the same second component of its output pair, regardless of the state of accumulation, then the accumulation state is redundant and can be simplified. More specifically, given vectors 'xs' and 'ys' of types α and β respectively, a function 'f' from α, β and state σ to a pair of σ and γ, and a state 's', if for all elements 'a' from α, 'b' from β, and states 's' and 's'', the second component of the output of 'f' is always the same, then the result of mapping function 'f' over vectors 'xs' and 'ys' with accumulation 's' and then taking the second component is the same as the result of mapping a function (that takes two inputs 'x' and 'y', applies 'f' to 'x', 'y', and state 's', and then takes the second component) over vectors 'xs' and 'ys'. In other words, if the second component of the output of 'f' does not depend on the state, then the accumulation operation can be replaced by a simpler mapping operation.
More concisely: If a function's second component is constant with respect to its accumulation state, then mapping the function over vectors and taking the second component is equivalent to applying a simpler function that takes two inputs and only depends on the first input.
|
Vector.mapAccumr_eq_map_of_unused_state
theorem Vector.mapAccumr_eq_map_of_unused_state :
∀ {α : Type u_2} {n : ℕ} {β : Type u_1} {xs : Vector α n} {σ : Type} (f : α → σ → σ × β) (s : σ),
(∀ (a : α) (s s' : σ), (f a s).2 = (f a s').2) →
(Vector.mapAccumr f xs s).2 = Vector.map (fun x => (f x s).2) xs
This theorem states that if there exists an accumulation function `f` of type `α → σ → σ × β`, where `α`, `β`, and `σ` are some types, that produces the same output regardless of the accumulation state, then the state is redundant and can be eliminated. More specifically, given a vector `xs` of type `α` and length `n`, and a state `s` of type `σ`, if for any elements `a` of type `α` and states `s` and `s'` of type `σ`, the second component of `f a s` equals the second component of `f a s'`, then the second component of `Vector.mapAccumr f xs s` (i.e., the result of running `f` over `xs` with initial state `s` and collecting the intermediate results) is equal to the result of mapping `xs` under the function `(λx, (f x s).2)`. This essentially means that if the output of `f` is independent of its state input, the state information is not necessary and can be ignored.
More concisely: If a function `f : α -> σ -> σ × β` has the property that `f a s = f a s'` implies `s = s'`, then `Vector.mapAccumr f xs s` equals `Vector.map (λx, f x s).2 xs`, for any vector `xs` of length `n` and type `α`.
|
Vector.mapAccumr_redundant_pair
theorem Vector.mapAccumr_redundant_pair :
∀ {α : Type u_2} {n : ℕ} {β : Type u_1} {xs : Vector α n} {σ : Type} {s : σ} (f : α → σ × σ → (σ × σ) × β),
(∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2) →
(Vector.mapAccumr f xs (s, s)).2 = (Vector.mapAccumr (fun x s => ((f x (s, s)).1.1, (f x (s, s)).2)) xs s).2
This theorem, named `Vector.mapAccumr_redundant_pair`, states that if we have a function `f`, which takes an element of type `α` and a pair of states of type `σ`, always producing a pair where both elements are the same, then we can simplify this function to only require a single state. In particular, when we apply `Vector.mapAccumr` with `f` to a vector `xs` and a pair of identical states `(s, s)`, it will yield the same results as applying `Vector.mapAccumr` with a simplified version of `f` that only takes a single state, to the same vector `xs` and single state `s`. The simplified version of `f` is defined as `(fun x s => ((f x (s, s)).1.1, (f x (s, s)).2))`, which preserves the behavior of `f` but only requires a single state.
More concisely: If `f` is a function that maps an element of type `α` to a pair of identical states, then `Vector.mapAccumr` applying `f` to a vector and a pair of identical states is equivalent to applying a simplified version of `f` that only takes a single state to the same vector and single state.
|
Vector.mapAccumr_eq_map_of_constant_state
theorem Vector.mapAccumr_eq_map_of_constant_state :
∀ {α : Type u_2} {n : ℕ} {β : Type u_1} {xs : Vector α n} {σ : Type} (f : α → σ → σ × β) (s : σ),
(∀ (a : α), (f a s).1 = s) → Vector.mapAccumr f xs s = (s, Vector.map (fun x => (f x s).2) xs)
The theorem `Vector.mapAccumr_eq_map_of_constant_state` states that for any type `α`, natural number `n`, type `β`, vector `xs` of length `n` with elements of type `α`, and type `σ`, if a function `f` maps `α` and `σ` to a pair of `σ` and `β` such that for all elements of type `α`, the first component of the pair (which is of type `σ`) is equal to the original `σ` (`s`), then running this function over the vector `xs` with the initial state `s` using `Vector.mapAccumr` is equivalent to just mapping the vector `xs` under the function which maps an element of type `α` to the second component of `f` applied to `α` and `s` (ignoring the fact that `f` also produces a state of type `σ`). In other words, if the state `σ` doesn't change during the accumulation process, it can be ignored, effectively simplifying the `Vector.mapAccumr` operation to a `Vector.map` operation.
More concisely: If `f : α → σ × β` is a function with constant second component when mapped over elements of type `α`, then `Vector.mapAccumr f s xs = Vector.map (snd ∘ f) xs`, where `s` is the initial state and `Vector.mapAccumr` and `Vector.map` are applied to a vector `xs` of length `n` with elements of type `α`.
|
Vector.mapAccumr₂_redundant_pair
theorem Vector.mapAccumr₂_redundant_pair :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} {s : σ}
(f : α → β → σ × σ → (σ × σ) × γ),
(∀ (x : α) (y : β) (s : σ),
let s' := (f x y (s, s)).1;
s'.1 = s'.2) →
(Vector.mapAccumr₂ f xs ys (s, s)).2 =
(Vector.mapAccumr₂ (fun x y s => ((f x y (s, s)).1.1, (f x y (s, s)).2)) xs ys s).2
The theorem `Vector.mapAccumr₂_redundant_pair` states that if we have a function `f` that operates on pairs of elements from two vectors (of types `α` and `β`, and of equal length `n`), and a pair of states `(s, s)` (where `s` is of type `σ`), such that `f` always returns the same value for both elements of the state pair, then the resultant vector from applying `f` across the pair of input vectors with the state pair `(s, s)` is the same as the resultant vector from applying a modified function on the input vectors with a single state `s`. The modified function takes the first element of the pair returned by `f`. In other words, if the state pair is redundant in the function `f`, it can be simplified to a single state without affecting the computation on the vectors.
More concisely: If `f` is a function that maps pairs of elements from vectors `X : vector α n` and `Y : vector β n` to a pair `(c, s)` such that `f x y = (g x, s)` for all `x : α` and `y : β`, then `Vector.mapAccumr₂ f (X, Y) (s, s) = Vector.mapAccumr (g) X s`.
|
Vector.mapAccumr₂_unused_input_right
theorem Vector.mapAccumr₂_unused_input_right :
∀ {α : Type} {n : ℕ} {β : Type} {xs : Vector α n} {ys : Vector β n} {σ γ : Type} {s : σ} [inst : Inhabited β]
(f : α → β → σ → σ × γ),
(∀ (a : α) (b : β) (s : σ), f a default s = f a b s) →
Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr (fun a s => f a default s) xs s
The theorem `Vector.mapAccumr₂_unused_input_right` states that if we have a function `f` which takes three arguments of types `α`, `β` and `σ` and returns a pair of type `σ × γ`, and this function always returns the same output and next state regardless of its second argument (of type `β`), then we can replace a call to `Vector.mapAccumr₂` using `f` and two vectors `xs` and `ys` (with `ys` of type `Vector β n`) with a call to `Vector.mapAccumr` using a new function that ignores its second argument.
In other words, if the function `f` is independent of its second argument, then the `β` vector `ys` is not used in `Vector.mapAccumr₂` and can be eliminated. This is formalized by the equality `Vector.mapAccumr₂ f xs ys s = Vector.mapAccumr (fun a s => f a default s) xs s`, where `default` is a placeholder for the unused `β` values.
More concisely: If `f` is a function that takes two arguments and returns a pair, where the second argument is always ignored and `Vector.mapAccumr₂` applies `f` to corresponding elements of two vectors `xs` and `ys`, then `Vector.mapAccumr₂ f xs ys s` is equal to `Vector.mapAccumr (fun a s => f a default) xs s`, where `default` is a constant value for the unused second argument in `ys`.
|