The type Vector represents lists with fixed length.

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

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

Equations

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

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

Equations

• Mathlib.Vector.instDecidableEq = inferInstanceAs (DecidableEq { l : List α // l.length = n })

@[match_pattern]

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

The empty vector with elements of type α

Equations

• Mathlib.Vector.nil = ⟨[], ⋯⟩

@[match_pattern]

def Mathlib.Vector.cons {α : Type u} {n : ℕ} : α → Mathlib.Vector α n → Mathlib.Vector α n.succ

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

• Mathlib.Vector.cons x✝ x = match x✝, x with | a, ⟨v, h⟩ => ⟨a :: v, ⋯⟩

@[reducible]

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

The length of a vector.

Equations

• x.length = n

def Mathlib.Vector.head {α : Type u} {n : ℕ} : Mathlib.Vector α n.succ → α

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

Equations

• x.head = match x with | ⟨a :: tail, property⟩ => a

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

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

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

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

Equations

• x.tail = match x with | ⟨[], h⟩ => ⟨[], ⋯⟩ | ⟨head :: v, h⟩ => ⟨v, ⋯⟩

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

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

@[simp]

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

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

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

The list obtained from a vector.

Equations

• v.toList = ↑v

def Mathlib.Vector.get {α : Type u} {n : ℕ} (l : Mathlib.Vector α n) (i : Fin n) : α

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

Equations

• l.get i = (↑l).get (Fin.cast ⋯ i)

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

Appending a vector to another.

Equations

• x✝.append x = match x✝, x with | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, ⋯⟩

def Mathlib.Vector.elim {α : Type u_1} {C : {n : ℕ} → Mathlib.Vector α n → Sort u} (H : (l : List α) → C ⟨l, ⋯⟩) {n : ℕ} (v : Mathlib.Vector α n) : C v

Elimination rule for Vector.

Equations

• Mathlib.Vector.elim H x = match x with | ⟨l, h⟩ => match n, h with | .(l.length), ⋯ => H l

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

Map a vector under a function.

Equations

• Mathlib.Vector.map f x = match x with | ⟨l, h⟩ => ⟨List.map f l, ⋯⟩

@[simp]

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

A nil vector maps to a nil vector.

@[simp]

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

map is natural with respect to cons.

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

Mapping two vectors under a curried function of two variables.

Equations

• Mathlib.Vector.map₂ f x✝ x = match x✝, x with | ⟨x, property⟩, ⟨y, property_1⟩ => ⟨List.zipWith f x y, ⋯⟩

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

Vector obtained by repeating an element.

Equations

• Mathlib.Vector.replicate n a = ⟨List.replicate n a, ⋯⟩

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

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

Equations

• Mathlib.Vector.drop i x = match x with | ⟨l, p⟩ => ⟨List.drop i l, ⋯⟩

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

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

Equations

• Mathlib.Vector.take i x = match x with | ⟨l, p⟩ => ⟨List.take i l, ⋯⟩

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

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

Equations

• Mathlib.Vector.eraseIdx i x = match x with | ⟨l, p⟩ => ⟨l.eraseIdx ↑i, ⋯⟩

@[deprecated Mathlib.Vector.eraseIdx]

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

Alias of Mathlib.Vector.eraseIdx.

---

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

Equations

• @Mathlib.Vector.removeNth = @Mathlib.Vector.eraseIdx

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

Vector of length n from a function on Fin n.

Equations

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

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

Create a vector from another with a provably equal length.

Equations

• Mathlib.Vector.congr h x = match x with | ⟨x, p⟩ => ⟨x, ⋯⟩

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

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

Equations

• Mathlib.Vector.mapAccumr f x✝ x = match x✝, x with | ⟨x, px⟩, c => let res := List.mapAccumr f x c; (res.fst, ⟨res.snd, ⋯⟩)

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

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

Equations

• Mathlib.Vector.mapAccumr₂ f x✝¹ x✝ x = match x✝¹, x✝, x with | ⟨x, px⟩, ⟨y, py⟩, c => let res := List.mapAccumr₂ f x y c; (res.fst, ⟨res.snd, ⋯⟩)

Shift Primitives

def Mathlib.Vector.shiftLeftFill {α : Type u} {n : ℕ} (v : Mathlib.Vector α n) (i : ℕ) (fill : α) : Mathlib.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

• v.shiftLeftFill i fill = Mathlib.Vector.congr ⋯ ((Mathlib.Vector.drop i v).append (Mathlib.Vector.replicate (min n i) fill))

def Mathlib.Vector.shiftRightFill {α : Type u} {n : ℕ} (v : Mathlib.Vector α n) (i : ℕ) (fill : α) : Mathlib.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

• v.shiftRightFill i fill = Mathlib.Vector.congr ⋯ ((Mathlib.Vector.replicate (min n i) fill).append (Mathlib.Vector.take (n - i) v))

Basic Theorems

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

Vector is determined by the underlying list.

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

A vector of length 0 is a nil vector.

@[simp]

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

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

@[simp]

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

A nil vector maps to a nil list.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Appending of vectors corresponds under toList to appending of lists.

@[simp]

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

drop of vectors corresponds under toList to drop of lists.

@[simp]

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

take of vectors corresponds under toList to take of lists.

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

Equations

• Mathlib.Vector.instGetElemNatLt = { getElem := fun (x : Mathlib.Vector α n) (i : ℕ) (h : i < n) => x.get ⟨i, h⟩ }