@[reducible, inline]

abbrev Data.Vector (α : Type u) : Type u

Boxed vector type. Lean's Array is already the equivalent of Haskell's Vector. $$\text{Vector}\ \alpha := \text{Array}\ \alpha$$

Equations

• Data.Vector α = Array α

@[inline]

def Data.Vector.empty {α : Type u_1} : Vector α

The empty vector. $$\text{empty} : \text{Vector}\ \alpha,\quad |\text{empty}| = 0$$

Equations

• Data.Vector.empty = #[]

@[inline]

def Data.Vector.singleton {α : Type u_1} (x : α) : Vector α

A vector containing a single element. $$\text{singleton}(x) = [x]$$

Equations

• Data.Vector.singleton x = #[x]

@[inline]

def Data.Vector.fromList {α : Type u_1} (xs : List α) : Vector α

Convert a list to a vector. $$\text{fromList}([x_1, \ldots, x_n]) = [x_1, \ldots, x_n]$$

Equations

• Data.Vector.fromList xs = xs.toArray

@[inline]

def Data.Vector.toList {α : Type u_1} (v : Vector α) : List α

Convert a vector to a list. $$\text{toList}([x_1, \ldots, x_n]) = [x_1, \ldots, x_n]$$

Equations

• v.toList = v.toList

@[inline]

def Data.Vector.replicate {α : Type u_1} (n : Nat) (x : α) : Vector α

Create a vector of n copies of element x. $$\text{replicate}(n, x) = [x, x, \ldots, x],\quad |\text{result}| = n$$

Equations

• Data.Vector.replicate n x = (List.replicate n x).toArray

def Data.Vector.generate {α : Type u_1} (n : Nat) (f : Nat → α) : Vector α

Create a vector of length n by applying f to each index. $$\text{generate}(n, f) = [f(0), f(1), \ldots, f(n-1)]$$

Equations

• Data.Vector.generate n f = Data.Vector.generate.go f n 0 #[]

def Data.Vector.generate.go {α : Type u_1} (f : Nat → α) : Nat → Nat → Vector α → Vector α

Equations

• Data.Vector.generate.go f 0 a✝¹ a✝ = a✝
• Data.Vector.generate.go f fuel.succ a✝¹ a✝ = Data.Vector.generate.go f fuel (a✝¹ + 1) (Array.push a✝ (f a✝¹))

@[inline]

def Data.Vector.length {α : Type u_1} (v : Vector α) : Nat

The number of elements. $$\text{length}(v) = |v|$$

Equations

• v.length = Array.size v

@[inline]

def Data.Vector.null {α : Type u_1} (v : Vector α) : Bool

Is the vector empty? $$\text{null}(v) \iff |v| = 0$$

Equations

• v.null = (Array.size v == 0)

@[inline]

def Data.Vector.getOp {α : Type u_1} (v : Vector α) (i : Nat) : Option α

Index into the vector. Returns none if out of bounds. $$v\text{!}(i) = v_i$$

Equations

• v.getOp i = if h : i < Array.size v then some v[i] else none

def Data.Vector.head {α : Type u_1} (v : Vector α) (h : Array.size v > 0 := by omega) : α

The first element of a non-empty vector. $$\text{head}(v) = v_0,\quad \text{requires } |v| > 0$$

Equations

• v.head h = v[0]

def Data.Vector.last {α : Type u_1} (v : Vector α) (h : Array.size v > 0 := by omega) : α

The last element of a non-empty vector. $$\text{last}(v) = v_{|v|-1},\quad \text{requires } |v| > 0$$

Equations

• v.last h = v[Array.size v - 1]

def Data.Vector.slice {α : Type u_1} (i n : Nat) (v : Vector α) : Vector α

Extract a slice from index i of length n. $$\text{slice}(i, n, v) = [v_i, v_{i+1}, \ldots, v_{i+n-1}]$$

Equations

• Data.Vector.slice i n v = (List.take n (List.drop i v.toList)).toArray

def Data.Vector.init {α : Type u_1} (v : Vector α) : autoParam (Array.size v > 0) init._auto_1 → Vector α

All elements except the last. $$\text{init}(v) = v[0..|v|-1],\quad \text{requires } |v| > 0$$

