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 List.Vector.snoc {α : Type u_1} {n : ℕ} : Vector α n → α → Vector α (n + 1)

Append a single element to the end of a vector

Equations

• xs.snoc x = xs ++ x ::ᵥ List.Vector.nil

Simplification lemmas

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Reverse induction principle

def List.Vector.revInductionOn {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_5} {n : ℕ} (v : Vector α n) (nil : C nil) (snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)) : C 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.

Equations

• v.revInductionOn nil snoc = cast ⋯ (v.reverse.inductionOn nil fun (n : ℕ) (x : α) (xs : List.Vector α n) (r : C xs.reverse) => cast ⋯ (snoc xs.reverse x r))

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

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

Equations

• One or more equations did not get rendered due to their size.

def List.Vector.revCasesOn {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_5} {n : ℕ} (v : Vector α n) (nil : C nil) (snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C (xs.snoc x)) : C v

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

Equations

• v.revCasesOn nil snoc = v.revInductionOn nil fun {n : ℕ} (xs : List.Vector α n) (x : α) (x_1 : C xs) => snoc xs x

More simplification lemmas

@[simp]

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

@[simp]

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

@[simp]

theorem List.Vector.mapAccumr_snoc {α : Type u_1} {β : Type u_2} {σ : Type u_3} {n : ℕ} {x : α} (xs : Vector α n) {f : α → σ → σ × β} {s : σ} : mapAccumr f (xs.snoc x) s = have q := f x s; have r := mapAccumr f xs q.1; (r.1, r.2.snoc q.2)

@[simp]

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

@[simp]

theorem List.Vector.mapAccumr₂_nil {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {s : σ} {f : α → β → σ → σ × φ} : mapAccumr₂ f nil nil s = (s, nil)

@[simp]

theorem List.Vector.mapAccumr₂_snoc {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {n : ℕ} {s : σ} (xs : Vector α n) (ys : Vector β n) (f : α → β → σ → σ × φ) (x : α) (y : β) : mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = have q := f x y s; have r := mapAccumr₂ f xs ys q.1; (r.1, r.2.snoc q.2)