mathlib documentation

data.vector2

Additional theorems about the vector type

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

@[instance]
def vector.inhabited {n : } {α : Type u_1} [inhabited α] :

Equations
@[ext]
theorem vector.ext {n : } {α : Type u_1} {v w : vector α n} :
(∀ (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.

@[instance]
def vector.zero_subsingleton {α : Type u_1} :

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

@[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.to_list_map {n : } {α : Type u_1} {β : Type u_2} (v : vector α n) (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_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) :

@[simp]
theorem vector.nth_tail {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]
theorem vector.tail_nil {α : Type u_1} :

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_singleton {α : Type u_1} (v : vector α 1) :
v.to_list = [v.head]

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.map_id {α : Type u_1} {n : } (v : vector α n) :

Mapping under id does not change a vector.

theorem vector.mem_iff_nth {n : } {α : Type u_1} {a : α} {v : vector α n} :
a v.to_list ∃ (i : fin n), v.nth i = a

theorem vector.nodup_iff_nth_inj {n : } {α : Type u_1} {v : vector α n} :

@[simp]
theorem vector.nth_mem {n : } {α : Type u_1} (i : fin n) (v : vector α n) :

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

def vector.reverse {n : } {α : Type u_1} :
vector α nvector α n

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.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} :
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} :
(β → α → β)β → vector α nvector β (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 i.cast_succ) (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 uType u_1} [monad m] {α : Type u} {n : } :
(fin nm α)m (vector α n)

Equations
theorem vector.m_of_fn_pure {m : Type u_1Type u_2} [monad m] [is_lawful_monad m] {α : Type u_1} {n : } (f : fin n → α) :
vector.m_of_fn (λ (i : fin n), pure (f i)) = pure (vector.of_fn f)

def vector.mmap {m : Type uType u_1} [monad m] {α : Type u_2} {β : Type u} (f : α → m β) {n : } :
vector α nm (vector β n)

Equations
@[simp]
theorem vector.mmap_nil {m : Type u_1Type u_2} [monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) :

@[simp]
theorem vector.mmap_cons {m : Type u_1Type 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), pure (h'::ᵥt')

def vector.induction_on {α : Type u_1} {n : } {C : Π {n : }, vector α nSort u_2} (v : vector α (n + 1)) :
C vector.nil(Π {n : } {x : α} {w : vector α n}, C wC (x::ᵥw))C v

Define C v by induction on v : vector α (n + 1), a vector of at least one element. This function has two arguments: h0 handles the base case on C nil, and hs defines the inductive step using ∀ x : α, C v → C (x ::ᵥ v).

Equations
def vector.to_array {n : } {α : Type u_1} :
vector α narray n α

Equations
def vector.insert_nth {n : } {α : Type u_1} :
α → fin (n + 1)vector α nvector α (n + 1)

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_ne {n : } {α : Type u_1} {a : α} {v : vector α (n + 1)} {i j : fin (n + 2)} (h : i j) :

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} :
vector α nfin nα → vector α n

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

Equations
@[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)

def vector.traverse {n : } {F : Type uType u} [applicative F] {α β : Type u} :
(α → F β)vector α nF (vector β n)

Equations
@[simp]
theorem vector.traverse_def {n : } {F : Type uType u} [applicative F] [is_lawful_applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : vector α n) :

theorem vector.id_traverse {n : } {α : Type u} (x : vector α n) :

theorem vector.comp_traverse {n : } {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : vector α n) :

theorem vector.traverse_eq_map_id {n : } {α β : Type u_1} (f : α → β) (x : vector α n) :

theorem vector.naturality {n : } {F G : Type uType u} [applicative F] [applicative G] [is_lawful_applicative F] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (f : α → F β) (x : vector α n) :

@[instance]

Equations