English
There exists a recursion principle for words: given a motive on Word M, a base case on empty and a step that appends a letter to the front, we obtain a function on all words respecting the motive.
Русский
Существует принцип рекурсии по словам: задан мотив на Word M, базовый случай на пустом слове и шаг, добавляющий букву вперед, задают функцию на всех словах, сохраняющую мотив.
LaTeX
$$$\\mathrm{consRecOn} : \\forall \\{motive : \\mathrm{Word} M \\to \\mathrm{Sort}^*\\}, \\mathrm{Word} M \\to \\mathrm{motive}(\\mathrm{empty}) \\\\to (\\forall i\\, m : M_i\\, w\\, h_1\\, h_2, \\mathrm{motive}\, w \\to \\mathrm{motive}(\\mathrm{cons}\; m\; w\; h_1\\; h_2)) \\to \\mathrm{motive}(w)$$$
Lean4
/-- Induct on a word by adding letters one at a time without reduction,
effectively inducting on the underlying `List`. -/
@[elab_as_elim]
def consRecOn {motive : Word M → Sort*} (w : Word M) (empty : motive empty)
(cons : ∀ (i) (m : M i) (w) h1 h2, motive w → motive (cons m w h1 h2)) : motive w :=
by
rcases w with ⟨w, h1, h2⟩
induction w with
| nil => exact empty
| cons m w
ih =>
refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
· rw [List.isChain_cons'] at h2
simp only [fstIdx, ne_eq, Option.map_eq_some_iff, Sigma.exists, exists_and_right, exists_eq_right, not_exists]
intro m' hm'
exact h2.1 _ hm' rfl
· exact h1 _ List.mem_cons_self