Equations

• v.init x✝ = v.toList.dropLast.toArray

def Data.Vector.tail {α : Type u_1} (v : Vector α) : autoParam (Array.size v > 0) tail._auto_1 → Vector α

All elements except the first. $$\text{tail}(v) = v[1..],\quad \text{requires } |v| > 0$$

Equations

• v.tail x✝ = (List.drop 1 v.toList).toArray

@[inline]

def Data.Vector.take {α : Type u_1} (n : Nat) (v : Vector α) : Vector α

Take the first n elements. $$\text{take}(n, v) = v[0..n]$$

Equations

• Data.Vector.take n v = (List.take n v.toList).toArray

@[inline]

def Data.Vector.drop {α : Type u_1} (n : Nat) (v : Vector α) : Vector α

Drop the first n elements. $$\text{drop}(n, v) = v[n..]$$

Equations

• Data.Vector.drop n v = (List.drop n v.toList).toArray

@[inline]

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

Apply a function to every element. $$\text{map}(f, [x_1, \ldots, x_n]) = [f(x_1), \ldots, f(x_n)]$$

Equations

• Data.Vector.map f v = Array.map f v

def Data.Vector.imap {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (v : Vector α) : Vector β

Map with index. $$\text{imap}(f, [x_0, \ldots, x_{n-1}]) = [f(0, x_0), \ldots, f(n-1, x_{n-1})]$$

Equations

• Data.Vector.imap f v = Data.Vector.imap.go f v 0 #[]

@[irreducible]

def Data.Vector.imap.go {α : Type u_1} {β : Type u_2} (f : Nat → α → β) (v : Vector α) (i : Nat) (acc : Array β) : Vector β

Equations

• Data.Vector.imap.go f v i acc = if h : i < Array.size v then Data.Vector.imap.go f v (i + 1) (acc.push (f i v[i])) else acc

def Data.Vector.concatMap {α : Type u_1} {β : Type u_2} (f : α → Vector β) (v : Vector α) : Vector β

Map and concatenate. $$\text{concatMap}(f, v) = \text{concat}(\text{map}(f, v))$$

Equations

• Data.Vector.concatMap f v = Array.foldl (fun (acc : Data.Vector β) (x : α) => acc ++ f x) #[] v

@[inline]

def Data.Vector.filter {α : Type u_1} (p : α → Bool) (v : Vector α) : Vector α

Keep elements satisfying a predicate. $$\text{filter}(p, v) = [x \in v \mid p(x)]$$

Equations

• Data.Vector.filter p v = Array.filter p v

def Data.Vector.ifilter {α : Type u_1} (p : Nat → α → Bool) (v : Vector α) : Vector α

Filter with index. $$\text{ifilter}(p, v) = [v_i \mid p(i, v_i)]$$

Equations

• Data.Vector.ifilter p v = Data.Vector.ifilter.go p v 0 #[]

@[irreducible]

def Data.Vector.ifilter.go {α : Type u_1} (p : Nat → α → Bool) (v : Vector α) (i : Nat) (acc : Array α) : Vector α

Equations

• Data.Vector.ifilter.go p v i acc = if h : i < Array.size v then have acc' := if p i v[i] = true then acc.push v[i] else acc; Data.Vector.ifilter.go p v (i + 1) acc' else acc

@[inline]

def Data.Vector.foldl' {β : Type u_1} {α : Type u_2} (f : β → α → β) (z : β) (v : Vector α) : β

Strict left fold. $$\text{foldl'}(f, z, [x_1, \ldots, x_n]) = f(\ldots f(f(z, x_1), x_2) \ldots, x_n)$$

Equations

• Data.Vector.foldl' f z v = Array.foldl f z v

def Data.Vector.foldl1' {α : Type u_1} (f : α → α → α) (v : Vector α) (h : Array.size v > 0 := by omega) : α

Strict left fold on non-empty vector using first element as seed. $$\text{foldl1'}(f, [x_1, \ldots, x_n]) = f(\ldots f(x_1, x_2) \ldots, x_n)$$

Equations

• Data.Vector.foldl1' f v h = Data.Vector.foldl1'.go f v 1 v[0]

@[irreducible]

def Data.Vector.foldl1'.go {α : Type u_1} (f : α → α → α) (v : Vector α) (i : Nat) (acc : α) : α

Equations

• Data.Vector.foldl1'.go f v i acc = if hi : i < Array.size v then Data.Vector.foldl1'.go f v (i + 1) (f acc v[i]) else acc

@[inline]

def Data.Vector.foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (z : β) (v : Vector α) : β

Right fold. $$\text{foldr}(f, z, [x_1, \ldots, x_n]) = f(x_1, f(x_2, \ldots f(x_n, z)))$$

Equations

• Data.Vector.foldr f z v = Array.foldr f z v

def Data.Vector.foldr1 {α : Type u_1} (f : α → α → α) (v : Vector α) (h : Array.size v > 0 := by omega) : α

Right fold on non-empty vector using last element as seed. $$\text{foldr1}(f, [x_1, \ldots, x_n]) = f(x_1, f(x_2, \ldots f(x_{n-1}, x_n)))$$

Equations

• Data.Vector.foldr1 f v h = Data.Vector.foldr1.go f v (Array.size v - 2) v[Array.size v - 1]

def Data.Vector.foldr1.go {α : Type u_1} (f : α → α → α) (v : Vector α) : Nat → α → α

Equations

• Data.Vector.foldr1.go f v 0 a✝ = if h0 : 0 < Array.size v then f v[0] a✝ else a✝
• Data.Vector.foldr1.go f v i.succ a✝ = if hi : i + 1 < Array.size v then Data.Vector.foldr1.go f v i (f v[i + 1] a✝) else a✝

def Data.Vector.ifoldl' {β : Sort u_1} {α : Type u_2} (f : β → Nat → α → β) (z : β) (v : Vector α) : β

Strict left fold with index. $$\text{ifoldl'}(f, z, v) = f(\ldots f(f(z, 0, v_0), 1, v_1) \ldots, n-1, v_{n-1})$$

Equations

• Data.Vector.ifoldl' f z v = Data.Vector.ifoldl'.go f v 0 z

@[irreducible]

def Data.Vector.ifoldl'.go {β : Sort u_1} {α : Type u_2} (f : β → Nat → α → β) (v : Vector α) (i : Nat) (acc : β) : β

Equations

• Data.Vector.ifoldl'.go f v i acc = if h : i < Array.size v then Data.Vector.ifoldl'.go f v (i + 1) (f acc i v[i]) else acc

def Data.Vector.ifoldr {α : Type u_1} {β : Sort u_2} (f : Nat → α → β → β) (z : β) (v : Vector α) : β

Right fold with index. $$\text{ifoldr}(f, z, v) = f(0, v_0, f(1, v_1, \ldots f(n-1, v_{n-1}, z)))$$

Equations

• Data.Vector.ifoldr f z v = Data.Vector.ifoldr.go f v (Array.size v) z

def Data.Vector.ifoldr.go {α : Type u_1} {β : Sort u_2} (f : Nat → α → β → β) (v : Vector α) : Nat → β → β

Equations

• Data.Vector.ifoldr.go f v 0 a✝ = a✝
• Data.Vector.ifoldr.go f v i.succ a✝ = if h : i < Array.size v then Data.Vector.ifoldr.go f v i (f i v[i] a✝) else a✝

@[inline]

def Data.Vector.all {α : Type u_1} (p : α → Bool) (v : Vector α) : Bool

Do all elements satisfy the predicate? $$\text{all}(p, v) = \forall x \in v.\; p(x)$$

Equations

• Data.Vector.all p v = Array.all v p

@[inline]

def Data.Vector.any {α : Type u_1} (p : α → Bool) (v : Vector α) : Bool

Does any element satisfy the predicate? $$\text{any}(p, v) = \exists x \in v.\; p(x)$$

Equations

• Data.Vector.any p v = Array.any v p

def Data.Vector.and (v : Vector Bool) : Bool

Are all elements true? $$\text{and}(v) = \bigwedge v$$

Equations

• v.and = Array.all v id

def Data.Vector.or (v : Vector Bool) : Bool

Is any element true? $$\text{or}(v) = \bigvee v$$

Equations

• v.or = Array.any v id

def Data.Vector.sum {α : Type u_1} [Add α] [OfNat α 0] (v : Vector α) : α

Sum of all elements. $$\text{sum}(v) = \sum v$$

Equations

• v.sum = Array.foldl (fun (x1 x2 : α) => x1 + x2) 0 v

def Data.Vector.product {α : Type u_1} [Mul α] [OfNat α 1] (v : Vector α) : α

Product of all elements. $$\text{product}(v) = \prod v$$

Equations

• v.product = Array.foldl (fun (x1 x2 : α) => x1 * x2) 1 v

def Data.Vector.maximum {α : Type u_1} [Ord α] (v : Vector α) (h : Array.size v > 0 := by omega) : α

Maximum element of a non-empty vector. $$\text{maximum}(v) = \max(v),\quad \text{requires } |v| > 0$$

Equations

• v.maximum h = Data.Vector.maximum.go v 1 v[0]

@[irreducible]

def Data.Vector.maximum.go {α : Type u_1} [Ord α] (v : Vector α) (i : Nat) (best : α) : α

Equations

• Data.Vector.maximum.go v i best = if hi : i < Array.size v then have x := v[i]; Data.Vector.maximum.go v (i + 1) (if (compare x best == Ordering.gt) = true then x else best) else best

def Data.Vector.minimum {α : Type u_1} [Ord α] (v : Vector α) (h : Array.size v > 0 := by omega) : α

Minimum element of a non-empty vector. $$\text{minimum}(v) = \min(v),\quad \text{requires } |v| > 0$$

Equations

• v.minimum h = Data.Vector.minimum.go v 1 v[0]

@[irreducible]

def Data.Vector.minimum.go {α : Type u_1} [Ord α] (v : Vector α) (i : Nat) (best : α) : α

Equations

• Data.Vector.minimum.go v i best = if hi : i < Array.size v then have x := v[i]; Data.Vector.minimum.go v (i + 1) (if (compare x best == Ordering.lt) = true then x else best) else best

def Data.Vector.elem {α : Type u_1} [BEq α] (x : α) (v : Vector α) : Bool

Does the element occur in the vector? $$\text{elem}(x, v) = \exists i.\; v_i = x$$

Equations

• Data.Vector.elem x v = Array.any v fun (x_1 : α) => x_1 == x

def Data.Vector.notElem {α : Type u_1} [BEq α] (x : α) (v : Vector α) : Bool

Does the element NOT occur in the vector? $$\text{notElem}(x, v) = \neg\text{elem}(x, v)$$

Equations

• Data.Vector.notElem x v = !Data.Vector.elem x v

def Data.Vector.find {α : Type u_1} (p : α → Bool) (v : Vector α) : Option α

Find the first element satisfying a predicate. $$\text{find}(p, v)$$

Equations

• Data.Vector.find p v = Data.Vector.find.go p v 0

@[irreducible]

def Data.Vector.find.go {α : Type u_1} (p : α → Bool) (v : Vector α) (i : Nat) : Option α

Equations

• Data.Vector.find.go p v i = if h : i < Array.size v then if p v[i] = true then some v[i] else Data.Vector.find.go p v (i + 1) else none

def Data.Vector.findIndex {α : Type u_1} (p : α → Bool) (v : Vector α) : Option Nat

Find the index of the first element satisfying a predicate. $$\text{findIndex}(p, v)$$

Equations

• Data.Vector.findIndex p v = Data.Vector.findIndex.go p v 0

@[irreducible]

def Data.Vector.findIndex.go {α : Type u_1} (p : α → Bool) (v : Vector α) (i : Nat) : Option Nat

Equations

• Data.Vector.findIndex.go p v i = if h : i < Array.size v then if p v[i] = true then some i else Data.Vector.findIndex.go p v (i + 1) else none

def Data.Vector.zip {α : Type u_1} {β : Type u_2} (u : Vector α) (v : Vector β) : Vector (α × β)

Zip two vectors into a vector of pairs. $$\text{zip}(u, v) = [(u_0, v_0), (u_1, v_1), \ldots]$$

Equations

• u.zip v = (u.toList.zip v.toList).toArray

def Data.Vector.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (u : Vector α) (v : Vector β) : Vector γ

Zip two vectors with a combining function. $$\text{zipWith}(f, u, v) = [f(u_0, v_0), f(u_1, v_1), \ldots]$$

Equations

• Data.Vector.zipWith f u v = (List.zipWith f u.toList v.toList).toArray

def Data.Vector.unzip {α : Type u_1} {β : Type u_2} (v : Vector (α × β)) : Vector α × Vector β

Unzip a vector of pairs into a pair of vectors. $$\text{unzip}([(a_1, b_1), \ldots]) = ([a_1, \ldots], [b_1, \ldots])$$

Equations

• v.unzip = match v.toList.unzip with | (as_, bs_) => (as_.toArray, bs_.toArray)

@[inline]

def Data.Vector.reverse {α : Type u_1} (v : Vector α) : Vector α

Reverse the elements. $$\text{reverse}([x_1, \ldots, x_n]) = [x_n, \ldots, x_1]$$

Equations

• v.reverse = Array.reverse v

def Data.Vector.backpermute {α : Type u_1} [Inhabited α] (v : Vector α) (is : Vector Nat) : Vector α

Permute elements according to an index vector. $$\text{backpermute}(v, is) = [v_{is_0}, v_{is_1}, \ldots]$$ Out-of-bounds indices produce a default value.

Equations

• v.backpermute is = Array.map (fun (i : Nat) => if h : i < Array.size v then v[i] else default) is

def Data.Vector.modify {α : Type u_1} (f : α → α) (i : Nat) (v : Vector α) : Vector α

Modify the element at index i by applying f. $$\text{modify}(f, i, v)$$ returns $v$ with $v_i$ replaced by $f(v_i)$. If i is out of bounds, returns v unchanged.

Equations

• Data.Vector.modify f i v = if h : i < Array.size v then Array.set v i (f v[i]) h else v

@[inline]

def Data.Vector.snoc {α : Type u_1} (v : Vector α) (x : α) : Vector α

Append an element to the end. $$\text{snoc}(v, x) = [v_0, \ldots, v_{n-1}, x]$$

Equations

• v.snoc x = Array.push v x

def Data.Vector.cons {α : Type u_1} (x : α) (v : Vector α) : Vector α

Prepend an element to the front. $$\text{cons}(x, v) = [x, v_0, \ldots, v_{n-1}]$$

Equations

• Data.Vector.cons x v = #[x] ++ v

theorem Data.Vector.toList_fromList {α : Type u_1} (xs : List α) : (fromList xs).toList = xs

fromList and toList are inverses. $$\text{toList}(\text{fromList}(xs)) = xs$$

theorem Data.Vector.length_empty {α : Type u_1} : empty.length = 0

length of empty is zero. $$\text{length}(\text{empty}) = 0$$

theorem Data.Vector.length_singleton {α : Type u_1} (x : α) : (singleton x).length = 1

length of singleton is one. $$\text{length}(\text{singleton}(x)) = 1$$

theorem Data.Vector.null_empty {α : Type u_1} : empty.null = true

null of empty is true. $$\text{null}(\text{empty}) = \text{true}$$

theorem Data.Vector.null_singleton {α : Type u_1} (x : α) : (singleton x).null = false

null of singleton is false. $$\text{null}(\text{singleton}(x)) = \text{false}$$

theorem Data.Vector.length_fromList {α : Type u_1} (xs : List α) : (fromList xs).length = xs.length

fromList preserves length. $$\text{length}(\text{fromList}(xs)) = \text{List.length}(xs)$$

theorem Data.Vector.length_reverse {α : Type u_1} (v : Vector α) : v.reverse.length = v.length

reverse preserves length. $$\text{length}(\text{reverse}(v)) = \text{length}(v)$$

theorem Data.Vector.length_map {α : Type u_1} {β : Type u_2} (f : α → β) (v : Vector α) : (map f v).length = v.length

map preserves length. $$\text{length}(\text{map}(f, v)) = \text{length}(v)$$

theorem Data.Vector.reverse_reverse {α : Type u_1} (v : Vector α) : v.reverse.reverse = v

reverse is an involution. $$\text{reverse}(\text{reverse}(v)) = v$$