Vectors

Vector α n is an array with a statically fixed size n. It combines the benefits of Lean's special support for Arrays that offer O(1) accesses and in-place mutations for arrays with no more than one reference, with static guarantees about the size of the underlying array.

structure Batteries.Vector (α : Type u) (n : Nat) : Type u

Vector α n is an Array α whose size is statically fixed to n

• toArray : Array α

  Internally, a vector is stored as an array for fast access

• size_eq : self.toArray.size = n

  size_eq fixes the size of toArray statically

theorem Batteries.Vector.size_eq {α : Type u} {n : Nat} (self : Batteries.Vector α n) : self.toArray.size = n

size_eq fixes the size of toArray statically

instance Batteries.instReprVector : {α : Type u_1} → {n : Nat} → [inst : Repr α] → Repr (Batteries.Vector α n)

Equations

• Batteries.instReprVector = { reprPrec := Batteries.reprVector✝ }

instance Batteries.instDecidableEqVector : {α : Type u_1} → {n : Nat} → [inst : DecidableEq α] → DecidableEq (Batteries.Vector α n)

Equations

• Batteries.instDecidableEqVector = Batteries.decEqVector✝

def Batteries.Vector.«term#v[_,]» : Lean.ParserDescr

Syntax for Vector α n

Equations

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

def Batteries.Vector.elimAsArray {α : Type u_1} {motive : {n : Nat} → Batteries.Vector α n → Sort u} (mk : (a : Array α) → motive { toArray := a, size_eq := ⋯ }) {n : Nat} (v : Batteries.Vector α n) : motive v

Custom eliminator for Vector α n through Array α

Equations

• Batteries.Vector.elimAsArray mk { toArray := a, size_eq := ⋯ } = mk a

def Batteries.Vector.elimAsList {α : Type u_1} {motive : {n : Nat} → Batteries.Vector α n → Sort u} (mk : (a : List α) → motive { toArray := { data := a }, size_eq := ⋯ }) {n : Nat} (v : Batteries.Vector α n) : motive v

Custom eliminator for Vector α n through List α

Equations

• Batteries.Vector.elimAsList mk { toArray := { data := a }, size_eq := ⋯ } = mk a

def Batteries.Vector.size {α : Type u_1} {n : Nat} : Batteries.Vector α n → Nat

Vector.size gives the size of a vector.

Equations

• x.size = n

def Batteries.Vector.empty {α : Type u_1} : Batteries.Vector α 0

Vector.empty produces an empty vector

Equations

