mathlib3 documentation

data.vector.basic

Additional theorems and definitions about the vector type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def vector.inhabited {n : } {α : Type u_1} [inhabited α] :
Equations
@[ext]
theorem vector.ext {n : } {α : Type u_1} {v w : vector α n} (h : (m : fin n), v.nth m = w.nth m) :
v = w

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

def vector.replicate {α : Type u_1} (n : ) (a : α) :
vector α n

A vector with n elements a.

Equations
@[protected, instance]

The empty vector is a subsingleton.

@[simp]
theorem vector.cons_val {n : } {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).val = a :: v.val
@[simp]
theorem vector.cons_head {n : } {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).head = a
@[simp]
theorem vector.cons_tail {n : } {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).tail = v
theorem vector.eq_cons_iff {n : } {α : Type u_1} (a : α) (v : vector α n.succ) (v' : vector α n) :
v = a ::ᵥ v' v.head = a v.tail = v'
theorem vector.ne_cons_iff {n : } {α : Type u_1} (a : α) (v : vector α n.succ) (v' : vector α n) :
v a ::ᵥ v' v.head a v.tail v'
theorem vector.exists_eq_cons {n : } {α : Type u_1} (v : vector α n.succ) :
(a : α) (as : vector α n), v = a ::ᵥ as
@[simp]
theorem vector.to_list_of_fn {α : Type u_1} {n : } (f : fin n α) :
@[simp]
theorem vector.mk_to_list {n : } {α : Type u_1} (v : vector α n) (h : v.to_list.length = n) :
v.to_list, h⟩ = v
@[simp]
theorem vector.length_coe {n : } {α : Type u_1} (v : vector α n) :
@[simp]
theorem vector.to_list_map {n : } {α : Type u_1} {β : Type u_2} (v : vector α n) (f : α β) :
@[simp]
theorem vector.head_map {n : } {α : Type u_1} {β : Type u_2} (v : vector α (n + 1)) (f : α β) :
(vector.map f v).head = f v.head
@[simp]
theorem vector.tail_map {n : } {α : Type u_1} {β : Type u_2} (v : vector α (n + 1)) (f : α β) :
theorem vector.nth_eq_nth_le {n : } {α : Type u_1} (v : vector α n) (i : fin n) :
v.nth i = v.to_list.nth_le i.val _
@[simp]
theorem vector.nth_replicate {n : } {α : Type u_1} (a : α) (i : fin n) :
@[simp]
theorem vector.nth_map {n : } {α : Type u_1} {β : Type u_2} (v : vector α n) (f : α β) (i : fin n) :
(vector.map f v).nth i = f (v.nth i)
@[simp]
theorem vector.nth_of_fn {α : Type u_1} {n : } (f : fin n α) (i : fin n) :
(vector.of_fn f).nth i = f i
@[simp]
theorem vector.of_fn_nth {n : } {α : Type u_1} (v : vector α n) :
def equiv.vector_equiv_fin (α : Type u_1) (n : ) :
vector α n (fin n α)

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

Equations
theorem vector.nth_tail {n : } {α : Type u_1} (x : vector α n) (i : fin (n - 1)) :
x.tail.nth i = x.nth i.val + 1, _⟩
@[simp]
theorem vector.nth_tail_succ {n : } {α : Type u_1} (v : vector α n.succ) (i : fin n) :
v.tail.nth i = v.nth i.succ
@[simp]
theorem vector.tail_val {n : } {α : Type u_1} (v : vector α n.succ) :
@[simp]

The tail of a nil vector is nil.

@[simp]
theorem vector.singleton_tail {α : Type u_1} (v : vector α 1) :

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

@[simp]
theorem vector.tail_of_fn {α : Type u_1} {n : } (f : fin n.succ α) :
(vector.of_fn f).tail = vector.of_fn (λ (i : fin (n.succ - 1)), f i.succ)
@[simp]
theorem vector.to_list_empty {α : Type u_1} (v : vector α 0) :
@[simp]
theorem vector.to_list_singleton {α : Type u_1} (v : vector α 1) :

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

@[simp]
theorem vector.empty_to_list_eq_ff {n : } {α : Type u_1} (v : vector α (n + 1)) :
theorem vector.not_empty_to_list {n : } {α : Type u_1} (v : vector α (n + 1)) :
@[simp]
theorem vector.map_id {α : Type u_1} {n : } (v : vector α n) :

Mapping under id does not change a vector.

theorem vector.nodup_iff_nth_inj {n : } {α : Type u_1} {v : vector α n} :
theorem vector.head'_to_list {n : } {α : Type u_1} (v : vector α n.succ) :
def vector.reverse {n : } {α : Type u_1} (v : vector α n) :
vector α n

Reverse a vector.

Equations
theorem vector.to_list_reverse {n : } {α : Type u_1} {v : vector α n} :

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

@[simp]
theorem vector.reverse_reverse {n : } {α : Type u_1} {v : vector α n} :
@[simp]
theorem vector.nth_zero {n : } {α : Type u_1} (v : vector α n.succ) :
v.nth 0 = v.head
@[simp]
theorem vector.head_of_fn {α : Type u_1} {n : } (f : fin n.succ α) :
@[simp]
theorem vector.nth_cons_zero {n : } {α : Type u_1} (a : α) (v : vector α n) :
(a ::ᵥ v).nth 0 = a
@[simp]
theorem vector.nth_cons_nil {α : Type u_1} {ix : fin 1} (x : α) :

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

@[simp]
theorem vector.nth_cons_succ {n : } {α : Type u_1} (a : α) (v : vector α n) (i : fin n) :
(a ::ᵥ v).nth i.succ = v.nth i
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
theorem vector.last_def {n : } {α : Type u_1} {v : vector α (n + 1)} :
v.last = v.nth (fin.last n)

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

theorem vector.reverse_nth_zero {n : } {α : Type u_1} {v : vector α (n + 1)} :

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

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
@[simp]
theorem vector.scanl_nil {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) :

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

@[simp]
theorem vector.scanl_cons {n : } {α : Type u_1} {β : Type u_2} (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_nth.

@[simp]
theorem vector.scanl_val {n : } {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) {v : vector α n} :

The underlying list of a vector after a scanl is the list.scanl of the underlying list of the original vector.

@[simp]
theorem vector.to_list_scanl {n : } {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) (v : vector α n) :

The to_list of a vector after a scanl is the list.scanl of the to_list of the original vector.

@[simp]
theorem vector.scanl_singleton {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) (v : vector α 1) :

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.

@[simp]
theorem vector.scanl_head {n : } {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) (v : vector α n) :
(vector.scanl f b v).head = b

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

@[simp]
theorem vector.scanl_nth {n : } {α : Type u_1} {β : Type u_2} (f : β α β) (b : β) (v : vector α n) (i : fin n) :
(vector.scanl f b v).nth i.succ = f ((vector.scanl f b v).nth (fin.cast_succ i)) (v.nth 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 i.cast_succ element of scanl f b v and nth v i.

This lemma is the nth version of scanl_cons.

def vector.m_of_fn {m : Type u Type u_1} [monad m] {α : Type u} {n : } :
(fin n m α) m (vector α n)

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

Equations
theorem vector.m_of_fn_pure {m : Type u_1 Type u_2} [monad m] [is_lawful_monad m] {α : Type u_1} {n : } (f : fin n α) :
def vector.mmap {m : Type u Type u_1} [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
@[simp]
theorem vector.mmap_nil {m : Type u_1 Type u_2} [monad m] {α : Type u_3} {β : Type u_1} (f : α m β) :
@[simp]
theorem vector.mmap_cons {m : Type u_1 Type u_2} [monad m] {α : Type u_3} {β : Type u_1} (f : α m β) (a : α) {n : } (v : vector α n) :
vector.mmap f (a ::ᵥ v) = f a >>= λ (h' : β), vector.mmap f v >>= λ (t' : vector β n), has_pure.pure (h' ::ᵥ t')
def vector.induction_on {α : Type u_1} {C : Π {n : }, vector α n Sort u_2} {n : } (v : vector α n) (h_nil : C vector.nil) (h_cons : Π {n : } {x : α} {w : vector α n}, C w C (x ::ᵥ w)) :
C 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).

This can be used as induction v using vector.induction_on.

Equations
  • v.induction_on h_nil h_cons = nat.rec (λ (v : vector α 0), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on._proof_1), h_nil) _ _) (λ (v_val_hd : α) (v_val_tl : list α) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) (λ (n : ) (ih : Π (v : vector α n), C v) (v : vector α n.succ), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (v : list α) (v_property : (a :: v).length = n.succ), h_cons (ih v, _⟩)) v_property)) n v
