Induction (Lean)

Definition

Induction (Lean)

In Lean, the tactic induction applies the induction principle of an inductive type. For a natural number and a statement , it implements proof by induction:

The zero case proves the starting claim. The successor case assumes the claim at and proves it at .

Syntax and goals

For a goal P n:

induction n with
| zero => sorry
| succ k ih => sorry

Branch	Available hypothesis	Goal
zero	—	P 0
succ k ih	ih : P k	P (k + 1)

k names the predecessor. ih names the induction hypothesis; neither name is a keyword. sorry marks an unfinished proof. Induction creates proof obligations; it does not establish them automatically.

What is being assumed?

The induction hypothesis concerns the entire statement chosen for induction.

• For , it is .
• For , it is .

In the second case, you may choose any input . Applying ih t supplies a proof of P k t. This is still induction on , not induction on .

Whether another variable is fixed or universally quantified matters. See generalising induction for the effect of intro placement and generalizing.

Example

Positivity of an Ackermann row

This statement keeps the second input universally quantified during induction:

theorem Ackermann_positive (x : ℕ) :
    ∀ (y : ℕ), 0 < Ackermann x y := by
  induction x with
  | zero =>
      intro y
      sorry
  | succ k ih =>
      intro y
      sorry

In the successor branch, ih : ∀ t, 0 < Ackermann k t. It describes the whole previous row. intro y then chooses an arbitrary input for the current row; it does not restrict the inputs accepted by ih.