English
A refined induction principle: to prove a property for RelSeries one may use a motive, a singleton witness, and a snoc step; the construction provides a proof for any p.
Русский
Уточнённый принцип индукции: чтобы доказать свойство для RelSeries, можно использовать мотивацию, базовый случай и шаг snoc.
LaTeX
$$InductionOn' (motive) (singleton) (snoc) (p) : motive p$$
Lean4
/-- To show a proposition `p` for `xs : RelSeries r` it suffices to show it for all singletons
and to show that when `p` holds for `xs` it also holds for `xs` appended with one element.
-/
@[elab_as_elim]
def inductionOn' (motive : RelSeries r → Sort*) (singleton : (x : α) → motive (RelSeries.singleton r x))
(snoc : (p : RelSeries r) → (x : α) → (hx : p.last ~[r] x) → (hp : motive p) → motive (p.snoc x hx))
(p : RelSeries r) : motive p :=
by
let this {n : ℕ} (heq : p.length = n) : motive p := by
induction n generalizing p with
| zero =>
convert singleton p.head
ext n
· exact heq
· simp [show n = 0 by cutsat, apply_zero]
| succ d hd =>
have ne0 : p.length ≠ 0 := by simp [heq]
have len : p.eraseLast.length = d := by simp [heq]
convert snoc p.eraseLast p.last (p.eraseLast_last_rel_last ne0) (hd _ len)
exact (p.snoc_self_eraseLast ne0).symm
exact this rfl
