English
An induction principle along the head of a ReflTransGen chain: to prove a property for all pairs (a,b) with ReflTransGen r a b, it suffices to prove it for the reflexive base and to show it is preserved when extending the chain by a head step.
Русский
Принцип индукции по голове цепи ReflTransGen: чтобы доказать свойство для всех пар (a,b) с ReflTransGen r a b, достаточно доказать его для рефлексивной основы и показать сохранение при добавлении головы к цепочке.
LaTeX
$$$ ∀ {α} {r : α → α → Prop} {b : α} {motive : (a : α) → \mathrm{ReflTransGen} r a b → \mathrm{Prop}} (h : \mathrm{ReflTransGen} r a b),\n (refl : ∀ a, motive a a \text{ refl}) → (head : ∀ {a c} (h' : r a c) (h : \mathrm{ReflTransGen} r c b), motive c h → motive a (h.head h')) → motive a h $$$
Lean4
@[elab_as_elim]
theorem head_induction_on {motive : ∀ a : α, ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b)
(refl : motive b refl) (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a (h.head h')) :
motive a h := by
induction h with
| refl => exact refl
| @tail b c _ hbc ih =>
apply ih
· exact head hbc _ refl
· exact fun h1 h2 ↦ head h1 (h2.tail hbc)
