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

@[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 : n) :
(a::ᵥv).val = a :: v.val
@[simp]
theorem vector.cons_head {n : } {α : Type u_1} (a : α) (v : n) :
(a::ᵥv).head = a
@[simp]
theorem vector.cons_tail {n : } {α : Type u_1} (a : α) (v : 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 : 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 : n) (f : α → β) :
theorem vector.nth_eq_nth_le {n : } {α : Type u_1} (v : 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 : n) (f : α → β) (i : fin n) :
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 : n) :
= v
@[simp]
theorem vector.nth_tail {n : } {α : Type u_1} (v : n.succ) (i : fin n) :
v.tail.nth i = v.nth i.succ
@[simp]
theorem vector.tail_val {n : } {α : Type u_1} (v : 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 : 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 : 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 : n) :
= v

Mapping under id does not change a vector.

theorem vector.mem_iff_nth {n : } {α : Type u_1} {a : α} {v : n} :
a v.to_list ∃ (i : fin n), v.nth i = a
theorem vector.nodup_iff_nth_inj {n : } {α : Type u_1} {v : n} :
@[simp]
theorem vector.nth_mem {n : } {α : Type u_1} (i : fin n) (v : n) :
theorem vector.head'_to_list {n : } {α : Type u_1} (v : n.succ) :
def vector.reverse {n : } {α : Type u_1} (v : n) :
n
Equations
theorem vector.to_list_reverse {n : } {α : Type u_1} {v : 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 : 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 : 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 : n) (i : fin n) :
(a::ᵥv).nth i.succ = v.nth i
def vector.last {n : } {α : Type u_1} (v : (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 : (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 : (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 : n) :
(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 : n) (x : α) :
b (x::ᵥv) = b::ᵥ (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 : n} :
b v).val = b v.val

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 : n) :
b v).to_list = b v.to_list

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 : 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 : n) :
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 : n) (i : fin n) :
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 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] {α : 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 : } :
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 : n) :
(a::ᵥv) = f a >>= λ (h' : β), v >>= λ (t' : n), pure (h'::ᵥt')
def vector.induction_on {α : Type u_1} {n : } {C : Π {n : }, nSort u_2} (v : (n + 1)) (h0 : C vector.nil) (hs : Π {n : } {x : α} {w : 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} :
n α
Equations
def vector.insert_nth {n : } {α : Type u_1} (a : α) (i : fin (n + 1)) (v : n) :
(n + 1)
Equations
theorem vector.insert_nth_val {n : } {α : Type u_1} {a : α} {i : fin (n + 1)} {v : n} :
v).val = v.val
@[simp]
theorem vector.remove_nth_val {n : } {α : Type u_1} {i : fin n} {v : n} :
theorem vector.remove_nth_insert_nth {n : } {α : Type u_1} {a : α} {v : n} {i : fin (n + 1)} :
v) = v
theorem vector.remove_nth_insert_nth' {n : } {α : Type u_1} {a : α} {v : (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 : n) :
v) = v)
def vector.update_nth {n : } {α : Type u_1} (v : n) (i : fin n) (a : α) :
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 : 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 : 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 : 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 : α → F β) :
nF (vector β n)
Equations
• v, Hv⟩ = cast _ (traverse_aux f v)
@[simp]
theorem vector.traverse_def {n : } {F : Type uType u} [applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : n) :
(x::ᵥxs) = <*> xs
theorem vector.id_traverse {n : } {α : Type u} (x : n) :
theorem vector.comp_traverse {n : } {F G : Type uType u} [applicative F] [applicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : n) :
x =
theorem vector.traverse_eq_map_id {n : } {α β : Type u_1} (f : α → β) (x : n) :
x = id.mk x)
theorem vector.naturality {n : } {F G : Type uType u} [applicative F] [applicative G] (η : G) {α β : Type u} (f : α → F β) (x : n) :
η x) = vector.traverse (η f) x
@[instance]
Equations