def vector.induction_on₂ {n : } {α : Type u_1} {β : Type u_2} {C : Π {n : }, vector α n vector β n Sort u_3} (v : vector α n) (w : vector β n) (h_nil : C vector.nil vector.nil) (h_cons : Π {n : } {a : α} {b : β} {x : vector α n} {y : vector β n}, C x y C (a ::ᵥ x) (b ::ᵥ y)) :
C v w

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

Equations
  • v.induction_on₂ w h_nil h_cons = nat.rec (λ (v : vector α 0) (w : vector β 0), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on₂._proof_1), subtype.cases_on w (λ (w_val : list β) (w_property : w_val.length = 0), w_val.cases_on (λ (w_property : list.nil.length = 0), w_property.dcases_on (λ (a : 0 = 0) (H_2 : w_property == vector.induction_on₂._proof_2), h_nil) _ _) (λ (w_val_hd : β) (w_val_tl : list β) (w_property : (w_val_hd :: w_val_tl).length = 0), w_property.dcases_on (λ (a : 0 = (w_val_tl.length.add 0).succ), nat.no_confusion a) _ _) w_property)) _ _) (λ (v_val_hd : α) (v_val_tl : list α) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) (λ (n : ) (ih : Π (v : vector α n) (w : vector β n), C v w) (v : vector α n.succ) (w : vector β n.succ), subtype.cases_on v (λ (v_val : list α) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (v : list α) (v_property : (a :: v).length = n.succ), subtype.cases_on w (λ (w_val : list β) (w_property : w_val.length = n.succ), w_val.cases_on (λ (w_property : list.nil.length = n.succ), w_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (b : β) (w : list β) (w_property : (b :: w).length = n.succ), h_cons (ih v, _⟩ w, _⟩)) w_property)) v_property)) n v w
