Additional theorems and definitions about the Vector type

This file introduces the infix notation ::ᵥ for Vector.cons.

ink

def Vector.«term_::ᵥ_» : Lean.TrailingParserDescr

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.«term_::ᵥ_» = Lean.ParserDescr.trailingNode `Vector.term_::ᵥ_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ᵥ ") (Lean.ParserDescr.cat `term 67))

ink

instance Vector.instInhabitedVector {n : ℕ} {α : Type u_1} [inst : Inhabited α] : Inhabited (Vector α n)

Equations

• Vector.instInhabitedVector = { default := Vector.ofFn default }

ink

theorem Vector.toList_injective {n : ℕ} {α : Type u_1} : Function.Injective Vector.toList

ink

theorem Vector.ext {n : ℕ} {α : Type u_1} {v : Vector α n} {w : Vector α n} : (∀ (m : Fin n), Vector.get v m = Vector.get w m) → v = w

Two v w : Vector α n are equal iff they are equal at every single index.

ink

instance Vector.zero_subsingleton {α : Type u_1} : Subsingleton (Vector α 0)

The empty Vector is a Subsingleton.

Equations

• @Vector.zero_subsingleton = @Vector.zero_subsingleton.proof_1

ink

@[simp]

theorem Vector.cons_val {n : ℕ} {α : Type u_1} (a : α) (v : Vector α n) : ↑(a ::ᵥ v) = a :: ↑v

ink

theorem Vector.eq_cons_iff {n : ℕ} {α : Type u_1} (a : α) (v : Vector α (Nat.succ n)) (v' : Vector α n) : v = a ::ᵥ v' ↔ Vector.head v = a ∧ Vector.tail v = v'

ink

theorem Vector.ne_cons_iff {n : ℕ} {α : Type u_1} (a : α) (v : Vector α (Nat.succ n)) (v' : Vector α n) : v ≠ a ::ᵥ v' ↔ Vector.head v ≠ a ∨ Vector.tail v ≠ v'

ink

theorem Vector.exists_eq_cons {n : ℕ} {α : Type u_1} (v : Vector α (Nat.succ n)) : ∃ a as, v = a ::ᵥ as

ink

@[simp]

theorem Vector.toList_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) : Vector.toList (Vector.ofFn f) = List.ofFn f

ink

@[simp]

theorem Vector.mk_toList {n : ℕ} {α : Type u_1} (v : Vector α n) (h : List.length (Vector.toList v) = n) : { val := Vector.toList v, property := h } = v

ink

@[simp]

theorem Vector.length_val {n : ℕ} {α : Type u_1} (v : Vector α n) : List.length ↑v = n

ink

@[simp]

theorem Vector.toList_map {n : ℕ} {α : Type u_2} {β : Type u_1} (v : Vector α n) (f : α → β) : Vector.toList (Vector.map f v) = List.map f (Vector.toList v)

ink

@[simp]

theorem Vector.head_map {n : ℕ} {α : Type u_2} {β : Type u_1} (v : Vector α (n + 1)) (f : α → β) : Vector.head (Vector.map f v) = f (Vector.head v)

ink

@[simp]

theorem Vector.tail_map {n : ℕ} {α : Type u_2} {β : Type u_1} (v : Vector α (n + 1)) (f : α → β) : Vector.tail (Vector.map f v) = Vector.map f (Vector.tail v)

ink

theorem Vector.get_eq_get {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n) : Vector.get v i = List.get (Vector.toList v) (↑(RelIso.toRelEmbedding (Fin.cast (_ : n = List.length (Vector.toList v)))).toEmbedding i)

ink

theorem Vector.nth_eq_nthLe {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n) : Vector.get v i = List.nthLe (Vector.toList v) ↑i (_ : ↑i < List.length (Vector.toList v))

ink

@[simp]

theorem Vector.get_replicate {n : ℕ} {α : Type u_1} (a : α) (i : Fin n) : Vector.get (Vector.replicate n a) i = a

ink

@[simp]

theorem Vector.get_map {n : ℕ} {α : Type u_2} {β : Type u_1} (v : Vector α n) (f : α → β) (i : Fin n) : Vector.get (Vector.map f v) i = f (Vector.get v i)

ink

@[simp]

theorem Vector.get_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n) : Vector.get (Vector.ofFn f) i = f i

ink

@[simp]

theorem Vector.ofFn_get {n : ℕ} {α : Type u_1} (v : Vector α n) : Vector.ofFn (Vector.get v) = v

ink

def Equiv.vectorEquivFin (α : Type u_1) (n : ℕ) : Vector α n ≃ (Fin n → α)

