English
The standard induction principle on FreeMonoid: to prove a property for all elements, prove it for 1 and show that it is preserved by multiplication on the left by generators.
Русский
Стандартный принцип индукции по FreeMonoid: чтобы доказать свойство для всех элементов, докажите сначала для 1 и покажите, что свойство сохраняется при умножении слева на образцы.
LaTeX
$$$\\\\forall p : FreeMonoid α \\to Prop, p(1) \\\\to (\\\\forall x, p(x) \\to p(of x)) \\\\to \\forall z, p(z)$$$
Lean4
/-- An induction principle for free monoids which mirrors induction on lists, with cases analogous
to the empty list and cons -/
@[to_additive (attr := elab_as_elim) /-- An induction principle for free monoids which mirrors
induction on lists, with cases analogous to the empty list and cons -/
]
protected theorem inductionOn' {p : FreeMonoid α → Prop} (a : FreeMonoid α) (one : p (1 : FreeMonoid α))
(mul_of : ∀ b a, p a → p (of b * a)) : p a :=
List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a