def vector.induction_on₃ {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) (h_nil : C vector.nil vector.nil vector.nil) (h_cons : Π {n : } {a : α} {b : β} {c : γ} {x : vector α n} {y : vector β n} {z : vector γ n}, C x y z C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
C 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
  • u.induction_on₃ v w h_nil h_cons = nat.rec (λ (u : vector α 0) (v : vector β 0) (w : vector γ 0), subtype.cases_on u (λ (u_val : list α) (u_property : u_val.length = 0), u_val.cases_on (λ (u_property : list.nil.length = 0), u_property.dcases_on (λ (a : 0 = 0) (H_2 : u_property == vector.induction_on₃._proof_1), subtype.cases_on v (λ (v_val : list β) (v_property : v_val.length = 0), v_val.cases_on (λ (v_property : list.nil.length = 0), v_property.dcases_on (λ (a : 0 = 0) (H_2 : v_property == vector.induction_on₃._proof_2), subtype.cases_on w (λ (w_val : list γ) (w_property : w_val.length = 0), w_val.cases_on (λ (w_property : list.nil.length = 0), w_property.dcases_on (λ (a : 0 = 0) (H_2 : w_property == vector.induction_on₃._proof_3), h_nil) _ _) (λ (w_val_hd : γ) (w_val_tl : list γ) (w_property : (w_val_hd :: w_val_tl).length = 0), w_property.dcases_on (λ (a : 0 = (w_val_tl.length.add 0).succ), nat.no_confusion a) _ _) w_property)) _ _) (λ (v_val_hd : β) (v_val_tl : list β) (v_property : (v_val_hd :: v_val_tl).length = 0), v_property.dcases_on (λ (a : 0 = (v_val_tl.length.add 0).succ), nat.no_confusion a) _ _) v_property)) _ _) (λ (u_val_hd : α) (u_val_tl : list α) (u_property : (u_val_hd :: u_val_tl).length = 0), u_property.dcases_on (λ (a : 0 = (u_val_tl.length.add 0).succ), nat.no_confusion a) _ _) u_property)) (λ (n : ) (ih : Π (u : vector α n) (v : vector β n) (w : vector γ n), C u v w) (u : vector α n.succ) (v : vector β n.succ) (w : vector γ n.succ), subtype.cases_on u (λ (u_val : list α) (u_property : u_val.length = n.succ), u_val.cases_on (λ (u_property : list.nil.length = n.succ), u_property.dcases_on (λ (a : n.succ = 0), nat.no_confusion a) _ _) (λ (a : α) (u : list α) (u_property : (a :: u).length = n.succ), subtype.cases_on v (λ (v_val : list β) (v_property : v_val.length = n.succ), v_val.cases_on (λ (v_property : list.nil.length = n.succ), v_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (b : β) (v : list β) (v_property : (b :: v).length = n.succ), subtype.cases_on w (λ (w_val : list γ) (w_property : w_val.length = n.succ), w_val.cases_on (λ (w_property : list.nil.length = n.succ), w_property.dcases_on (λ (a_1 : n.succ = 0), nat.no_confusion a_1) _ _) (λ (c : γ) (w : list γ) (w_property : (c :: w).length = n.succ), h_cons (ih u, _⟩ v, _⟩ w, _⟩)) w_property)) v_property)) u_property)) n u v w
def vector.to_array {n : } {α : Type u_1} :
vector α n array n α

Cast a vector to an array.

Equations
def vector.insert_nth {n : } {α : Type u_1} (a : α) (i : fin (n + 1)) (v : vector α n) :
vector α (n + 1)

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

Equations
theorem vector.insert_nth_val {n : } {α : Type u_1} {a : α} {i : fin (n + 1)} {v : vector α n} :
@[simp]
theorem vector.remove_nth_val {n : } {α : Type u_1} {i : fin n} {v : vector α n} :
theorem vector.remove_nth_insert_nth {n : } {α : Type u_1} {a : α} {v : vector α n} {i : fin (n + 1)} :
theorem vector.remove_nth_insert_nth' {n : } {α : Type u_1} {a : α} {v : vector α (n + 1)} {i : fin (n + 1)} {j : fin (n + 2)} :
theorem vector.insert_nth_comm {n : } {α : Type u_1} (a b : α) (i j : fin (n + 1)) (h : i j) (v : vector α n) :
def vector.update_nth {n : } {α : Type u_1} (v : vector α n) (i : fin n) (a : α) :
vector α n

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

Equations
@[simp]
theorem vector.to_list_update_nth {n : } {α : Type u_1} (v : vector α n) (i : fin n) (a : α) :
@[simp]
theorem vector.nth_update_nth_same {n : } {α : Type u_1} (v : vector α n) (i : fin n) (a : α) :
(v.update_nth i a).nth i = a
theorem vector.nth_update_nth_of_ne {n : } {α : Type u_1} {v : vector α n} {i j : fin n} (h : i j) (a : α) :
(v.update_nth i a).nth j = v.nth j
theorem vector.nth_update_nth_eq_if {n : } {α : Type u_1} {v : vector α n} {i j : fin n} (a : α) :
(v.update_nth i a).nth j = ite (i = j) a (v.nth j)
theorem vector.prod_update_nth {n : } {α : Type u_1} [monoid α] (v : vector α n) (i : fin n) (a : α) :
theorem vector.sum_update_nth {n : } {α : Type u_1} [add_monoid α] (v : vector α n) (i : fin n) (a : α) :
theorem vector.sum_update_nth' {n : } {α : Type u_1} [add_comm_group α] (v : vector α n) (i : fin n) (a : α) :
theorem vector.prod_update_nth' {n : } {α : Type u_1} [comm_group α] (v : vector α n) (i : fin n) (a : α) :
@[protected]
def vector.traverse {n : } {F : Type u Type u} [applicative F] {α β : Type u} (f : α F β) :
vector α n F (vector β n)

Apply an applicative function to each component of a vector.

Equations
@[protected, simp]
theorem vector.traverse_def {n : } {F : Type u Type u} [applicative F] {α β : Type u} (f : α F β) (x : α) (xs : vector α n) :
@[protected]
theorem vector.id_traverse {n : } {α : Type u} (x : vector α n) :
@[protected, nolint]
@[protected]
theorem vector.traverse_eq_map_id {n : } {α β : Type u_1} (f : α β) (x : vector α n) :
@[protected]
theorem vector.naturality {n : } {F G : Type u Type u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (f : α F β) (x : vector α n) :
@[protected, instance]
Equations
@[protected, instance]
meta def vector.reflect [reflected_univ] {α : Type u} [has_reflect α] [reflected (Type u) α] {n : } :