English
Define a function C on vectors by induction on their length: C(v) is determined by the base case for nil and an inductive step for x ::ᵥ w using C w.
Русский
Определить функцию C на векторах по индукции по их длине: базовый случай для nil и шаг индукции для x ::ᵥ w через C w.
LaTeX
$$$\\mathrm{inductionOn} : \\forall C, C\\;\\mathrm{nil} \\to (\\forall {n} {x} {w}, C w \\to C (x ::ᵥ w)) \\to C v$$$
Lean4
/-- Define `C v` by induction on `v : Vector α n`.
This function has two arguments: `nil` handles the base case on `C nil`,
and `cons` defines the inductive step using `∀ x : α, C w → C (x ::ᵥ w)`.
It is used as the default induction principle for the `induction` tactic.
-/
@[elab_as_elim, induction_eliminator]
def inductionOn {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n) (nil : C nil)
(cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : C v := by
induction n with
| zero =>
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
exact nil
| succ n ih =>
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
cases v_property
exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)
