data.vector2 - mathlib docs

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 = ⟨list.scanl f b v.to_list, _⟩

source

@[simp]

theorem vector.scanl_nil {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) :

vector.scanl f b vector.nil = b::ᵥ vector.nil

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

source

@[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.

source

@[simp]

theorem vector.scanl_val {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) {v : vector α n} :

(vector.scanl f b v).val = list.scanl f b v.val

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

source

@[simp]

theorem vector.to_list_scanl {n : ℕ} {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α n) :

(vector.scanl f b v).to_list = list.scanl f 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.

source

@[simp]

theorem vector.scanl_singleton {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (v : vector α 1) :

vector.scanl f b v = b::ᵥf b v.head::ᵥ 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.

source

@[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 : β.

source

@[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.

source

def vector.m_of_fn {m : Type u → Type u_1} [monad m] {α : Type u} {n : ℕ} :

(fin n → m α) → m (vector α n)

Equations

vector.m_of_fn f = f 0 >>= λ (a : α), vector.m_of_fn (λ (i : fin n), f i.succ) >>= λ (v : vector α n), pure (a::ᵥv)
vector.m_of_fn f = pure vector.nil

source

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 → α) :

vector.m_of_fn (λ (i : fin n), pure (f i)) = pure (vector.of_fn f)

source

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

vector α n → m (vector β n)

Equations

vector.mmap f xs = f xs.head >>= λ (h' : β), vector.mmap f xs.tail >>= λ (t' : vector β n), pure (h'::ᵥt')
vector.mmap f xs = pure vector.nil

source

@[simp]

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

vector.mmap f vector.nil = pure vector.nil

source

@[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), pure (h'::ᵥt')

source

def vector.induction_on {α : Type u_1} {n : ℕ} {C : Π {n : ℕ}, vector α n → Sort u_2} (v : vector α (n + 1)) (h0 : C vector.nil) (hs : Π {n : ℕ} {x : α} {w : vector α n}, C w → C (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

v.induction_on h0 hs = nat.rec (λ (v : vector α (0 + 1)), _.mpr (_.mpr (hs h0))) (λ (n : ℕ) (hn : Π (v : vector α (n + 1)), C v) (v : vector α (n.succ + 1)), _.mpr (hs (hn v.tail))) n v

source

def vector.to_array {n : ℕ} {α : Type u_1} :

vector α n → array n α

Equations

vector.to_array ⟨xs, h⟩ = cast _ xs.to_array

source

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

vector α (n + 1)

Equations

vector.insert_nth a i v = ⟨list.insert_nth ↑i a v.val, _⟩

source

theorem vector.insert_nth_val {n : ℕ} {α : Type u_1} {a : α} {i : fin (n + 1)} {v : vector α n} :

(vector.insert_nth a i v).val = list.insert_nth i.val a v.val

source

@[simp]

theorem vector.remove_nth_val {n : ℕ} {α : Type u_1} {i : fin n} {v : vector α n} :

(vector.remove_nth i v).val = v.val.remove_nth ↑i

source

theorem vector.remove_nth_insert_nth {n : ℕ} {α : Type u_1} {a : α} {v : vector α n} {i : fin (n + 1)} :

vector.remove_nth i (vector.insert_nth a i v) = v

source

theorem vector.remove_nth_insert_nth' {n : ℕ} {α : Type u_1} {a : α} {v : vector α (n + 1)} {i : fin (n + 1)} {j : fin (n + 2)} :

vector.remove_nth (⇑(j.succ_above) i) (vector.insert_nth a j v) = vector.insert_nth a (i.pred_above j) (vector.remove_nth i v)

source

theorem vector.insert_nth_comm {n : ℕ} {α : Type u_1} (a b : α) (i j : fin (n + 1)) (h : i ≤ j) (v : vector α n) :

vector.insert_nth b j.succ (vector.insert_nth a i v) = vector.insert_nth a (⇑fin.cast_succ i) (vector.insert_nth b j v)

source

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

v.update_nth i a = ⟨v.val.update_nth i.val a, _⟩

source

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

source

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

source

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)

source

@[protected]

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

vector α n → F (vector β n)

Equations

vector.traverse f ⟨v, Hv⟩ = cast _ (traverse_aux f v)

source

@[protected, simp]

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

vector.traverse f (x::ᵥxs) = vector.cons <$> f x <*> vector.traverse f xs

source

@[protected]

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

vector.traverse id.mk x = x

source

@[protected]

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