Vector.reverse.proof_1
theorem Vector.reverse.proof_1 : ∀ {n : ℕ} {α : Type u_1} (v : Vector α n), v.toList.reverse.length = n
The theorem `Vector.reverse.proof_1` states that for any natural number `n` and any type `α`, if you have a vector `v` of type `α` with length `n`, then the length of the reversed list obtained from that vector is still `n`. This means that reversing a list does not change its length, even when the list is derived from a vector.
More concisely: For any natural number `n` and type `α`, the length of the reversed vector of size `n` in type `α` is equal to the original vector's length.
|
Vector.scanl_cons
theorem Vector.scanl_cons :
∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α n) (x : α),
Vector.scanl f b (x ::ᵥ v) = b ::ᵥ Vector.scanl f (f b x) v
The theorem `Vector.scanl_cons` says that for all types `α` and `β`, natural numbers `n`, a vector of length `n` with elements of type `α`, a function `f` from `β` and `α` to `β`, and an element `b` of type `β` and `x` of type `α`, the function `Vector.scanl` applied to `f`, `b`, and a vector created by appending `x` to the beginning of `v` is equal to a vector created by appending `b` to the beginning of the result of `Vector.scanl` applied to `f`, `f b x`, and `v`. This theorem essentially describes the step-by-step behavior of the function `Vector.scanl`, showing how it recursively applies the function `f` on the elements of the vector, starting with the initial value `b` and then using the result of each step as the initial value for the next step.
More concisely: For all types `α` and `β`, vectors `v` of length `n+1` in `α`, function `f` from `β` to `β`, and elements `b` of type `β` and `x` of type `α`, `Vector.scanl f b (cons x v) = cons b (Vector.scanl f (f b x) v)`.
|
Vector.scanl_val
theorem Vector.scanl_val :
∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) {v : Vector α n},
↑(Vector.scanl f b v) = List.scanl f b ↑v
The theorem `Vector.scanl_val` states that for any function `f` of type `β → α → β`, any value `b` of type `β`, and any vector `v` of type `Vector α n`, the underlying list of a vector obtained by applying the `Vector.scanl` function to `f`, `b`, and `v` is identical to the list obtained by applying the `List.scanl` function to `f`, `b`, and the underlying list of `v`. In other words, the `Vector.scanl` operation on a vector is equivalent to the `List.scanl` operation on the underlying list of the vector.
More concisely: For any function `f : β -> α -> β`, value `b : β`, and vector `v : Vector α n`, the underlying list of `Vector.scanl f b v` equals the list obtained by applying `List.scanl f b (toList v)`.
|
Vector.map_id
theorem Vector.map_id : ∀ {α : Type u_1} {n : ℕ} (v : Vector α n), Vector.map id v = v
This theorem states that mapping the identity function (`id`) over a vector does not change the vector. In other words, for any type `α` and any natural number `n`, if you have a vector `v` of length `n` with elements of type `α`, applying the `Vector.map` function with the identity function as the mapping function to `v` will yield `v` itself. This property is analogous to the identity property in mathematics, where applying the identity operation to any number returns the same number.
More concisely: For any type α and natural number n, the application of the identity function to a vector of length n using Vector.map does not change the original vector. In mathematical notation: ∀α n, Vector.map id v = v, where v is a vector of length n with elements of type α.
|
Vector.exists_eq_cons
theorem Vector.exists_eq_cons : ∀ {n : ℕ} {α : Type u_1} (v : Vector α n.succ), ∃ a as, v = a ::ᵥ as
The theorem `Vector.exists_eq_cons` states that for any natural number `n` and any type `α`, for any vector `v` of length `n+1` with elements of type `α`, there exists an element `a` of type `α` and a vector `as` such that `v` is the result of prepending `a` to `as`. In other words, any `n+1` length vector can be expressed as a head element followed by a vector of length `n`.
More concisely: For any natural number `n` and type `α`, given a vector `v` of length `n+1` in `α`, there exists an element `a` in `α` and a vector `as` of length `n` such that `v = [a] ++ as`.
|
Vector.tail_nil
theorem Vector.tail_nil : ∀ {α : Type u_1}, Vector.nil.tail = Vector.nil
This theorem states that the tail of an empty vector is also an empty vector, irrespective of the type of the elements that the vector is supposed to contain. More specifically, for any type `α`, if you take the tail (i.e., all elements except the first) of an empty vector, you still get an empty vector. This makes sense, as there are no elements to remove from an empty vector, so the result must still be an empty vector.
More concisely: For any type `α`, the tail of an empty vector of type `α vec` is an empty vector.
|
Vector.toList_scanl
theorem Vector.toList_scanl :
∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α n),
(Vector.scanl f b v).toList = List.scanl f b v.toList
The theorem `Vector.toList_scanl` states that for any natural number `n`, any types `α` and `β`, any function `f` from `β` to `α` to `β`, any value `b` of type `β`, and any `n`-element vector `v` of type `α`, the operation of first applying the `Vector.scanl` function to `f`, `b`, and `v` and then converting the result to a list is equivalent to first converting `v` to a list and then applying the `List.scanl` function to `f`, `b`, and the resulting list. In other words, scanning a vector from the left and then converting it to a list gives the same result as first converting the vector to a list and then scanning the list from the left.
More concisely: For any natural number `n`, type `α`, type `β`, function `f` from `β` to `α`, value `b` of type `β`, and vector `v` of length `n` of type `α`, `Vector.scanl f b v` converted to a list is equal to the list obtained by converting `v` to a list and applying `List.scanl f b`.
|
Vector.scanl_singleton
theorem Vector.scanl_singleton :
∀ {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α 1),
Vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ Vector.nil
The theorem `Vector.scanl_singleton` states that for any given function `f` of type `β → α → β`, a starting value `b` of type `β`, and a `Vector` `v` of length 1 with elements of type `α`, applying the `Vector.scanl` function to `f`, `b`, and `v` results in a new `Vector` of length 2 with the starting value `b` as the first element and the value computed by applying `f` to `b` and the head of `v` as the second element. In other words, the `Vector.scanl` function, when applied to a single-element vector, creates a new vector that starts with the provided starting value and ends with the result of applying the provided function to the starting value and the single element of the original vector.
More concisely: For any function `f : β -> α -> β` and `x : α`, `Vector.scanl f x [x] = [x, f x x]`.
|
Vector.scanl_nil
theorem Vector.scanl_nil :
∀ {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β), Vector.scanl f b Vector.nil = b ::ᵥ Vector.nil
This theorem states that for any function `f` of type `β → α → β` and a starting value `b` of type `β`, if we apply the `Vector.scanl` function to the empty vector (`Vector.nil`), the result is a vector with the starting value `b` as its only element. In other words, when we scan an empty vector from 0 to `Fin.last n` (which does not exist because the vector is empty) using `f` and `b`, we simply return a vector containing the starting value `b`.
More concisely: For any function `f : β -> α -> β` and value `b : β`, `Vector.scanl f b Vector.nil = singleton b`, where `singleton` is the constructor for a vector with a single element.
|
Vector.get_tail_succ
theorem Vector.get_tail_succ :
∀ {n : ℕ} {α : Type u_1} (v : Vector α n.succ) (i : Fin n), v.tail.get i = v.get i.succ
This theorem, `Vector.get_tail_succ`, states that for any natural number `n` and any type `α`, if you have a vector `v` of length `n+1` with elements of type `α`, and an index `i` less than `n`, then getting the `i`th element of the tail of `v` is the same as getting the `i+1`th element of `v`. In simple terms, the theorem is saying that the tail of a vector effectively shifts the indices of the elements by one, which is a common property of list-like structures when you remove the head.
More concisely: For any natural number `n` and type `α`, the `(i+1)`th element of a `n+1`-length vector `v` is equal to the `i`th element of its tail.
|
Vector.get_ofFn
theorem Vector.get_ofFn : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n), (Vector.ofFn f).get i = f i
The theorem `Vector.get_ofFn` states that for every type `α`, natural number `n`, function `f` mapping from `Fin n` to `α`, and `i` of type `Fin n`, when we get the `i`-th element from a vector created by applying `f` to every element of `Fin n` (through the function `Vector.ofFn`), it is equivalent to directly applying `f` to `i`. In other words, when we first construct a vector by applying a function to each element in a finite set, and then retrieve an element from the vector, it's the same as if we applied the function directly to the element.
More concisely: For every type `α`, natural number `n`, function `f` from `Fin n` to `α`, and `i` in `Fin n`, `Vector.get i (Vector.ofFn n f) = f i`.
|
Vector.singleton_tail
theorem Vector.singleton_tail : ∀ {α : Type u_1} (v : Vector α 1), v.tail = Vector.nil
The theorem `Vector.singleton_tail` states that for any vector `v` which has a single element of any type `α`, the tail of this vector is `nil`. This means that if you remove the first element from a one-element vector, you are left with an empty vector.
More concisely: For any vector `v` of length 1 over type `α`, `v.tail` equals the empty vector.
|
Vector.ext
theorem Vector.ext : ∀ {n : ℕ} {α : Type u_1} {v w : Vector α n}, (∀ (m : Fin n), v.get m = w.get m) → v = w
This theorem states that for any natural number `n` and any type `α`, two vectors `v` and `w` of type `α` and length `n` are equal if and only if their elements are equal at every index. These indices are represented by `m`, which is a finite number within the range of `0` to `n-1`. This means that if we can show that for all indices `m`, the `m`-th element of `v` is equal to the `m`-th element of `w`, then we can conclude that `v` is equal to `w`.
More concisely: For any natural number `n` and type `α`, two vectors `v` and `w` of length `n` over `α` are equal if and only if their corresponding elements are equal for all indices `m` in the range `0` to `n-1`.
|
Vector.scanl_get
theorem Vector.scanl_get :
∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α n) (i : Fin n),
(Vector.scanl f b v).get i.succ = f ((Vector.scanl f b v).get i.castSucc) (v.get i)
This theorem states that, for a function `f` from type `β` to `α` to `β`, an initial value `b` of type `β`, a vector `v` of length `n` with elements of type `α`, and an index `i` within `n`, the `i+1`-th element of the vector obtained by applying the scanl operation on `v` starting with `b` and using `f`, is equal to the result of applying `f` to the `i`-th element of the scanl vector and the `i`-th element of `v`. This is the version of the `scanl_cons` theorem that works with the `get` operation for accessing elements of vectors.
More concisely: For any function `f` from type `β` to `α` to `β`, initial value `b` of type `β`, vector `v` of length `n` with elements of type `α`, and index `i` within `n`, the `i+1`-th element of the scanl sequence `[b, f(b, v(0)), f(f(b, v(0)), v(1)), ..., f(f(...f(b, v(i-1)), v(i)))]` is equal to `f(v(i), v(i))`.
|
Vector.scanl_head
theorem Vector.scanl_head :
∀ {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α n), (Vector.scanl f b v).head = b
The theorem `Vector.scanl_head` asserts that for any natural number `n`, any type `α` and `β`, any function `f` from `β` to `α` to `β`, any starting value `b` of type `β`, and any vector `v` of type `Vector α n`, the first element of the `Vector.scanl` operation on vector `v` using function `f` and starting value `b` (which is retrieved using the `.head` method) is always equal to the starting value `b`. In simpler terms, it states that when performing a `scanl` operation (a cumulative operation from left to right) on a vector, the first result is always the initial value you started with.
More concisely: For any natural number `n`, any type `α` and `β`, any function `f : β -> α -> β`, any starting value `b : β`, and any vector `v : Vector α n`: The first element of `Vector.scanl f b v` is equal to `b`.
|
Vector.get_eq_get
theorem Vector.get_eq_get :
∀ {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n), v.get i = v.toList.get (Fin.cast ⋯ i)
This theorem states that for any natural number `n` and any type `α`, given a vector `v` of length `n` with elements of type `α` and an index `i` of type `Fin n`, the `i`-th element of the vector `v` obtained by `Vector.get` equals the `i`-th element of the list converted from the vector `v` using `Vector.toList`, where the index `i` is cast into an equal `Fin` type using `Fin.cast`. Essentially, this theorem confirms that the process of converting a vector to a list preserves the ordering of elements.
More concisely: For any natural number `n` and type `α`, given a vector `v` of length `n` with elements of type `α`, the `i`-th element of `Vector.get v i` equals the `i`-th element of the list obtained by `Vector.toList v`, where `i` is treated as a `Fin n`.
|
Vector.reverse_get_zero
theorem Vector.reverse_get_zero : ∀ {n : ℕ} {α : Type u_1} {v : Vector α (n + 1)}, v.reverse.head = v.last
This theorem states that for any given vector `v` of type `α` with length `n + 1`, the first element of the reversed vector is equal to the last element of the original vector. In other words, if you take any list of specified length `n + 1` and flip it around, the first item in this new reversed list will be the same as the last item in the original list.
More concisely: For any vector `v` of length `n + 1` over type `α`, the first and last elements are equal: `v(0) = v(n)`.
|
Vector.toList_reverse
theorem Vector.toList_reverse : ∀ {n : ℕ} {α : Type u_1} {v : Vector α n}, v.reverse.toList = v.toList.reverse := by
sorry
The theorem `Vector.toList_reverse` states that for any natural number `n`, any type `α`, and any vector `v` that is of type Vector with elements of type `α` and of length `n`, if you reverse the vector and then convert it to a list, you will get the same result as if you had first converted the vector to a list and then reversed the list. In other words, the process of reversing a vector and then converting it to a list is equivalent to first converting the vector to a list and then reversing the list.
More concisely: For any natural number `n` and type `α`, the conversion of the reversed vector `(Vector.reverse : Vector α n)` to a list and then the reversal of that list is equal to the reversal of the original vector `v : Vector α n` followed by its conversion to a list. In symbols: `List.reverse (List.fromVec v) = List.reverse (List.fromVec (Vector.reverse v))`.
|
Vector.toList_singleton
theorem Vector.toList_singleton : ∀ {α : Type u_1} (v : Vector α 1), v.toList = [v.head]
The theorem `Vector.toList_singleton` says that for any vector `v`, which is of type `Vector` and has a length of 1 with elements of type `α`, the list obtained from it via `toList` is the same as the list that contains only the head of the vector `v`. In other words, if you have a single-element vector, converting it to a list gives you a single-element list containing the same element.
More concisely: For any single-element vector `v` of type `Vector α` in Lean, `toList v` is equal to the list containing its unique element `v.head`.
|
Vector.get_cons_nil
theorem Vector.get_cons_nil : ∀ {α : Type u_1} {ix : Fin 1} (x : α), (x ::ᵥ Vector.nil).get ix = x
This theorem states that in a vector of type `α` that consists of only one element `x`, accessing the `n`th (where `n` ranges over a finite set `Fin`) element will always yield `x` itself. In other words, no matter what index you try to access within the boundaries of the vector, you will always get the single element contained in the vector since it's the only element present.
More concisely: For any vector `v` of length 1 over type `α`, and any index `n` in the finite set `Fin`, the `n`-th element of `v` is equal to the unique element `x` in `v`, i.e., `v!(n) = x`.
|
Vector.ofFn_get
theorem Vector.ofFn_get : ∀ {n : ℕ} {α : Type u_1} (v : Vector α n), Vector.ofFn v.get = v
The theorem `Vector.ofFn_get` states that for any natural number `n` and any type `α`, given a vector `v` of length `n` with elements of type `α`, if we create a new vector by applying the function `Vector.get v` to each element of a `Fin n` type (essentially, this is a function that retrieves the elements of `v`), we get back the original vector `v`. In other words, this theorem says that retrieving all elements from a vector and constructing a new vector from them gives us the original vector.
More concisely: For any natural number `n` and type `α`, the application of the `Vector.get` function to each element of a vector `v` of length `n` over `α` results in the original vector `v`. In mathematical notation: for all `n : ℕ` and `α`, `∀ i : Fin n, Vector.get v i = v.get i`.
|
Vector.get_cons_succ
theorem Vector.get_cons_succ :
∀ {n : ℕ} {α : Type u_1} (a : α) (v : Vector α n) (i : Fin n), (a ::ᵥ v).get i.succ = v.get i
This theorem states that for any natural number `n`, any type `α`, any element `a` of type `α`, any vector `v` of length `n` with elements of type `α`, and any `i` in the finite set of first `n` natural numbers, the (`i+1`)th element of the vector which is formed by appending `a` at the start of `v`, is the same as the `i`th element of the original vector `v`. In other words, prepending an element to a vector and then accessing the successor of an index, is the same as accessing the element at the original index in the original vector.
More concisely: For any natural number `n`, any type `α`, any `a : α`, any vector `v : α^n`, and any index `i : ℕ`, the `(i+1)`th element of `[a | v]` equals the `i`th element of `v`.
|
Vector.last_def
theorem Vector.last_def : ∀ {n : ℕ} {α : Type u_1} {v : Vector α (n + 1)}, v.last = v.get (Fin.last n)
The theorem `Vector.last_def` states that for any natural number `n`, any type `α`, and any vector `v` of type `α` with length `n + 1`, the last element of the vector `v` is the same as the element at the "greatest" index position in the vector, where the index position is defined by `Fin.last n`. In other words, when you have a vector with at least one element, getting the last element of the vector is equivalent to getting the element at the highest index position.
More concisely: For any natural number `n` and type `α`, the last element of a vector `v` of length `n+1` over `α` is equal to the element at index `Fin.last n` in `v`.
|
Vector.get_zero
theorem Vector.get_zero : ∀ {n : ℕ} {α : Type u_1} (v : Vector α n.succ), v.get 0 = v.head
This theorem, referred to as `Vector.get_zero`, states that for any natural number `n` and any type `α`, given a vector `v` of length `n+1` with elements of type `α`, the first element of the vector obtained using the `Vector.get` function with an index of `0` is equal to the first element of the vector as obtained by the `Vector.head` function. In other words, it confirms that both `Vector.get v 0` and `Vector.head v` retrieve the same first element from a vector `v` of non-zero length.
More concisely: For any vector `v` of length `n+1` and type `α`, `Vector.get v 0 = Vector.head v`.
|