The natural equivalence between length-n vectors and functions from Fin n.

Equations

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

ink

theorem Vector.get_tail {n : ℕ} {α : Type u_1} (x : Vector α n) (i : Fin (n - 1)) : Vector.get (Vector.tail x) i = Vector.get x { val := ↑i + 1, isLt := (_ : ↑i + 1 < n) }

ink

@[simp]

theorem Vector.get_tail_succ {n : ℕ} {α : Type u_1} (v : Vector α (Nat.succ n)) (i : Fin n) : Vector.get (Vector.tail v) i = Vector.get v (Fin.succ i)

ink

@[simp]

theorem Vector.tail_val {n : ℕ} {α : Type u_1} (v : Vector α (Nat.succ n)) : ↑(Vector.tail v) = List.tail ↑v

ink

@[simp]

theorem Vector.tail_nil {α : Type u_1} : Vector.tail Vector.nil = Vector.nil

The tail of a nil vector is nil.

ink

@[simp]

theorem Vector.singleton_tail {α : Type u_1} (v : Vector α 1) : Vector.tail v = Vector.nil

The tail of a vector made up of one element is nil.

ink

@[simp]

theorem Vector.tail_ofFn {α : Type u_1} {n : ℕ} (f : Fin (Nat.succ n) → α) : Vector.tail (Vector.ofFn f) = Vector.ofFn fun i => f (Fin.succ i)

ink

@[simp]

theorem Vector.toList_empty {α : Type u_1} (v : Vector α 0) : Vector.toList v = []

ink

@[simp]

theorem Vector.toList_singleton {α : Type u_1} (v : Vector α 1) : Vector.toList v = [Vector.head v]

The list that makes up a Vector made up of a single element, retrieved via toList, is equal to the list of that single element.

ink

@[simp]

theorem Vector.empty_toList_eq_ff {n : ℕ} {α : Type u_1} (v : Vector α (n + 1)) : List.isEmpty (Vector.toList v) = false

ink

theorem Vector.not_empty_toList {n : ℕ} {α : Type u_1} (v : Vector α (n + 1)) : ¬List.isEmpty (Vector.toList v) = true

ink

@[simp]

theorem Vector.map_id {α : Type u_1} {n : ℕ} (v : Vector α n) : Vector.map id v = v

Mapping under id does not change a vector.

ink

theorem Vector.nodup_iff_injective_get {n : ℕ} {α : Type u_1} {v : Vector α n} : List.Nodup (Vector.toList v) ↔ Function.Injective (Vector.get v)

ink

theorem Vector.head?_toList {n : ℕ} {α : Type u_1} (v : Vector α (Nat.succ n)) : List.head? (Vector.toList v) = some (Vector.head v)

ink

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

Reverse a vector.

Equations

• Vector.reverse v = { val := List.reverse (Vector.toList v), property := (_ : List.length (List.reverse (Vector.toList v)) = n) }

ink

theorem Vector.toList_reverse {n : ℕ} {α : Type u_1} {v : Vector α n} : Vector.toList (Vector.reverse v) = List.reverse (Vector.toList v)

The List of a vector after a reverse, retrieved by toList is equal to the List.reverse after retrieving a vector's toList.

ink

@[simp]

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

ink

@[simp]

theorem Vector.get_zero {n : ℕ} {α : Type u_1} (v : Vector α (Nat.succ n)) : Vector.get v 0 = Vector.head v

ink

@[simp]

theorem Vector.head_ofFn {α : Type u_1} {n : ℕ} (f : Fin (Nat.succ n) → α) : Vector.head (Vector.ofFn f) = f 0

ink

theorem Vector.get_cons_zero {n : ℕ} {α : Type u_1} (a : α) (v : Vector α n) : Vector.get (a ::ᵥ v) 0 = a

ink

@[simp]

theorem Vector.get_cons_nil {α : Type u_1} {ix : Fin 1} (x : α) : Vector.get (x ::ᵥ Vector.nil) ix = x

Accessing the nth element of a vector made up of one element x : α is x itself.

ink

@[simp]

theorem Vector.get_cons_succ {n : ℕ} {α : Type u_1} (a : α) (v : Vector α n) (i : Fin n) : Vector.get (a ::ᵥ v) (Fin.succ i) = Vector.get v i

ink

def Vector.last {n : ℕ} {α : Type u_1} (v : Vector α (n + 1)) : α

The last element of a Vector, given that the vector is at least one element.

Equations

• Vector.last v = Vector.get v (Fin.last n)

ink

