This file establishes a snoc : Vector α n → α → Vector α (n+1) operation, that appends a single element to the back of a vector.

It provides a collection of lemmas that show how different Vector operations reduce when their argument is snoc xs x.

Also, an alternative, reverse, induction principle is added, that breaks down a vector into snoc xs x for its inductive case. Effectively doing induction from right-to-left

def Vector.snoc {α : Type u_1} {n : ℕ} : Vector α n → α → Vector α (n + 1)

Append a single element to the end of a vector

Simplification lemmas

@[simp]

theorem Vector.snoc_cons {α : Type u_1} {n : ℕ} (xs : Vector α n) {x : α} {y : α} : Vector.snoc (x ::ᵥ xs) y = x ::ᵥ Vector.snoc xs y

@[simp]

theorem Vector.snoc_nil : ∀ {α : Type u_1} {x : α}, Vector.snoc Vector.nil x = x ::ᵥ Vector.nil

@[simp]

theorem Vector.reverse_cons {α : Type u_1} {n : ℕ} (xs : Vector α n) {x : α} : Vector.reverse (x ::ᵥ xs) = Vector.snoc (Vector.reverse xs) x

@[simp]

theorem Vector.reverse_snoc {α : Type u_1} {n : ℕ} (xs : Vector α n) {x : α} : Vector.reverse (Vector.snoc xs x) = x ::ᵥ Vector.reverse xs

theorem Vector.replicate_succ_to_snoc {α : Type u_1} {n : ℕ} (val : α) : Vector.replicate (n + 1) val = Vector.snoc (Vector.replicate n val) val

Reverse induction principle

def Vector.revInductionOn {α : Type u_2} {C : {n : ℕ} → Vector α n → Sort u_1} {n : ℕ} (v : Vector α n) (nil : C 0 Vector.nil) (snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C n xs → C (n + 1) (Vector.snoc xs x)) : C n v

Define C v by reverse induction on v : Vector α n. That is, break the vector down starting from the right-most element, using snoc

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

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

def Vector.revInductionOn₂ {α : Type u_2} {β : Type u_3} {C : {n : ℕ} → Vector α n → Vector β n → Sort u_1} {n : ℕ} (v : Vector α n) (w : Vector β n) (nil : C 0 Vector.nil Vector.nil) (snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C n xs ys → C (n + 1) (Vector.snoc xs x) (Vector.snoc ys y)) : C n v w

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

def Vector.revCasesOn {α : Type u_2} {C : {n : ℕ} → Vector α n → Sort u_1} {n : ℕ} (v : Vector α n) (nil : C 0 Vector.nil) (snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C (n + 1) (Vector.snoc xs x)) : C n v

Define C v by reverse case analysis, i.e. by handling the cases nil and xs.snoc x separately

More simplification lemmas

@[simp]

theorem Vector.map_snoc {α : Type u_2} {n : ℕ} (xs : Vector α n) : ∀ {α : Type u_1} {f : α → α} {x : α}, Vector.map f (Vector.snoc xs x) = Vector.snoc (Vector.map f xs) (f x)

@[simp]

theorem Vector.mapAccumr_nil : ∀ {α : Type u_1} {α_1 : Type} {β : Type u_2} {f : α → α_1 → α_1 × β} {s : α_1}, Vector.mapAccumr f Vector.nil s = (s, Vector.nil)

@[simp]

theorem Vector.mapAccumr_snoc {α : Type u_2} {n : ℕ} (xs : Vector α n) : ∀ {α : Type} {β : Type u_1} {f : α → α → α × β} {x : α} {s : α}, Vector.mapAccumr f (Vector.snoc xs x) s = let q := f x s; let r := Vector.mapAccumr f xs q.fst; (r.fst, Vector.snoc r.snd q.snd)

@[simp]

theorem Vector.map₂_snoc {α : Type u_2} {n : ℕ} {β : Type u_3} (xs : Vector α n) (ys : Vector β n) : ∀ {α : Type u_1} {f : α → β → α} {x : α} {y : β}, Vector.map₂ f (Vector.snoc xs x) (Vector.snoc ys y) = Vector.snoc (Vector.map₂ f xs ys) (f x y)

@[simp]

theorem Vector.mapAccumr₂_nil : ∀ {α β α_1 β_1 : Type} {f : α → β → α_1 → α_1 × β_1} {s : α_1}, Vector.mapAccumr₂ f Vector.nil Vector.nil s = (s, Vector.nil)

@[simp]

theorem Vector.mapAccumr₂_snoc {α : Type} {n : ℕ} {β : Type} (xs : Vector α n) (ys : Vector β n) {σ : Type} {φ : Type} {c : σ} (f : α → β → σ → σ × φ) (x : α) (y : β) : Vector.mapAccumr₂ f (Vector.snoc xs x) (Vector.snoc ys y) c = let q := f x y c; let r := Vector.mapAccumr₂ f xs ys q.fst; (r.fst, Vector.snoc r.snd q.snd)