Vector.map_cons
theorem Vector.map_cons :
∀ {α : Type u} {β : Type v} {n : ℕ} (f : α → β) (a : α) (v : Vector α n),
Vector.map f (a ::ᵥ v) = f a ::ᵥ Vector.map f v
The theorem `Vector.map_cons` states that for any types `α` and `β`, any natural number `n`, any function `f` from `α` to `β`, any element `a` of type `α`, and any `n`-length vector `v` of elements of type `α`, applying the function `f` to each element of the vector that results from cons-ing `a` onto `v` (using the vector-specific version of the cons operator `::ᵥ`) results in the same vector as cons-ing `f a` onto the result of mapping `f` over `v`. In other words, for vectors, mapping and cons-ing commute with each other.
More concisely: For any types α and β, natural number n, function f : α → β, element a : α, and vectors xs : vector α (len n), the application of the function f to the cons-ed element a and the resulting vector obtained by mapping f over xs is equal to the cons of f a to the result of mapping f over xs. In symbols: (∀ i : nat, f (xs.get i) = (map f xs).push (f a)).
|
Vector.toList_length
theorem Vector.toList_length : ∀ {α : Type u} {n : ℕ} (v : Vector α n), v.toList.length = n
The theorem `Vector.toList_length` asserts that for any vector `v` which is of length `n` and has elements of type `α`, when the vector is converted to a list using the function `Vector.toList`, the length of the resulting list is `n`. In other words, the transformation of a vector into a list preserves the size.
More concisely: For any vector `v` of length `n` and type `α`, the length of `Vector.toList v` is equal to `n`.
|
Vector.toList_cons
theorem Vector.toList_cons : ∀ {α : Type u} {n : ℕ} (a : α) (v : Vector α n), (a ::ᵥ v).toList = a :: v.toList := by
sorry
The theorem `Vector.toList_cons` states that for any type `α`, any natural number `n`, any element `a` of type `α`, and any vector `v` of length `n` with elements of type `α`, if you construct a new vector by prepending `a` to `v` and then convert this vector to a list, you get the same result as if you first convert `v` to a list and then prepend `a` to this list. In other words, converting a vector to a list preserves the operation of prepending an element.
More concisely: For any type α, natural number n, element a of α, and vector v of length n in α, the conversion of the vector obtained by prepending a to v to a list is equal to the list obtained by prepending a to the list representation of v.
|
Vector.eq_nil
theorem Vector.eq_nil : ∀ {α : Type u} (v : Vector α 0), v = Vector.nil
This theorem states that for any type `α`, any vector of length `0` of type `α` is the same as the `nil` vector of type `α`. In other words, there is only one vector of length `0` for any given type `α`, and that is the `nil` vector. This is because a vector of length `0` cannot contain any elements, so it must be empty, which is exactly what the `nil` vector is.
More concisely: For any type `α`, the unique vector of length 0 is equal to the nil vector of type `α`.
|
Vector.head_cons
theorem Vector.head_cons : ∀ {α : Type u} {n : ℕ} (a : α) (v : Vector α n), (a ::ᵥ v).head = a
The theorem `Vector.head_cons` states that for any type `α`, any natural number `n`, any element `a` of type `α`, and any vector `v` of length `n` with elements of type `α`, if we prepend the element `a` to the vector `v`, the head of the resulting vector (i.e., the first element) is the element `a` that was prepended. In other words, this theorem is about the property of the `head` operation on vectors, asserting that the head of a vector obtained by prepending an element is indeed the element that was prepended.
More concisely: For any type `α`, any natural number `n`, any `α` element `a`, and any vector `v` of length `n` in `α`, the head of the vector obtained by prepending `a` to `v` is equal to `a`.
|
Vector.map_nil
theorem Vector.map_nil : ∀ {α : Type u} {β : Type v} (f : α → β), Vector.map f Vector.nil = Vector.nil
This theorem, `Vector.map_nil`, states that for any function `f` mapping from a type `α` to a type `β`, if you apply this function to an empty vector of type `α` (`Vector.nil`), the result will be an empty vector of type `β`. This is analogous to the mathematical concept that applying a function to an empty set results in an empty set. This theorem thus captures an important property of functions when applied to empty collections.
More concisely: For any function `f` from type `α` to type `β`, `Vector.map f Vector.nil` equals `Vector.nil` of type `Vector β`.
|
Vector.toList_drop
theorem Vector.toList_drop :
∀ {α : Type u} {n m : ℕ} (v : Vector α m), (Vector.drop n v).toList = List.drop n v.toList
This theorem states that the `drop` operation on vectors is analogous to the `drop` operation on lists when the vector is converted to a list using `toList`. In other words, for every type `α` and natural numbers `n` and `m`, if we have a vector `v` of length `m` with elements of type `α`, then dropping the first `n` elements from `v` and converting the resulting vector to a list gives the same list as first converting `v` to a list and then dropping the first `n` elements from the resulting list.
More concisely: For all types `α` and natural numbers `n` and `m`, if `v` is a vector of length `m` with elements of type `α`, then `drop n (toList (vector.init n v)) = take (m - n) (drop n (toList v))`.
|
Vector.toList_take
theorem Vector.toList_take :
∀ {α : Type u} {n m : ℕ} (v : Vector α m), (Vector.take n v).toList = List.take n v.toList
This theorem states that for any type `α`, and for any natural numbers `n` and `m`, and for any vector `v` of length `m` with elements of type `α`, the operation of taking the first `n` elements from the vector `v` and then converting it to a list is equivalent to first converting the vector `v` to a list and then taking the first `n` elements from that list. In other words, taking elements from a vector and then turning it into a list is the same as turning the vector into a list first and then taking elements from it.
More concisely: For any type `α`, natural numbers `n` and `m`, and vector `v` of length `m` with elements of type `α`, the sublist of `v` of length `n` is equal to the sublist of the list obtained from `v` of the first `n` elements.
|
Vector.tail_cons
theorem Vector.tail_cons : ∀ {α : Type u} {n : ℕ} (a : α) (v : Vector α n), (a ::ᵥ v).tail = v
This theorem, `Vector.tail_cons`, states that for any type `α` and a non-negative integer `n`, if an element `a` of type `α` is prepended to a vector `v` of length `n` and type `α`, then taking the tail of the new vector results in the original vector `v`. In other words, prepending a value to a vector and immediately removing it leaves the original vector unchanged.
More concisely: For any type `α` and non-negative integer `n`, prepending an element `a` to a vector `v` of length `n` results in a vector `x` such that `x.tail = v`.
|
Vector.toList_nil
theorem Vector.toList_nil : ∀ {α : Type u}, Vector.nil.toList = []
This theorem states that for all types `α`, the list representation of an empty vector (a vector with no elements) of type `α` is an empty list. This means that, no matter what type of elements the vector is meant to contain, when it's empty and converted to a list, it results in an empty list.
More concisely: For all types `α`, the empty vector of type `α` is equivalent to the empty list when converted to a list.
|
Vector.eq
theorem Vector.eq : ∀ {α : Type u} {n : ℕ} (a1 a2 : Vector α n), a1.toList = a2.toList → a1 = a2
This theorem states that for any type `α` and for any natural number `n`, if two vectors `a1` and `a2` of length `n` with elements of type `α` have the same underlying list, then `a1` and `a2` are equal. In other words, the equality of two vectors is determined entirely by the equality of their underlying lists.
More concisely: For any type `α` and natural number `n`, if two `n`-vectors `a1` and `a2` of type `α` have the same underlying lists, then `a1 = a2`.
|
Vector.cons_head_tail
theorem Vector.cons_head_tail : ∀ {α : Type u} {n : ℕ} (v : Vector α n.succ), v.head ::ᵥ v.tail = v
The theorem `Vector.cons_head_tail` states that for any vector `v` of length `n+1` with elements of any type `α`, if you prepend the head of `v` to the tail of `v`, you get back the original vector `v`. In other words, it asserts that the operation of taking the head and tail of a vector and then reassembling them through prepending does not change the vector.
More concisely: For any vector `v` of length `n+1` over type `α`, `v = cons (hd v) (tl v)`.
|
Vector.toList_mk
theorem Vector.toList_mk : ∀ {α : Type u} {n : ℕ} (v : List α) (P : v.length = n), Vector.toList ⟨v, P⟩ = v
The theorem `Vector.toList_mk` states that for any type `α`, natural number `n` and list `v` of type `α`, given a proof `P` that the length of `v` equals `n`, the list obtained from a vector created from `v` and `P` is indeed `v`. In other words, the function `Vector.toList` converts a vector back to its original list form.
In slightly more mathematical terms, the theorem is saying that if we create a vector from a list, ensuring that the length of the list matches the declared length of the vector, when we convert this vector back to a list using `Vector.toList`, we get the original list back. This provides evidence of the bi-directionality between lists and vectors under these conditions.
More concisely: For any type `α` and natural number `n`, if `v` is a list of length `n` and `x : Vector α n`, then `Vector.toList x = v` holds.
|
Vector.toList_append
theorem Vector.toList_append :
∀ {α : Type u} {n m : ℕ} (v : Vector α n) (w : Vector α m), (v.append w).toList = v.toList ++ w.toList
This theorem states that for any types `α`, and any natural numbers `n` and `m`, appending two vectors `v` and `w` of lengths `n` and `m` respectively (where the vectors contain elements of type `α`), is equivalent to appending the corresponding lists of `v` and `w` when the vectors are converted to lists using the function `toList`. In other words, the operation of appending vectors corresponds directly to the operation of appending lists when the vectors are viewed as lists.
More concisely: For any types `α` and natural numbers `n` and `m`, the concatenation of vectors `v` of length `n` and `w` of length `m` over `α` is equivalent to the concatenation of the lists obtained by converting `v` and `w` to lists using `toList`.
|
Vector.nil.proof_1
theorem Vector.nil.proof_1 : ∀ {α : Type u_1}, [].length = [].length
The theorem `Vector.nil.proof_1` states that for all types `α`, the length of an empty list is equal to the length of another empty list. This might seem trivial, but it's an important foundational piece in Lean's type theory that ensures consistency when dealing with lists of any type.
More concisely: The theorem asserts that the length of an empty list is equal to 0, for all types α.
|