theorem Vector.last_def {n : ℕ} {α : Type u_1} {v : Vector α (n + 1)} : Vector.last v = Vector.get v (Fin.last n)

The last element of a Vector, given that the vector is at least one element.

ink

theorem Vector.reverse_get_zero {n : ℕ} {α : Type u_1} {v : Vector α (n + 1)} : Vector.head (Vector.reverse v) = Vector.last v

The last element of a vector is the head of the reverse vector.

ink

def Vector.scanl {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α n) : Vector β (n + 1)

Construct a Vector β (n + 1) from a Vector α n by scanning f : β → α → β→ α → β→ β from the "left", that is, from 0 to Fin.last n, using b : β as the starting value.

Equations

• Vector.scanl f b v = { val := List.scanl f b (Vector.toList v), property := (_ : List.length (List.scanl f b (Vector.toList v)) = n + 1) }

ink

@[simp]

theorem Vector.scanl_nil {α : Type u_2} {β : Type u_1} (f : β → α → β) (b : β) : Vector.scanl f b Vector.nil = b ::ᵥ Vector.nil

Providing an empty vector to scanl gives the starting value b : β.

ink

@[simp]

theorem Vector.scanl_cons {n : ℕ} {α : Type u_2} {β : Type u_1} (f : β → α → β) (b : β) (v : Vector α n) (x : α) : Vector.scanl f b (x ::ᵥ v) = b ::ᵥ Vector.scanl f (f b x) v

The recursive step of scanl splits a vector x ::ᵥ v : Vector α (n + 1) into the provided starting value b : β and the recursed scanl f b x : β as the starting value.

This lemma is the cons version of scanl_get.

ink

@[simp]

theorem Vector.scanl_val {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) {v : Vector α n} : ↑(Vector.scanl f b v) = List.scanl f b ↑v

The underlying List of a Vector after a scanl is the List.scanl of the underlying List of the original Vector.

ink

@[simp]

theorem Vector.toList_scanl {n : ℕ} {α : Type u_2} {β : Type u_1} (f : β → α → β) (b : β) (v : Vector α n) : Vector.toList (Vector.scanl f b v) = List.scanl f b (Vector.toList v)

The toList of a Vector after a scanl is the List.scanl of the toList of the original Vector.

ink

@[simp]

theorem Vector.scanl_singleton {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : Vector α 1) : Vector.scanl f b v = b ::ᵥ f b (Vector.head v) ::ᵥ Vector.nil

The recursive step of scanl splits a vector made up of a single element x ::ᵥ nil : Vector α 1 into a Vector of the provided starting value b : β and the mapped f b x : β as the last value.

ink

@[simp]

theorem Vector.scanl_head {n : ℕ} {α : Type u_2} {β : Type u_1} (f : β → α → β) (b : β) (v : Vector α n) : Vector.head (Vector.scanl f b v) = b

The first element of scanl of a vector v : Vector α n, retrieved via head, is the starting value b : β.

ink

@[simp]

theorem Vector.scanl_get {n : ℕ} {α : Type u_2} {β : Type u_1} (f : β → α → β) (b : β) (v : Vector α n) (i : Fin n) : Vector.get (Vector.scanl f b v) (Fin.succ i) = f (Vector.get (Vector.scanl f b v) (↑Fin.castSucc.toEmbedding i)) (Vector.get v i)

For an index i : Fin n, the nth element of scanl of a vector v : Vector α n at i.succ, is equal to the application function f : β → α → β→ α → β→ β of the castSucc i element of scanl f b v and get v i.

This lemma is the get version of scanl_cons.

ink

def Vector.mOfFn {m : Type u → Type u_1} [inst : Monad m] {α : Type u} {n : ℕ} : (Fin n → m α) → m (Vector α n)

Monadic analog of Vector.ofFn. Given a monadic function on fin n, return a Vector α n inside the monad.

Equations

• Vector.mOfFn x_2 = pure Vector.nil
• Vector.mOfFn f = do let a ← f 0 let v ← Vector.mOfFn fun i => f (Fin.succ i) pure (a ::ᵥ v)

ink

theorem Vector.mOfFn_pure {m : Type u_1 → Type u_2} [inst : Monad m] [inst : LawfulMonad m] {α : Type u_1} {n : ℕ} (f : Fin n → α) : (Vector.mOfFn fun i => pure (f i)) = pure (Vector.ofFn f)

ink

def Vector.mmap {m : Type u → Type u_1} [inst : Monad m] {α : Type u_2} {β : Type u} (f : α → m β) {n : ℕ} : Vector α n → m (Vector β n)

