The type Vector represents lists with fixed length.

def Vector (α : Type u) (n : ℕ) : Type u

Vector α n is the type of lists of length n with elements of type α.

Equations

• Vector α n = { l // List.length l = n }

instance Vector.instDecidableEqVector {α : Type u} {n : ℕ} [DecidableEq α] : DecidableEq (Vector α n)

Equations

• Vector.instDecidableEqVector = inferInstanceAs (DecidableEq { l // List.length l = n })

@[match_pattern]

def Vector.nil {α : Type u} : Vector α 0

The empty vector with elements of type α

Equations

• Vector.nil = { val := [], property := (_ : List.length [] = List.length []) }

@[match_pattern]

def Vector.cons {α : Type u} {n : ℕ} : α → Vector α n → Vector α (Nat.succ n)

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.

Equations

• Vector.cons x x = match x, x with | a, { val := v, property := h } => { val := a :: v, property := (_ : Nat.succ (List.length v) = Nat.succ n) }

@[reducible]

def Vector.length {α : Type u} {n : ℕ} : Vector α n → ℕ

The length of a vector.

Equations

• Vector.length x = n

def Vector.head {α : Type u} {n : ℕ} : Vector α (Nat.succ n) → α

The first element of a vector with length at least 1.

Equations

• Vector.head x = match x with | { val := [], property := h } => Nat.noConfusion h | { val := a :: tail, property := property } => a

theorem Vector.head_cons {α : Type u} {n : ℕ} (a : α) (v : Vector α n) : Vector.head (Vector.cons a v) = a

The head of a vector obtained by prepending is the element prepended.

def Vector.tail {α : Type u} {n : ℕ} : Vector α n → Vector α (n - 1)

The tail of a vector, with an empty vector having empty tail.

Equations

• One or more equations did not get rendered due to their size.

theorem Vector.tail_cons {α : Type u} {n : ℕ} (a : α) (v : Vector α n) : Vector.tail (Vector.cons a v) = v

The tail of a vector obtained by prepending is the vector prepended. to

@[simp]

theorem Vector.cons_head_tail {α : Type u} {n : ℕ} (v : Vector α (Nat.succ n)) : Vector.cons (Vector.head v) (Vector.tail v) = v

Prepending the head of a vector to its tail gives the vector.

def Vector.toList {α : Type u} {n : ℕ} (v : Vector α n) : List α

The list obtained from a vector.

Equations

• Vector.toList v = ↑v

def Vector.get {α : Type u} {n : ℕ} : Vector α n → Fin n → α

nth element of a vector, indexed by a Fin type.

Equations

• Vector.get x x = match x, x with | { val := l, property := h }, i => List.nthLe l ↑i (_ : ↑i < List.length l)

def Vector.append {α : Type u} {n : ℕ} {m : ℕ} : Vector α n → Vector α m → Vector α (n + m)

Appending a vector to another.

Equations

• Vector.append x x = match x, x with | { val := l₁, property := h₁ }, { val := l₂, property := h₂ } => { val := l₁ ++ l₂, property := (_ : List.length (l₁ ++ l₂) = n + m) }

def Vector.elim {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u} (H : (l : List α) → C (List.length l) { val := l, property := (_ : List.length l = List.length l) }) {n : ℕ} (v : Vector α n) : C n v

Elimination rule for Vector.

Equations

• Vector.elim H x = match x with | { val := l, property := h } => match n, h with | .(List.length l), (_ : List.length l = List.length l) => H l

def Vector.map {α : Type u} {β : Type v} {n : ℕ} (f : α → β) : Vector α n → Vector β n

Map a vector under a function.

Equations

• Vector.map f x = match x with | { val := l, property := h } => { val := List.map f l, property := (_ : List.length (List.map f l) = n) }

@[simp]

theorem Vector.map_nil {α : Type u} {β : Type v} (f : α → β) : Vector.map f Vector.nil = Vector.nil

A nil vector maps to a nil vector.

@[simp]

theorem Vector.map_cons {α : Type u} {β : Type v} {n : ℕ} (f : α → β) (a : α) (v : Vector α n) : Vector.map f (Vector.cons a v) = Vector.cons (f a) (Vector.map f v)

map is natural with respect to cons.

def Vector.map₂ {α : Type u} {β : Type v} {φ : Type w} {n : ℕ} (f : α → β → φ) : Vector α n → Vector β n → Vector φ n

Mapping two vectors under a curried function of two variables.

Equations

• One or more equations did not get rendered due to their size.

def Vector.replicate {α : Type u} (n : ℕ) (a : α) : Vector α n

Vector obtained by repeating an element.

Equations

• Vector.replicate n a = { val := List.replicate n a, property := (_ : List.length (List.replicate n a) = n) }

def Vector.drop {α : Type u} {n : ℕ} (i : ℕ) : Vector α n → Vector α (n - i)

Drop i elements from a vector of length n; we can have i > n.

Equations

• Vector.drop i x = match x with | { val := l, property := p } => { val := List.drop i l, property := (_ : List.length (List.drop i l) = n - i) }

def Vector.take {α : Type u} {n : ℕ} (i : ℕ) : Vector α n → Vector α (min i n)

Take i elements from a vector of length n; we can have i > n.

Equations

• Vector.take i x = match x with | { val := l, property := p } => { val := List.take i l, property := (_ : List.length (List.take i l) = min i n) }

def Vector.removeNth {α : Type u} {n : ℕ} (i : Fin n) : Vector α n → Vector α (n - 1)

Remove the element at position i from a vector of length n.

Equations

• Vector.removeNth i x = match x with | { val := l, property := p } => { val := List.removeNth l ↑i, property := (_ : List.length (List.removeNth l ↑i) = n - 1) }

def Vector.ofFn {α : Type u} {n : ℕ} : (Fin n → α) → Vector α n

Vector of length n from a function on Fin n.

Equations

• Vector.ofFn x_2 = Vector.nil
• Vector.ofFn f = Vector.cons (f 0) (Vector.ofFn fun i => f (Fin.succ i))

def Vector.congr {α : Type u} {n : ℕ} {m : ℕ} (h : n = m) : Vector α n → Vector α m

Create a vector from another with a provably equal length.

Equations

• Vector.congr h x = match x with | { val := x, property := p } => { val := x, property := (_ : List.length x = m) }

def Vector.mapAccumr {α : Type u} {β : Type v} {n : ℕ} {σ : Type} (f : α → σ → σ × β) : Vector α n → σ → σ × Vector β n

Runs a function over a vector returning the intermediate results and a final result.

Equations

• One or more equations did not get rendered due to their size.

def Vector.mapAccumr₂ {n : ℕ} {α : Type} {β : Type} {σ : Type} {φ : Type} (f : α → β → σ → σ × φ) : Vector α n → Vector β n → σ → σ × Vector φ n

Runs a function over a pair of vectors returning the intermediate results and a final result.

Equations

• One or more equations did not get rendered due to their size.

Shift Primitives

def Vector.shiftLeftFill {α : Type u} {n : ℕ} (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

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.

Equations

• Vector.shiftLeftFill v i fill = Vector.congr (_ : n - i + min n i = n) (Vector.append (Vector.drop i v) (Vector.replicate (min n i) fill))

def Vector.shiftRightFill {α : Type u} {n : ℕ} (v : Vector α n) (i : ℕ) (fill : α) : Vector α n

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.

Equations

• Vector.shiftRightFill v i fill = Vector.congr (_ : min n i + min (n - i) n = n) (Vector.append (Vector.replicate (min n i) fill) (Vector.take (n - i) v))

Basic Theorems

theorem Vector.eq {α : Type u} {n : ℕ} (a1 : Vector α n) (a2 : Vector α n) : Vector.toList a1 = Vector.toList a2 → a1 = a2

Vector is determined by the underlying list.

theorem Vector.eq_nil {α : Type u} (v : Vector α 0) : v = Vector.nil

A vector of length 0 is a nil vector.

@[simp]

theorem Vector.toList_mk {α : Type u} {n : ℕ} (v : List α) (P : List.length v = n) : Vector.toList { val := v, property := P } = v

Vector of length from a list v with witness that v has length n maps to v under toList.

@[simp]

theorem Vector.toList_nil {α : Type u} : Vector.toList Vector.nil = []

A nil vector maps to a nil list.

@[simp]

theorem Vector.toList_length {α : Type u} {n : ℕ} (v : Vector α n) : List.length (Vector.toList v) = n

The length of the list to which a vector of length n maps is n.

@[simp]

theorem Vector.toList_cons {α : Type u} {n : ℕ} (a : α) (v : Vector α n) : Vector.toList (Vector.cons a v) = a :: Vector.toList v

toList of cons of a vector and an element is the cons of the list obtained by toList and the element

@[simp]

theorem Vector.toList_append {α : Type u} {n : ℕ} {m : ℕ} (v : Vector α n) (w : Vector α m) : Vector.toList (Vector.append v w) = Vector.toList v ++ Vector.toList w

Appending of vectors corresponds under toList to appending of lists.

@[simp]

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

drop of vectors corresponds under toList to drop of lists.

@[simp]

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

take of vectors corresponds under toList to take of lists.

instance Vector.instGetElemVectorNatLtInstLTNat {α : Type u} {n : ℕ} : GetElem (Vector α n) ℕ α fun x i => i < n

Equations

• Vector.instGetElemVectorNatLtInstLTNat = { getElem := fun x i h => Vector.get x { val := i, isLt := h } }