Documentation

Mathlib.Data.Vector.Snoc

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

Append a single element to the end of a vector

Equations
  • xs.snoc x = xs.append (x ::ᵥ Mathlib.Vector.nil)
Instances For

    Simplification lemmas #

    @[simp]
    theorem Mathlib.Vector.snoc_cons {α : Type u_1} {n : } (xs : Mathlib.Vector α n) {x : α} {y : α} :
    (x ::ᵥ xs).snoc y = x ::ᵥ xs.snoc y
    @[simp]
    theorem Mathlib.Vector.snoc_nil :
    ∀ {α : Type u_1} {x : α}, Mathlib.Vector.nil.snoc x = x ::ᵥ Mathlib.Vector.nil
    @[simp]
    theorem Mathlib.Vector.reverse_cons {α : Type u_1} {n : } (xs : Mathlib.Vector α n) {x : α} :
    (x ::ᵥ xs).reverse = xs.reverse.snoc x
    @[simp]
    theorem Mathlib.Vector.reverse_snoc {α : Type u_1} {n : } (xs : Mathlib.Vector α n) {x : α} :
    (xs.snoc x).reverse = x ::ᵥ xs.reverse
    theorem Mathlib.Vector.replicate_succ_to_snoc {α : Type u_1} {n : } (val : α) :

    Reverse induction principle #

    def Mathlib.Vector.revInductionOn {α : Type u_2} {C : {n : } → Mathlib.Vector α nSort u_1} {n : } (v : Mathlib.Vector α n) (nil : C Mathlib.Vector.nil) (snoc : {n : } → (xs : Mathlib.Vector α n) → (x : α) → C xsC (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 : Mathlib.Vector α n) (r : C xs.reverse) => cast (snoc xs.reverse x r))
    Instances For
      def Mathlib.Vector.revInductionOn₂ {α : Type u_2} {β : Type u_3} {C : {n : } → Mathlib.Vector α nMathlib.Vector β nSort u_1} {n : } (v : Mathlib.Vector α n) (w : Mathlib.Vector β n) (nil : C Mathlib.Vector.nil Mathlib.Vector.nil) (snoc : {n : } → (xs : Mathlib.Vector α n) → (ys : Mathlib.Vector β n) → (x : α) → (y : β) → C xs ysC (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.
      Instances For
        def Mathlib.Vector.revCasesOn {α : Type u_2} {C : {n : } → Mathlib.Vector α nSort u_1} {n : } (v : Mathlib.Vector α n) (nil : C Mathlib.Vector.nil) (snoc : {n : } → (xs : Mathlib.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 : Mathlib.Vector α n) (x : α) (x_1 : C xs) => snoc xs x
        Instances For

          More simplification lemmas #

          @[simp]
          theorem Mathlib.Vector.map_snoc {α : Type u_2} {n : } (xs : Mathlib.Vector α n) :
          ∀ {α_1 : Type u_1} {f : αα_1} {x : α}, Mathlib.Vector.map f (xs.snoc x) = (Mathlib.Vector.map f xs).snoc (f x)
          @[simp]
          theorem Mathlib.Vector.mapAccumr_nil :
          ∀ {α : Type u_1} {α_1 : Type} {β : Type u_2} {f : αα_1α_1 × β} {s : α_1}, Mathlib.Vector.mapAccumr f Mathlib.Vector.nil s = (s, Mathlib.Vector.nil)
          @[simp]
          theorem Mathlib.Vector.mapAccumr_snoc {α : Type u_2} {n : } (xs : Mathlib.Vector α n) :
          ∀ {α_1 : Type} {β : Type u_1} {f : αα_1α_1 × β} {x : α} {s : α_1}, Mathlib.Vector.mapAccumr f (xs.snoc x) s = let q := f x s; let r := Mathlib.Vector.mapAccumr f xs q.1; (r.1, r.2.snoc q.2)
          @[simp]
          theorem Mathlib.Vector.map₂_snoc {α : Type u_2} {n : } {β : Type u_3} (xs : Mathlib.Vector α n) (ys : Mathlib.Vector β n) :
          ∀ {α_1 : Type u_1} {f : αβα_1} {x : α} {y : β}, Mathlib.Vector.map₂ f (xs.snoc x) (ys.snoc y) = (Mathlib.Vector.map₂ f xs ys).snoc (f x y)
          @[simp]
          theorem Mathlib.Vector.mapAccumr₂_nil :
          ∀ {α β α_1 β_1 : Type} {f : αβα_1α_1 × β_1} {s : α_1}, Mathlib.Vector.mapAccumr₂ f Mathlib.Vector.nil Mathlib.Vector.nil s = (s, Mathlib.Vector.nil)
          @[simp]
          theorem Mathlib.Vector.mapAccumr₂_snoc {α : Type} {n : } {β : Type} (xs : Mathlib.Vector α n) (ys : Mathlib.Vector β n) {σ : Type} {φ : Type} {c : σ} (f : αβσσ × φ) (x : α) (y : β) :
          Mathlib.Vector.mapAccumr₂ f (xs.snoc x) (ys.snoc y) c = let q := f x y c; let r := Mathlib.Vector.mapAccumr₂ f xs ys q.1; (r.1, r.2.snoc q.2)