Apply a monadic function to each component of a vector, returning a vector inside the monad.

Equations

• Vector.mmap f x_2 = pure Vector.nil
• Vector.mmap f xs = do let h' ← f (Vector.head xs) let t' ← Vector.mmap f (Vector.tail xs) pure (h' ::ᵥ t')

ink

@[simp]

theorem Vector.mmap_nil {m : Type u_1 → Type u_2} [inst : Monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) : Vector.mmap f Vector.nil = pure Vector.nil

ink

@[simp]

theorem Vector.mmap_cons {m : Type u_1 → Type u_2} [inst : Monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) (a : α) {n : ℕ} (v : Vector α n) : Vector.mmap f (a ::ᵥ v) = do let h' ← f a let t' ← Vector.mmap f v pure (h' ::ᵥ t')

ink

def Vector.inductionOn {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_2} {n : ℕ} (v : Vector α n) (h_nil : C 0 Vector.nil) (h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C n w → C (Nat.succ n) (x ::ᵥ w)) : C n v

Define C v by induction on v : Vector α n.

This function has two arguments: h_nil handles the base case on C nil, and h_cons defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w)∀ x : α, C w → C (x ::ᵥ w)→ C (x ::ᵥ w).

This can be used as induction v using Vector.inductionOn.

Equations

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

ink

def Vector.inductionOn₂ {n : ℕ} {α : Type u_1} {β : Type u_2} {C : {n : ℕ} → Vector α n → Vector β n → Sort u_3} (v : Vector α n) (w : Vector β n) (nil : C 0 Vector.nil Vector.nil) (cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C n x y → C (Nat.succ n) (a ::ᵥ x) (b ::ᵥ y)) : C n v w

Define C v w by induction on a pair of vectors v : Vector α n and w : Vector β n.

Equations

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

ink

