Vector.map_snoc
theorem Vector.map_snoc :
∀ {α : Type u_2} {n : ℕ} (xs : Vector α n) {α_1 : Type u_1} {f : α → α_1} {x : α},
Vector.map f (xs.snoc x) = (Vector.map f xs).snoc (f x)
The `Vector.map_snoc` theorem states that for any type `α`, a natural number `n`, a vector `xs` of length `n` with elements of type `α`, another type `α_1`, a function `f` from `α` to `α_1`, and an element `x` of type `α`, mapping function `f` over a vector that results from appending `x` to `xs` is equivalent to appending `f(x)` to the vector that results from mapping `f` over `xs`. In other words, if we first append an element to a vector and then apply a function to each element of the vector, it's the same as if we first applied the function to each element of the vector and the element, and then appended the result to the transformed vector.
More concisely: For any type `α`, vector `xs : α^n`, function `f : α → α₁`, and elements `x : α` and `y : α₁`, `(f <$> (xs ++ [x]) = (xs ++ [x]) ++ [f x])` holds in Lean.
|
Vector.mapAccumr_snoc
theorem Vector.mapAccumr_snoc :
∀ {α : Type u_2} {n : ℕ} (xs : Vector α n) {α_1 : Type} {β : Type u_1} {f : α → α_1 → α_1 × β} {x : α} {s : α_1},
Vector.mapAccumr f (xs.snoc x) s =
let q := f x s;
let r := Vector.mapAccumr f xs q.1;
(r.1, r.2.snoc q.2)
The theorem `Vector.mapAccumr_snoc` states that for any types `α`, `α_1`, and `β`, any natural number `n`, any vector `xs` of length `n` with elements of type `α`, any function `f` from `α` and `α_1` to a pair of `α_1` and `β`, any element `x` of type `α`, and any element `s` of type `α_1`, the result of mapping function `f` over the vector obtained by appending `x` to the end of `xs` and starting with `s` is equal to a pair. The first element of the pair is the first element of the result of mapping function `f` over `xs` starting with `f(x, s).1`, and the second element of the pair is the result of appending `f(x, s).2` to the end of the second element of the result of mapping function `f` over `xs` starting with `f(x, s).1`.
More concisely: For any types `α`, `α_1`, and `β`, any natural number `n`, any vector `xs : α^n`, any function `f : α × α_1 → (α_1, β)`, any `x : α`, and any `s : α_1`, `mapAccumr f (xs ++ [x]) s = (foldl f (map f xs) s.1, s.2 ++ foldl f (map f xs) s.1)`.
|
Vector.mapAccumr₂_snoc
theorem Vector.mapAccumr₂_snoc :
∀ {α : Type} {n : ℕ} {β : Type} (xs : Vector α n) (ys : Vector β n) {σ φ : Type} {c : σ} (f : α → β → σ → σ × φ)
(x : α) (y : β),
Vector.mapAccumr₂ f (xs.snoc x) (ys.snoc y) c =
let q := f x y c;
let r := Vector.mapAccumr₂ f xs ys q.1;
(r.1, r.2.snoc q.2)
The theorem `Vector.mapAccumr₂_snoc` in Lean 4 states that for any two vectors `xs` and `ys` of equal length `n`, any types `α`, `β`, `σ`, `φ`, a function `f` that operates on types `α`, `β`, and `σ`, and any elements `x` of type `α` and `y` of type `β` and `c` of type `σ`, applying the `mapAccumr₂` function to the vectors obtained by appending `x` to `xs` and `y` to `ys` is equal to applying `f` to `x`, `y`, and `c`, then applying `mapAccumr₂` to `xs`, `ys`, and the first element of the result from `f`, and finally appending the second element of the result from `f` to the second element of the result from `mapAccumr₂`.
In other words, it states that the process of mapping and accumulating a function `f` over two vectors extended by `x` and `y` is equivalent to the process of mapping and accumulating the function `f` over the original vectors and then appending the result of `f` applied to `x`, `y`, and `c` to the end.
More concisely: For equal-length vectors `xs` and `ys` of type `α List`, the application of `mapAccumr₂ f (x :: xs) (y :: ys) c` is equal to `let (acc, last) := mapAccumr₂ f xs ys c in (f x y :: acc, last)`.
|
Vector.map₂_snoc
theorem Vector.map₂_snoc :
∀ {α : Type u_2} {n : ℕ} {β : Type u_3} (xs : Vector α n) (ys : Vector β n) {α_1 : Type u_1} {f : α → β → α_1}
{x : α} {y : β}, Vector.map₂ f (xs.snoc x) (ys.snoc y) = (Vector.map₂ f xs ys).snoc (f x y)
The theorem `Vector.map₂_snoc` states that for all types `α`, `β`, `α_1`, and natural number `n`, and for all vectors `xs` of length `n` with elements of type `α`, `ys` of length `n` with elements of type `β`, elements `x` of type `α`, `y` of type `β`, and a binary function `f` from `α` and `β` to `α_1`, mapping two vectors extended by `x` and `y` respectively with the function `f` is equivalent to extending the vector resulting from mapping the original two vectors with `f` by the result of applying `f` to `x` and `y`. In other words, it verifies the property that appending elements to two vectors and then applying a binary operation is the same as applying the binary operation first and then appending the result of applying the binary operation to the appended elements.
More concisely: For all types `α`, `β`, and `α_1`, and for all vectors `xs : Vector α of length n`, `ys : Vector β of length n`, binary function `f : α × β → α_1`, and elements `x : α`, `y : β`, `Vector.map₂ f (xs ++ [x]) (ys ++ [y]) = (Map.map2 f xs ys) ++ [f x y]`.
|