• Batteries.Vector.empty = { toArray := #[], size_eq := ⋯ }

def Batteries.Vector.mkEmpty {α : Type u_1} (capacity : Nat) : Batteries.Vector α 0

Make an empty vector with pre-allocated capacity

Equations

• Batteries.Vector.mkEmpty capacity = { toArray := Array.mkEmpty capacity, size_eq := ⋯ }

def Batteries.Vector.mkVector {α : Type u_1} (n : Nat) (v : α) : Batteries.Vector α n

Makes a vector of size n with all cells containing v

Equations

• Batteries.Vector.mkVector n v = { toArray := mkArray n v, size_eq := ⋯ }

def Batteries.Vector.singleton {α : Type u_1} (v : α) : Batteries.Vector α 1

Returns a vector of size 1 with a single element v

Equations

• Batteries.Vector.singleton v = Batteries.Vector.mkVector 1 v

instance Batteries.Vector.instInhabited {α : Type u_1} {n : Nat} [Inhabited α] : Inhabited (Batteries.Vector α n)

The Inhabited instance for Vector α n with [Inhabited α] produces a vector of size n with all its elements equal to the default element of type α

Equations

• Batteries.Vector.instInhabited = { default := Batteries.Vector.mkVector n default }

def Batteries.Vector.toList {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) : List α

The list obtained from a vector.

Equations

• v.toList = v.toArray.toList

def Batteries.Vector.get {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) : α

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

Equations

• v.get i = v.toArray.get (Fin.cast ⋯ i)

def Batteries.Vector.uget {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : USize) (h : i.toNat < n) : α

Vector lookup function that takes an index i of type USize

Equations

• v.uget i h = v.toArray.uget i ⋯

instance Batteries.Vector.instGetElemNatLt {α : Type u_1} {n : Nat} : GetElem (Batteries.Vector α n) Nat α fun (x : Batteries.Vector α n) (i : Nat) => i < n

Vector α n nstance for the GetElem typeclass.

Equations

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

def Batteries.Vector.getD {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (v₀ : α) : α

getD v i v₀ gets the iᵗʰ element of v if valid. Otherwise it returns v₀ by default

Equations

• v.getD i v₀ = v.toArray.getD i v₀

@[reducible, inline]

abbrev Batteries.Vector.back! {α : Type u_1} {n : Nat} [Inhabited α] (v : Batteries.Vector α n) : α

v.back! v gets the last element of the vector. panics if v is empty.

Equations

• v.back! = v[n - 1]!

@[reducible, inline]

abbrev Batteries.Vector.back? {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) : Option α

v.back? gets the last element x of the array as some x if it exists. Else the vector is empty and it returns none

Equations

• v.back? = v[n - 1]?

@[reducible, inline]

abbrev Batteries.Vector.head {α : Type u_1} {n : Nat} (v : Batteries.Vector α (n + 1)) : α

Vector.head produces the head of a vector

Equations

• v.head = v[0]

def Batteries.Vector.push {α : Type u_1} {n : Nat} (x : α) (v : Batteries.Vector α n) : Batteries.Vector α (n + 1)

push v x pushes x to the end of vector v in O(1) time

Equations

• Batteries.Vector.push x v = { toArray := v.toArray.push x, size_eq := ⋯ }

def Batteries.Vector.pop {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) : Batteries.Vector α (n - 1)

pop v returns the vector with the last element removed

Equations

• v.pop = { toArray := v.toArray.pop, size_eq := ⋯ }

def Batteries.Vector.set {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (x : α) : Batteries.Vector α n

Sets an element in a vector using a Fin index.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• v.set i x = { toArray := v.toArray.set (Fin.cast ⋯ i) x, size_eq := ⋯ }

def Batteries.Vector.setN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) (h : autoParam (i < n) _auto✝) : Batteries.Vector α n

setN v i h x sets an element in a vector using a Nat index which is provably valid. By default a proof by get_elem_tactic is provided.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• v.setN i x h = v.set ⟨i, h⟩ x

def Batteries.Vector.setD {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : Batteries.Vector α n

Sets an element in a vector, or do nothing if the index is out of bounds.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• v.setD i x = { toArray := v.toArray.setD i x, size_eq := ⋯ }

def Batteries.Vector.set! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : Batteries.Vector α n

Sets an element in an array, or panic if the index is out of bounds.

This will perform the update destructively provided that a has a reference count of 1 when called.

Equations

• v.set! i x = { toArray := v.toArray.set! i x, size_eq := ⋯ }

def Batteries.Vector.append {α : Type u_1} {n : Nat} {m : Nat} : Batteries.Vector α n → Batteries.Vector α m → Batteries.Vector α (n + m)

Appends a vector to another.

Equations

• { toArray := a₁, size_eq := size_eq }.append { toArray := a₂, size_eq := size_eq_1 } = { toArray := a₁ ++ a₂, size_eq := ⋯ }

instance Batteries.Vector.instHAppendHAddNat {α : Type u_1} {n : Nat} {m : Nat} : HAppend (Batteries.Vector α n) (Batteries.Vector α m) (Batteries.Vector α (n + m))

Equations

• Batteries.Vector.instHAppendHAddNat = { hAppend := Batteries.Vector.append }

def Batteries.Vector.cast {α : Type u_1} {n : Nat} {m : Nat} (h : n = m) : Batteries.Vector α n → Batteries.Vector α m

Creates a vector from another with a provably equal length.

Equations

• Batteries.Vector.cast h { toArray := x_1, size_eq := p } = { toArray := x_1, size_eq := ⋯ }

def Batteries.Vector.extract {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (start : Nat) (stop : Nat) : Batteries.Vector α (min stop n - start)

extract v start halt Returns the slice of v from indices start to stop (exclusive). If start is greater or equal to stop, the result is empty. If stop is greater than the size of v, the size is used instead.

Equations

• v.extract start stop = { toArray := v.toArray.extract start stop, size_eq := ⋯ }

def Batteries.Vector.map {α : Type u_1} {β : Type u_2} {n : Nat} (f : α → β) (v : Batteries.Vector α n) : Batteries.Vector β n

Maps a vector under a function.

Equations

• Batteries.Vector.map f v = { toArray := Array.map f v.toArray, size_eq := ⋯ }

def Batteries.Vector.zipWith {α : Type u_1} {n : Nat} {β : Type u_2} {φ : Type u_3} (a : Batteries.Vector α n) (b : Batteries.Vector β n) (f : α → β → φ) : Batteries.Vector φ n

Maps two vectors under a curried function of two variables.

Equations

• { toArray := a, size_eq := h₁ }.zipWith { toArray := b, size_eq := h₂ } x = { toArray := a.zipWith b x, size_eq := ⋯ }

def Batteries.Vector.ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : Batteries.Vector α n

Returns a vector of length n from a function on Fin n.

Equations

• Batteries.Vector.ofFn f = { toArray := Array.ofFn f, size_eq := ⋯ }

def Batteries.Vector.swap {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (j : Fin n) : Batteries.Vector α n

Swaps two entries in a Vector.

This will perform the update destructively provided that v has a reference count of 1 when called.

Equations

• v.swap i j = { toArray := v.toArray.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), size_eq := ⋯ }

def Batteries.Vector.swapN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (j : Nat) (hi : autoParam (i < n) _auto✝) (hj : autoParam (j < n) _auto✝) : Batteries.Vector α n

swapN v i j hi hj swaps two Nat indexed entries in a Vector α n. Uses get_elem_tactic to supply proofs hi and hj respectively that the indices i and j are in range.

This will perform the update destructively provided that v has a reference count of 1 when called.

Equations

• v.swapN i j hi hj = v.swap ⟨i, hi⟩ ⟨j, hj⟩

def Batteries.Vector.swap! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (j : Nat) : Batteries.Vector α n

Swaps two entries in a Vector α n, or panics if either index is out of bounds.

This will perform the update destructively provided that v has a reference count of 1 when called.

Equations

• v.swap! i j = { toArray := v.toArray.swap! i j, size_eq := ⋯ }

def Batteries.Vector.swapAt {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (x : α) : α × Batteries.Vector α n

Swaps the entry with index i : Fin n in the vector for a new entry. The old entry is returned with the modified vector.

Equations

• v.swapAt i x = ((v.toArray.swapAt (Fin.cast ⋯ i) x).fst, { toArray := (v.toArray.swapAt (Fin.cast ⋯ i) x).snd, size_eq := ⋯ })

def Batteries.Vector.swapAtN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) (h : autoParam (i < n) _auto✝) : α × Batteries.Vector α n

Swaps the entry with index i : Nat in the vector for a new entry x. The old entry is returned alongwith the modified vector.

Automatically generates a proof of i < n with get_elem_tactic where feasible.

Equations

• v.swapAtN i x h = v.swapAt ⟨i, h⟩ x

@[inline]

def Batteries.Vector.swapAt! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) : α × Batteries.Vector α n

swapAt! v i x swaps out the entry at index i : Nat in the vector for x, if the index is valid. Otherwise it panics The old entry is returned with the modified vector.

Equations

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

def Batteries.Vector.range (n : Nat) : Batteries.Vector Nat n

range n returns the vector #v[0,1,2,...,n-1].

Equations

• Batteries.Vector.range n = { toArray := Array.range n, size_eq := ⋯ }

def Batteries.Vector.shrink {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (m : Nat) : Batteries.Vector α (min n m)

shrink v m shrinks the vector to the first m elements if m < n. Returns v unchanged if m ≥ n.

Equations

• v.shrink m = { toArray := v.toArray.shrink m, size_eq := ⋯ }

def Batteries.Vector.drop {α : Type u_1} {n : Nat} (i : Nat) (v : Batteries.Vector α n) : Batteries.Vector α (n - i)

Drops the first (up to) i elements from a vector of length n. If m ≥ n, the return value is empty.

Equations

• Batteries.Vector.drop i v = Batteries.Vector.cast ⋯ (v.extract i n)

def Batteries.Vector.take {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (m : Nat) : Batteries.Vector α (min n m)

Takes the first (up to) i elements from a vector of length n.

Equations

• @Batteries.Vector.take = @Batteries.Vector.shrink

@[inline]

def Batteries.Vector.isEqv {α : Type u_1} {n : Nat} (a : Batteries.Vector α n) (b : Batteries.Vector α n) (p : α → α → Bool) : Bool

isEqv takes a given boolean property p. It returns true if and only if p a[i] b[i] holds true for all valid indices i.

Equations

• a.isEqv b p = a.toArray.isEqvAux b.toArray ⋯ p 0

instance Batteries.Vector.instBEq {α : Type u_1} {n : Nat} [BEq α] : BEq (Batteries.Vector α n)

Equations

• Batteries.Vector.instBEq = { beq := fun (a b : Batteries.Vector α n) => a.isEqv b BEq.beq }

def Batteries.Vector.reverse {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) : Batteries.Vector α n

reverse v reverses the vector v.

Equations

• v.reverse = { toArray := v.toArray.reverse, size_eq := ⋯ }

def Batteries.Vector.feraseIdx {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) : Batteries.Vector α (n - 1)

O(|v| - i). feraseIdx v i removes the element at position i in vector v.

Equations

• v.feraseIdx i = { toArray := v.toArray.feraseIdx (Fin.cast ⋯ i), size_eq := ⋯ }

@[inline]

def Batteries.Vector.tail {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) : Batteries.Vector α (n - 1)

Vector.tail produces the tail of the vector v.

Equations

• v_2.tail = v_2
• v_2.tail = v_2.feraseIdx 0

@[inline]

def Batteries.Vector.eraseIdx! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) : Batteries.Vector α (n - 1)

O(|v| - i). eraseIdx! v i removes the element at position i from vector v of length n. Panics if i is not less than n.

Equations

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

@[reducible, inline]

abbrev Batteries.Vector.eraseIdxN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (h : autoParam (i < n) _auto✝) : Batteries.Vector α (n - 1)

eraseIdxN v i h removes the element at position i from a vector of length n. h : i < n has a default argument by get_elem_tactic which tries to supply a proof that the index is valid.

This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

Equations

• v.eraseIdxN i h = v.feraseIdx ⟨i, h⟩

def Batteries.Vector.indexOf? {α : Type u_1} {n : Nat} [BEq α] (v : Batteries.Vector α n) (x : α) : Option (Fin n)

If x is an element of vector v at index j, then indexOf? v x returns some j. Otherwise it returns none.

Equations

• v.indexOf? x = match v.toArray.indexOf? x with | some res => some (Fin.cast ⋯ res) | none => none

def Batteries.Vector.isPrefixOf {α : Type u_1} {m : Nat} {n : Nat} [BEq α] (as : Batteries.Vector α m) (bs : Batteries.Vector α n) : Bool

isPrefixOf as bs returns true iff vector as is a prefix of vectorbs

Equations

• as.isPrefixOf bs = as.toArray.isPrefixOf bs.toArray

def Batteries.Vector.allDiff {α : Type u_1} {n : Nat} [BEq α] (as : Batteries.Vector α n) : Bool

allDiff as i returns true when all elements of v are distinct from each other`

Equations

• as.allDiff = as.toArray.allDiff