English
There exists a reverse induction principle on vectors: for any property C on Vector α n, if C nil holds and for all xs and x, C xs → C (xs.snoc x), then C v holds for every v.
Русский
Существует принцип индукции по обратной стороне на векторах: для любого свойства C на Vector α n, если C nil выполняется и для всех xs и x, C xs → C (xs.snoc x), то C v выполняется для каждого v.
LaTeX
$$$\forall C:\, {n:\mathbb{N}} \to Vector\ α\ n \to Prop,\ C\ nil \land (\forall {n} {xs:Vector\ α\ n} {x:α}, C xs \to C (xs.snoc x))\Rightarrow C v$$$
Lean4
/-- 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`. -/
@[elab_as_elim]
def revInductionOn {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n) (nil : C nil)
(snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α), C xs → C (xs.snoc x)) : C v :=
cast (by simp) <|
inductionOn (C := fun v => C v.reverse) v.reverse nil
(@fun n x xs (r : C xs.reverse) => cast (by simp) <| snoc xs.reverse x r)
