English
An induction principle for TransGen along the head: to prove a property for any h : TransGen r a b, it suffices to prove the base case for single steps and to show how to extend via head.
Русский
Принцип индукции по голове TransGen: чтобы доказать свойство для любого h : TransGen r a b, достаточно доказать базу для одиночного шага и показать, как продолжать через head.
LaTeX
$$$ {motive : \forall a b, TransGen r a b \to \mathrm{Prop}} {a b} (h : TransGen r a b), (single : \forall {a} (h : r a b), motive a (single h)) \\n (head : \forall {a c} (h' : r a c) (h : TransGen r c b), motive c h \\to motive a (h.head h')) : motive a h $$$
Lean4
@[elab_as_elim]
theorem head_induction_on {motive : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b)
(single : ∀ {a} (h : r a b), motive a (single h))
(head : ∀ {a c} (h' : r a c) (h : TransGen r c b), motive c h → motive a (h.head h')) : motive a h := by
induction h with
| single h => exact single h
| @tail b c _ hbc h_ih =>
apply h_ih
· exact fun h ↦ head h (.single hbc) (single hbc)
· exact fun hab hbc ↦ head hab _
