English
Induction principle for TransGen along a chain: to prove a predicate for any TransGen proof h : TransGen r a b, it suffices to prove it for the base case of a single r-step and to show closure under concatenation.
Русский
Принцип индукции по TransGen вдоль цепи: чтобы доказать свойство для любого доказательства h : TransGen r a b, достаточно доказать базовый случай одного шага и замкнуть по конкатенации.
LaTeX
$$$ ∀ {a b : α}, \mathrm{TransGen} r a b → \mathrm{Prop}, \\n (single : ∀ {a b} (h : r a b), motive (single h)) \\n (trans : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive (h₁.trans h₂)) \\n \rightarrow \text{motive } h $$$
Lean4
@[elab_as_elim]
theorem trans_induction_on {motive : ∀ {a b : α}, ReflTransGen r a b → Prop} {a b : α} (h : ReflTransGen r a b)
(refl : ∀ a, @motive a a refl) (single : ∀ {a b} (h : r a b), motive (single h))
(trans :
∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive (h₁.trans h₂)) :
motive h := by
induction h with
| refl => exact refl a
| tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)
