English
To prove a property for every RelSeries, it suffices to prove it for singletons and show that if it holds for a series p, it also holds for p.cons x hx. This provides an induction principle akin to structural induction on RelSeries.
Русский
Чтобы доказать свойство для любой RelSeries, достаточно доказать его для одиночных элементов и показать, что если свойство верно для p, то верно и для p.cons x hx. Это принцип структурного индукции на RelSeries.
LaTeX
$$@[elab_as_elim]\ninductionOn (motive) (singleton) (cons) (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` prepended with one element.
Note: This can also be used to construct data, but it does not have good definitional properties,
since `(p.cons x hx).tail _ = p` is not a definitional equality.
-/
@[elab_as_elim]
def inductionOn (motive : RelSeries r → Sort*) (singleton : (x : α) → motive (RelSeries.singleton r x))
(cons : (p : RelSeries r) → (x : α) → (hx : x ~[r] p.head) → (hp : motive p) → motive (p.cons 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 lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
nth_rw 3 [heq] at lq
convert cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩) (hd _ lq)
exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm
exact this rfl
