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
Simplification lemmas #
Reverse induction principle #
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
.
Instances For
Define C v w
by reverse induction on a pair of vectors v : Vector α n
and
w : Vector β n
.
Instances For
Define C v
by reverse case analysis, i.e. by handling the cases nil
and xs.snoc x
separately