Mathlib.Data.Vector.Defs

List.Vector definition

(α : Type u) (n : ℕ)

Full source

/--
`List.Vector α n` is the type of lists of length `n` with elements of type `α`.

Note that there is also `Vector α n` in the root namespace,
which is the type of *arrays* of length `n` with elements of type `α`.

Typically, if you are doing programming or verification, you will primarily use `Vector α n`,
and if you are doing mathematics, you may want to use `List.Vector α n` instead.
-/
def List.Vector (α : Type u) (n : ℕ) :=
  { l : List α // l.length = n }

List-based vectors of fixed length

Informal description

For a type $\alpha$ and a natural number $n$, the type `List.Vector α n` consists of all lists of elements of $\alpha$ with length exactly $n$. This is distinct from the `Vector α n` type (which represents arrays of fixed length $n$), and is more suitable for mathematical contexts where list operations are preferred over array operations.

List.Vector.instDecidableEq instance

[DecidableEq α] : DecidableEq (Vector α n)

Full source

instance [DecidableEq α] : DecidableEq (Vector α n) :=
  inferInstanceAs (DecidableEq {l : List α // l.length = n})

Decidable Equality for List-Based Vectors

Informal description

For any type $\alpha$ with decidable equality and any natural number $n$, the equality of two vectors in `List.Vector α n` is decidable.

List.Vector.nil definition

: Vector α 0

Full source

/-- The empty vector with elements of type `α` -/
@[match_pattern]
def nil : Vector α 0 :=
  ⟨[], rfl⟩

Empty vector

Informal description

The empty vector of type $\alpha$ with length $0$, represented as the empty list.

List.Vector.cons definition

: α → Vector α n → Vector α (Nat.succ n)

Full source

/-- If `a : α` and `l : Vector α n`, then `cons a l`, is the vector of length `n + 1`
whose first element is a and with l as the rest of the list. -/
@[match_pattern]
def cons : α → Vector α n → Vector α (Nat.succ n)
  | a, ⟨v, h⟩ => ⟨a :: v, congrArg Nat.succ h⟩

Vector cons operation

Informal description

Given an element $a$ of type $\alpha$ and a vector $l$ of length $n$ over $\alpha$, the operation $\text{cons}(a, l)$ constructs a new vector of length $n+1$ where $a$ is the first element and $l$ forms the remaining elements. More formally, if $l$ is represented as a pair $(v, h)$ where $v$ is a list of length $n$ (with proof $h$), then $\text{cons}(a, l)$ returns the pair $(a :: v, h')$ where $h'$ is the proof that the new list has length $n+1$.

List.Vector.length definition

(_ : Vector α n) : ℕ

Full source

/-- The length of a vector. -/
@[reducible, nolint unusedArguments]
def length (_ : Vector α n) : ℕ :=
  n

Length of a list-based vector

Informal description

The function returns the length $ n $ of a vector in `List.Vector α n`, which is the fixed length parameter of the vector type.

List.Vector.head definition

: Vector α (Nat.succ n) → α

Full source

/-- The first element of a vector with length at least `1`. -/
def head : Vector α (Nat.succ n) → α
  | ⟨a :: _, _⟩ => a

Head of a non-empty vector

Informal description

For a vector $v$ of type $\text{Vector}\,\alpha\,(n+1)$ (i.e., a list of elements of type $\alpha$ with length $n+1$), the function $\text{head}$ returns the first element of $v$.

List.Vector.head_cons theorem

(a : α) : ∀ v : Vector α n, head (cons a v) = a

Full source

/-- The head of a vector obtained by prepending is the element prepended. -/
theorem head_cons (a : α) : ∀ v : Vector α n, head (cons a v) = a
  | ⟨_, _⟩ => rfl

Head of Prepended Vector Equals Prepended Element

Informal description

For any element $a$ of type $\alpha$ and any vector $v$ of length $n$ over $\alpha$, the head of the vector obtained by prepending $a$ to $v$ is equal to $a$, i.e., $\text{head}(\text{cons}(a, v)) = a$.

List.Vector.tail definition

: Vector α n → Vector α (n - 1)

Full source

/-- The tail of a vector, with an empty vector having empty tail. -/
def tail : Vector α n → Vector α (n - 1)
  | ⟨[], h⟩ => ⟨[], congrArg pred h⟩
  | ⟨_ :: v, h⟩ => ⟨v, congrArg pred h⟩

Tail of a vector

Informal description

For a vector of length $n$ (where $n$ is a natural number), the tail is the vector obtained by removing the first element, resulting in a vector of length $n-1$. If the input vector is empty, the tail is also empty.

List.Vector.tail_cons theorem

(a : α) : ∀ v : Vector α n, tail (cons a v) = v

Full source

/-- The tail of a vector obtained by prepending is the vector prepended. to -/
theorem tail_cons (a : α) : ∀ v : Vector α n, tail (cons a v) = v
  | ⟨_, _⟩ => rfl

Tail of Prepended Vector Equals Original Vector

Informal description

For any element $a$ of type $\alpha$ and any vector $v$ of length $n$ over $\alpha$, the tail of the vector obtained by prepending $a$ to $v$ is equal to $v$ itself. In other words, $\text{tail}(\text{cons}(a, v)) = v$.

List.Vector.cons_head_tail theorem

: ∀ v : Vector α (succ n), cons (head v) (tail v) = v

Full source

/-- Prepending the head of a vector to its tail gives the vector. -/
@[simp]
theorem cons_head_tail : ∀ v : Vector α (succ n), cons (head v) (tail v) = v
  | ⟨[], h⟩ => by contradiction
  | ⟨_ :: _, _⟩ => rfl

Reconstruction of Vector from Head and Tail

Informal description

For any non-empty vector $v$ of length $n+1$ over a type $\alpha$, prepending the head of $v$ to its tail reconstructs the original vector. That is, $\text{cons}(\text{head}(v), \text{tail}(v)) = v$.

List.Vector.toList definition

(v : Vector α n) : List α

Full source

/-- The list obtained from a vector. -/
def toList (v : Vector α n) : List α :=
  v.1

Underlying list of a vector

Informal description

The function maps a vector $ v $ of type `List.Vector α n` (a list of elements of type $ \alpha $ with fixed length $ n $) to its underlying list of elements.

List.Vector.get definition

(l : Vector α n) (i : Fin n) : α

Full source

/-- nth element of a vector, indexed by a `Fin` type. -/
def get (l : Vector α n) (i : Fin n) : α :=
  l.1.get <| i.cast l.2.symm

Element access in list-based vectors

Informal description

For a vector $v$ of type `List.Vector α n` (a list of elements of type $\alpha$ with fixed length $n$) and an index $i$ of type `Fin n` (the canonical type with $n$ elements), the function returns the $i$-th element of $v$.

List.Vector.append definition

{n m : Nat} : Vector α n → Vector α m → Vector α (n + m)

Full source

/-- Appending a vector to another. -/
def append {n m : Nat} : Vector α n → Vector α m → Vector α (n + m)
  | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, by simp [*]⟩

Concatenation of fixed-length vectors

Informal description

Given two vectors $ v_1 $ of length $ n $ and $ v_2 $ of length $ m $ with elements of type $ \alpha $, their concatenation $ v_1 \cdot v_2 $ is a vector of length $ n + m $ consisting of the elements of $ v_1 $ followed by the elements of $ v_2 $.

List.Vector.elim definition

{α} {C : ∀ {n}, Vector α n → Sort u} (H : ∀ l : List α, C ⟨l, rfl⟩) {n : ℕ} : ∀ v : Vector α n, C v

Full source

/-- Elimination rule for `Vector`. -/
@[elab_as_elim]
def elim {α} {C : ∀ {n}, Vector α n → Sort u}
    (H : ∀ l : List α, C ⟨l, rfl⟩) {n : ℕ} : ∀ v : Vector α n, C v
  | ⟨l, h⟩ =>
    match n, h with
    | _, rfl => H l

Eliminator for list-based vectors

Informal description

Given a type $\alpha$ and a dependent type $C$ indexed by vectors of $\alpha$ of any length $n$, the eliminator `List.Vector.elim` takes a function $H$ that operates on arbitrary lists of $\alpha$ (without length constraints) and produces a function that operates on vectors of $\alpha$ of any fixed length $n$. Specifically, for any vector $v$ of length $n$, the eliminator applies $H$ to the underlying list of $v$.

List.Vector.map definition

(f : α → β) : Vector α n → Vector β n

Full source

/-- Map a vector under a function. -/
def map (f : α → β) : Vector α n → Vector β n
  | ⟨l, h⟩ => ⟨List.map f l, by simp [*]⟩

Mapping a function over a vector

Informal description

Given a function $f : \alpha \to \beta$ and a vector $\mathbf{v} \in \text{Vector} \alpha n$ (a list of length $n$ with elements in $\alpha$), the function returns a new vector $\mathbf{w} \in \text{Vector} \beta n$ where each element $w_i = f(v_i)$ for $i = 1, \dots, n$.

List.Vector.map_nil theorem

(f : α → β) : map f nil = nil

Full source

/-- A `nil` vector maps to a `nil` vector. -/
@[simp]
theorem map_nil (f : α → β) : map f nil = nil :=
  rfl

Mapping over the empty vector yields the empty vector

Informal description

For any function $f : \alpha \to \beta$, applying the map operation to the empty vector $\text{nil}$ yields the empty vector $\text{nil}$ in $\text{Vector} \beta 0$, i.e., $\text{map} f \text{nil} = \text{nil}$.

List.Vector.map_cons theorem

(f : α → β) (a : α) : ∀ v : Vector α n, map f (cons a v) = cons (f a) (map f v)

Full source

/-- `map` is natural with respect to `cons`. -/
@[simp]
theorem map_cons (f : α → β) (a : α) : ∀ v : Vector α n, map f (cons a v) = cons (f a) (map f v)
  | ⟨_, _⟩ => rfl

Naturality of Vector Map under Cons: $\text{map}\, f (\text{cons}\, a\, v) = \text{cons}\, (f a)\, (\text{map}\, f\, v)$

Informal description

For any function $f : \alpha \to \beta$, element $a \in \alpha$, and vector $v \in \text{Vector} \alpha n$, the map operation satisfies the naturality property: \[ \text{map}\, f (\text{cons}\, a\, v) = \text{cons}\, (f a)\, (\text{map}\, f\, v). \]

List.Vector.pmap definition

(f : (a : α) → p a → β) : (v : Vector α n) → (∀ x ∈ v.toList, p x) → Vector β n

Full source

/-- Map a vector under a partial function. -/
def pmap (f : (a : α) → p a → β) :
    (v : Vector α n) → (∀ x ∈ v.toList, p x) → Vector β n
  | ⟨l, h⟩, hp => ⟨List.pmap f l hp, by simp [h]⟩

Partial mapping of a vector with a predicate

Informal description

Given a predicate $p$ on elements of type $\alpha$, a function $f$ that maps elements of $\alpha$ satisfying $p$ to elements of type $\beta$, and a vector $v : \text{Vector } \alpha n$ where all elements satisfy $p$, the function $\text{pmap}$ applies $f$ to each element of $v$ to produce a new vector of type $\text{Vector } \beta n$.

List.Vector.pmap_nil theorem

(f : (a : α) → p a → β) (hp : ∀ x ∈ nil.toList, p x) : nil.pmap f hp = nil

Full source

@[simp]
theorem pmap_nil (f : (a : α) → p a → β) (hp : ∀ x ∈ nil.toList, p x) :
    nil.pmap f hp = nil := rfl

Partial Map Preserves Empty Vector: $\text{pmap}\, f\, \text{nil}\, \text{hp} = \text{nil}$

Informal description

For any function $f \colon \alpha \to \beta$ and predicate $p$ on $\alpha$, if all elements of the empty vector satisfy $p$, then applying the partial map $f$ to the empty vector (with proof that all elements satisfy $p$) yields the empty vector. That is, $\text{pmap}\, f\, \text{nil}\, \text{hp} = \text{nil}$.

List.Vector.map₂ definition

(f : α → β → φ) : Vector α n → Vector β n → Vector φ n

Full source

/-- Mapping two vectors under a curried function of two variables. -/
def map₂ (f : α → β → φ) : Vector α n → Vector β n → Vector φ n
  | ⟨x, _⟩, ⟨y, _⟩ => ⟨List.zipWith f x y, by simp [*]⟩

Pairwise mapping of vectors

Informal description

Given a function $f : \alpha \to \beta \to \phi$ and two vectors $\mathbf{x} : \text{Vector } \alpha n$ and $\mathbf{y} : \text{Vector } \beta n$, the function $\text{map}_2$ applies $f$ pairwise to the elements of $\mathbf{x}$ and $\mathbf{y}$ to produce a new vector $\mathbf{z} : \text{Vector } \phi n$ where each element $z_i = f(x_i, y_i)$.

List.Vector.replicate definition

(n : ℕ) (a : α) : Vector α n

Full source

/-- Vector obtained by repeating an element. -/
def replicate (n : ℕ) (a : α) : Vector α n :=
  ⟨List.replicate n a, List.length_replicate⟩

Vector with repeated elements

Informal description

For a natural number $n$ and an element $a$ of type $\alpha$, the function `List.Vector.replicate n a` returns a vector (list of fixed length) of length $n$ where every element is $a$.

List.Vector.drop definition

(i : ℕ) : Vector α n → Vector α (n - i)

Full source

/-- Drop `i` elements from a vector of length `n`; we can have `i > n`. -/
def drop (i : ℕ) : Vector α n → Vector α (n - i)
  | ⟨l, p⟩ => ⟨List.drop i l, by simp [*]⟩

Drop elements from a fixed-length vector

Informal description

Given a natural number $i$ and a vector of length $n$ (represented as a list with length $n$), the function returns a new vector obtained by dropping the first $i$ elements from the original vector. The resulting vector has length $n - i$, even if $i > n$ (in which case the result is an empty vector).

List.Vector.take definition

(i : ℕ) : Vector α n → Vector α (min i n)

Full source

/-- Take `i` elements from a vector of length `n`; we can have `i > n`. -/
def take (i : ℕ) : Vector α n → Vector α (min i n)
  | ⟨l, p⟩ => ⟨List.take i l, by simp [*]⟩

Prefix of a vector up to length $ i $

Informal description

Given a natural number $ i $ and a vector $ v $ of length $ n $ (i.e., $ v \in \text{Vector} \alpha n $), the function returns a new vector consisting of the first $ \min(i, n) $ elements of $ v $.

List.Vector.eraseIdx definition

(i : Fin n) : Vector α n → Vector α (n - 1)

Full source

/-- Remove the element at position `i` from a vector of length `n`. -/
def eraseIdx (i : Fin n) : Vector α n → Vector α (n - 1)
  | ⟨l, p⟩ => ⟨List.eraseIdx l i.1, by rw [l.length_eraseIdx_of_lt] <;> rw [p]; exact i.2⟩

Vector element removal at index

Informal description

Given a vector $v$ of length $n$ and an index $i$ (where $i < n$), the operation removes the element at position $i$ from $v$, resulting in a new vector of length $n - 1$.

List.Vector.ofFn definition

: ∀ {n}, (Fin n → α) → Vector α n

Full source

/-- Vector of length `n` from a function on `Fin n`. -/
def ofFn : ∀ {n}, (Fin n → α) → Vector α n
  | 0, _ => nil
  | _ + 1, f => cons (f 0) (ofFn fun i ↦ f i.succ)

Vector from a function on finite indices

Informal description

For any natural number $n$ and any function $f \colon \mathrm{Fin}\,n \to \alpha$, the operation constructs a vector of length $n$ over $\alpha$ whose $i$-th element is $f(i)$. More precisely: - When $n = 0$, it returns the empty vector. - For $n = k + 1$, it constructs the vector by prepending $f(0)$ to the vector obtained from the function $i \mapsto f(i+1)$ on $\mathrm{Fin}\,k$.

List.Vector.congr definition

{n m : ℕ} (h : n = m) : Vector α n → Vector α m

Full source

/-- Create a vector from another with a provably equal length. -/
protected def congr {n m : ℕ} (h : n = m) : Vector α n → Vector α m
  | ⟨x, p⟩ => ⟨x, h ▸ p⟩

Vector length conversion via equality

Informal description

Given a natural number equality $n = m$, the function converts a vector of length $n$ to a vector of length $m$ by transporting the length proof along the equality.

List.Vector.mapAccumr definition

(f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n

Full source

/-- Runs a function over a vector returning the intermediate results and a
final result.
-/
def mapAccumr (f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n
  | ⟨x, px⟩, c =>
    let res := List.mapAccumr f x c
    ⟨res.1, res.2, by simp [*, res]⟩

Right-to-left map with accumulation over fixed-length lists

Informal description

Given a function $f : \alpha \to \sigma \to \sigma \times \beta$, a vector $v$ of type `Vector α n`, and an initial state $c$ of type $\sigma$, the function `List.Vector.mapAccumr` applies $f$ to each element of $v$ from right to left, accumulating the intermediate states in $\sigma$ and producing a final state and a new vector of type `Vector β n`. More precisely, for each element $x_i$ in $v$ (processed from right to left), $f$ is applied to $x_i$ and the current state, producing a new state and a result $y_i$. The final result is a pair consisting of the last state and the vector of all $y_i$ values.

List.Vector.mapAccumr₂ definition

(f : α → β → σ → σ × φ) : Vector α n → Vector β n → σ → σ × Vector φ n

Full source

/-- Runs a function over a pair of vectors returning the intermediate results and a
final result.
-/
def mapAccumr₂ (f : α → β → σ → σ × φ) : Vector α n → Vector β n → σ → σ × Vector φ n
  | ⟨x, px⟩, ⟨y, py⟩, c =>
    let res := List.mapAccumr₂ f x y c
    ⟨res.1, res.2, by simp [*, res]⟩

Right-to-left pairwise accumulation over two vectors

Informal description

Given a function $f : \alpha \to \beta \to \sigma \to \sigma \times \phi$, two vectors $\mathbf{v} : \text{Vector } \alpha n$ and $\mathbf{w} : \text{Vector } \beta n$, and an initial state $c : \sigma$, the function `List.Vector.mapAccumr₂` applies $f$ pairwise to the elements of $\mathbf{v}$ and $\mathbf{w}$ from right to left, accumulating the state $\sigma$ and producing a new vector of type $\text{Vector } \phi n$ along with the final state. More precisely, it returns a pair $(\sigma', \mathbf{u})$, where $\sigma'$ is the final state after processing all elements, and $\mathbf{u}$ is the vector of results obtained from applying $f$ to each corresponding pair of elements in $\mathbf{v}$ and $\mathbf{w}$.

List.Vector.shiftLeftFill definition

(v : Vector α n) (i : ℕ) (fill : α) : Vector α n

Full source

/-- `shiftLeftFill v i` is the vector obtained by left-shifting `v` `i` times and padding with the
    `fill` argument. If `v.length < i` then this will return `replicate n fill`. -/
def shiftLeftFill (v : Vector α n) (i : ℕ) (fill : α) : Vector α n :=
  Vector.congr (by simp) <|
    append (drop i v) (replicate (min n i) fill)

Left-shift with fill for fixed-length vectors

Informal description

Given a vector $ v $ of length $ n $, a natural number $ i $, and a fill element $ \text{fill} $, the function `shiftLeftFill v i fill` returns a new vector obtained by left-shifting $ v $ $ i $ times and padding the right end with $ \text{fill} $. If $ i $ is greater than or equal to $ n $, the result is a vector of length $ n $ filled entirely with $ \text{fill} $. More precisely, the result is constructed by dropping the first $ i $ elements of $ v $ and appending $ \min(n, i) $ copies of $ \text{fill} $ to the end, ensuring the output has length $ n $.

List.Vector.shiftRightFill definition

(v : Vector α n) (i : ℕ) (fill : α) : Vector α n

Full source

/-- `shiftRightFill v i` is the vector obtained by right-shifting `v` `i` times and padding with the
    `fill` argument. If `v.length < i` then this will return `replicate n fill`. -/
def shiftRightFill (v : Vector α n) (i : ℕ) (fill : α) : Vector α n :=
  Vector.congr (by omega) <| append (replicate (min n i) fill) (take (n - i) v)

Right-shift with fill for fixed-length vectors

Informal description

Given a vector $ v $ of length $ n $, a natural number $ i $, and a fill element $ \text{fill} $, the function `shiftRightFill v i fill` returns a new vector obtained by right-shifting $ v $ $ i $ times and padding the left end with $ \text{fill} $. If $ i $ is greater than or equal to $ n $, the result is a vector of length $ n $ filled entirely with $ \text{fill} $. More precisely, the result is constructed by taking the last $ n - i $ elements of $ v $ (if $ i < n $) and prepending $ \min(n, i) $ copies of $ \text{fill} $ to the beginning, ensuring the output has length $ n $.

List.Vector.eq theorem

{n : ℕ} : ∀ a1 a2 : Vector α n, toList a1 = toList a2 → a1 = a2

Full source

/-- Vector is determined by the underlying list. -/
protected theorem eq {n : ℕ} : ∀ a1 a2 : Vector α n, toList a1 = toList a2 → a1 = a2
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Equality of Vectors via Underlying Lists

Informal description

For any natural number $n$ and any two vectors $a_1, a_2$ of type `List.Vector α n`, if their underlying lists are equal (i.e., $\text{toList}(a_1) = \text{toList}(a_2)$), then $a_1 = a_2$.

List.Vector.toList_mk theorem

(v : List α) (P : List.length v = n) : toList (Subtype.mk v P) = v

Full source

/-- Vector of length from a list `v`
with witness that `v` has length `n` maps to `v` under `toList`. -/
@[simp]
theorem toList_mk (v : List α) (P : List.length v = n) : toList (Subtype.mk v P) = v :=
  rfl

Vector Construction Preserves Underlying List

Informal description

For any list $v$ of type $\alpha$ with a proof $P$ that its length is $n$, the underlying list of the vector constructed from $v$ and $P$ is equal to $v$ itself, i.e., $\text{toList}(\text{Subtype.mk}\ v\ P) = v$.

List.Vector.toList_nil theorem

: toList nil = @List.nil α

Full source

/-- A nil vector maps to a nil list. -/
@[simp]
theorem toList_nil : toList nil = @List.nil α :=
  rfl

Empty Vector Maps to Empty List

Informal description

The underlying list of the empty vector is the empty list, i.e., $\text{toList}(\text{nil}) = \text{nil}$.

List.Vector.toList_length theorem

(v : Vector α n) : (toList v).length = n

Full source

/-- The length of the list to which a vector of length `n` maps is `n`. -/
@[simp]
theorem toList_length (v : Vector α n) : (toList v).length = n :=
  v.2

Length Preservation of Vector-to-List Conversion: $|\text{toList}(v)| = n$

Informal description

For any vector $v$ of length $n$ over a type $\alpha$, the length of its underlying list $\text{toList}(v)$ is equal to $n$.

List.Vector.toList_cons theorem

(a : α) (v : Vector α n) : toList (cons a v) = a :: toList v

Full source

/-- `toList` of `cons` of a vector and an element is
the `cons` of the list obtained by `toList` and the element -/
@[simp]
theorem toList_cons (a : α) (v : Vector α n) : toList (cons a v) = a :: toList v := by
  cases v; rfl

List conversion of vector cons operation: $\text{toList}(\text{cons}(a, v)) = a :: \text{toList}(v)$

Informal description

For any element $a$ of type $\alpha$ and any vector $v$ of length $n$ over $\alpha$, the underlying list of the vector obtained by prepending $a$ to $v$ is equal to the list obtained by prepending $a$ to the underlying list of $v$. In symbols: $\text{toList}(\text{cons}(a, v)) = a :: \text{toList}(v)$.

List.Vector.toList_append theorem

{n m : ℕ} (v : Vector α n) (w : Vector α m) : toList (append v w) = toList v ++ toList w

Full source

/-- Appending of vectors corresponds under `toList` to appending of lists. -/
@[simp]
theorem toList_append {n m : ℕ} (v : Vector α n) (w : Vector α m) :
    toList (append v w) = toList v ++ toList w := by
  cases v
  cases w
  rfl

List conversion preserves vector concatenation: $\text{toList}(v \cdot w) = \text{toList}(v) +\!\!+ \text{toList}(w)$

Informal description

For any vectors $v$ of length $n$ and $w$ of length $m$ with elements of type $\alpha$, the underlying list of their concatenation $\text{append}(v, w)$ is equal to the concatenation of their underlying lists $\text{toList}(v) +\!\!+ \text{toList}(w)$.

List.Vector.toList_drop theorem

{n m : ℕ} (v : Vector α m) : toList (drop n v) = List.drop n (toList v)

Full source

/-- `drop` of vectors corresponds under `toList` to `drop` of lists. -/
@[simp]
theorem toList_drop {n m : ℕ} (v : Vector α m) : toList (drop n v) = List.drop n (toList v) := by
  cases v
  rfl

List Conversion Preserves Vector Drop Operation: $\text{toList}(\text{drop}(n, v)) = \text{drop}(n, \text{toList}(v))$

Informal description

For any natural numbers $n$ and $m$, and any vector $v$ of length $m$ with elements of type $\alpha$, the underlying list of the vector obtained by dropping the first $n$ elements of $v$ is equal to the list obtained by dropping the first $n$ elements of the underlying list of $v$. In symbols: $\text{toList}(\text{drop}(n, v)) = \text{drop}(n, \text{toList}(v))$.

List.Vector.toList_take theorem

{n m : ℕ} (v : Vector α m) : toList (take n v) = List.take n (toList v)

Full source

/-- `take` of vectors corresponds under `toList` to `take` of lists. -/
@[simp]
theorem toList_take {n m : ℕ} (v : Vector α m) : toList (take n v) = List.take n (toList v) := by
  cases v
  rfl

List Conversion Preserves Vector Prefix: $\text{toList}(\text{take}(n, v)) = \text{take}(n, \text{toList}(v))$

Informal description

For any natural numbers $n$ and $m$, and any vector $v$ of length $m$ with elements of type $\alpha$, the underlying list of the prefix vector $\text{take}(n, v)$ is equal to the prefix list $\text{take}(n, \text{toList}(v))$.

List.Vector.instGetElemNatLt instance

: GetElem (Vector α n) Nat α fun _ i => i < n

Full source

instance : GetElem (Vector α n) Nat α fun _ i => i < n where
  getElem := fun x i h => get x ⟨i, h⟩

Element Access for List-Based Vectors

Informal description

For any type $\alpha$ and natural number $n$, the type `List.Vector α n` (lists of length $n$) supports element access via the notation `v[i]` where $i$ is a natural number less than $n$.

List.Vector.getElem_def theorem

(v : Vector α n) (i : ℕ) {hi : i < n} : v[i] = v.toList[i]'(by simpa)

Full source

lemma getElem_def (v : Vector α n) (i : ℕ) {hi : i < n} :
    v[i] = v.toList[i]'(by simpa) := rfl

Vector Element Access Equals List Element Access: $v[i] = \text{toList}(v)[i]$

Informal description

For any vector $v$ of type `List.Vector α n` and any natural number $i$ such that $i < n$, the $i$-th element of $v$ (accessed via the notation $v[i]$) is equal to the $i$-th element of the underlying list $\text{toList}(v)$.

List.Vector.toList_getElem theorem

(v : Vector α n) (i : ℕ) {hi : i < v.toList.length} : v.toList[i] = v[i]'(by simp_all)

Full source

lemma toList_getElem (v : Vector α n) (i : ℕ) {hi : i < v.toList.length} :
    v.toList[i] = v[i]'(by simp_all) := rfl

Equality of List and Vector Element Access: $\text{toList}(v)[i] = v[i]$

Informal description

For any vector $v$ of type `List.Vector α n` and any natural number $i$ such that $i < \text{length}(\text{toList}(v))$, the $i$-th element of the underlying list $\text{toList}(v)$ is equal to the $i$-th element of $v$ (accessed via the `GetElem` notation).