def Vector.inductionOn₃ {n : ℕ} {α : Type u_1} {β : Type u_2} {γ : Type u_3} {C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4} (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C 0 Vector.nil Vector.nil Vector.nil) (cons : {n : ℕ} → {a : α} → {b : β} → {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C n x y z → C (Nat.succ n) (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) : C n u v w

Define C u v w by induction on a triplet of vectors u : Vector α n, v : Vector β n, and w : Vector γ b.

Equations

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

ink

def Vector.toArray {n : ℕ} {α : Type u_1} : Vector α n → Array α

Cast a vector to an array.

Equations

• Vector.toArray x = match x with | { val := xs, property := property } => cast (_ : Array α = Array α) (List.toArray xs)

ink

def Vector.insertNth {n : ℕ} {α : Type u_1} (a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1)

v.insertNth a i inserts a into the vector v at position i (and shifting later components to the right).

Equations

• Vector.insertNth a i v = { val := List.insertNth (↑i) a ↑v, property := (_ : List.length (List.insertNth (↑i) a ↑v) = n + 1) }

ink

theorem Vector.insertNth_val {n : ℕ} {α : Type u_1} {a : α} {i : Fin (n + 1)} {v : Vector α n} : ↑(Vector.insertNth a i v) = List.insertNth (↑i) a ↑v

ink

@[simp]

theorem Vector.removeNth_val {n : ℕ} {α : Type u_1} {i : Fin n} {v : Vector α n} : ↑(Vector.removeNth i v) = List.removeNth ↑v ↑i

ink

theorem Vector.removeNth_insertNth {n : ℕ} {α : Type u_1} {a : α} {v : Vector α n} {i : Fin (n + 1)} : Vector.removeNth i (Vector.insertNth a i v) = v

ink

theorem Vector.removeNth_insertNth' {n : ℕ} {α : Type u_1} {a : α} {v : Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} : Vector.removeNth (↑(Fin.succAbove j).toEmbedding i) (Vector.insertNth a j v) = Vector.insertNth a (Fin.predAbove i j) (Vector.removeNth i v)

ink

theorem Vector.insertNth_comm {n : ℕ} {α : Type u_1} (a : α) (b : α) (i : Fin (n + 1)) (j : Fin (n + 1)) (h : i ≤ j) (v : Vector α n) : Vector.insertNth b (Fin.succ j) (Vector.insertNth a i v) = Vector.insertNth a (↑Fin.castSucc.toEmbedding i) (Vector.insertNth b j v)

ink

def Vector.set {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) : Vector α n

set v n a replaces the nth element of v with a

Equations

• Vector.set v i a = { val := List.set (↑v) (↑i) a, property := (_ : List.length (List.set (↑v) (↑i) a) = n) }

ink

@[simp]

theorem Vector.toList_set {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) : Vector.toList (Vector.set v i a) = List.set (Vector.toList v) (↑i) a

ink

@[simp]

theorem Vector.get_set_same {n : ℕ} {α : Type u_1} (v : Vector α n) (i : Fin n) (a : α) : Vector.get (Vector.set v i a) i = a

ink

theorem Vector.get_set_of_ne {n : ℕ} {α : Type u_1} {v : Vector α n} {i : Fin n} {j : Fin n} (h : i ≠ j) (a : α) : Vector.get (Vector.set v i a) j = Vector.get v j

ink

theorem Vector.get_set_eq_if {n : ℕ} {α : Type u_1} {v : Vector α n} {i : Fin n} {j : Fin n} (a : α) : Vector.get (Vector.set v i a) j = if i = j then a else Vector.get v j

ink

theorem Vector.sum_set {n : ℕ} {α : Type u_1} [inst : AddMonoid α] (v : Vector α n) (i : Fin n) (a : α) : List.sum (Vector.toList (Vector.set v i a)) = List.sum (Vector.toList (Vector.take (↑i) v)) + a + List.sum (Vector.toList (Vector.drop (↑i + 1) v))

ink

theorem Vector.prod_set {n : ℕ} {α : Type u_1} [inst : Monoid α] (v : Vector α n) (i : Fin n) (a : α) : List.prod (Vector.toList (Vector.set v i a)) = List.prod (Vector.toList (Vector.take (↑i) v)) * a * List.prod (Vector.toList (Vector.drop (↑i + 1) v))

ink

theorem Vector.sum_set' {n : ℕ} {α : Type u_1} [inst : AddCommGroup α] (v : Vector α n) (i : Fin n) (a : α) : List.sum (Vector.toList (Vector.set v i a)) = List.sum (Vector.toList v) + -Vector.get v i + a

ink

theorem Vector.prod_set' {n : ℕ} {α : Type u_1} [inst : CommGroup α] (v : Vector α n) (i : Fin n) (a : α) : List.prod (Vector.toList (Vector.set v i a)) = List.prod (Vector.toList v) * (Vector.get v i)⁻¹ * a

ink

def Vector.traverse {n : ℕ} {F : Type u → Type u} [inst : Applicative F] {α : Type u} {β : Type u} (f : α → F β) : Vector α n → F (Vector β n)

Apply an applicative function to each component of a vector.

Equations

• Vector.traverse f x = match x with | { val := v, property := Hv } => cast (_ : F (Vector β (List.length v)) = F (Vector β n)) (Vector.traverseAux f v)

ink

@[simp]

theorem Vector.traverse_def {n : ℕ} {F : Type u → Type u} [inst : Applicative F] {α : Type u} {β : Type u} (f : α → F β) (x : α) (xs : Vector α n) : Vector.traverse f (x ::ᵥ xs) = Seq.seq (Vector.cons <$> f x) fun x => Vector.traverse f xs

ink

theorem Vector.id_traverse {n : ℕ} {α : Type u} (x : Vector α n) : Vector.traverse pure x = x

ink

theorem Vector.comp_traverse {n : ℕ} {F : Type u → Type u} {G : Type u → Type u} [inst : Applicative F] [inst : Applicative G] [inst : LawfulApplicative G] {α : Type u} {β : Type u} {γ : Type u} (f : β → F γ) (g : α → G β) (x : Vector α n) : Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (Vector.traverse f <$> Vector.traverse g x)

ink

theorem Vector.traverse_eq_map_id {n : ℕ} {α : Type u_1} {β : Type u_1} (f : α → β) (x : Vector α n) : Vector.traverse (pure ∘ f) x = pure (Vector.map f x)

ink

theorem Vector.naturality {n : ℕ} {F : Type u → Type u} {G : Type u → Type u} [inst : Applicative F] [inst : Applicative G] [inst : LawfulApplicative F] [inst : LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u} {β : Type u} (f : α → F β) (x : Vector α n) : (fun {α} => ApplicativeTransformation.app η α) (Vector β n) (Vector.traverse f x) = Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) β ∘ f) x

ink

instance Vector.instTraversableFlipTypeNatVector {n : ℕ} : Traversable (flip Vector n)

Equations

• Vector.instTraversableFlipTypeNatVector = Traversable.mk (@Vector.traverse n)

ink

instance Vector.instIsLawfulTraversableFlipTypeNatVectorInstTraversableFlipTypeNatVector {n : ℕ} : IsLawfulTraversable (flip Vector n)

Equations

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