Counting & logic

The induction principle

State the principle itself as a theorem, with a base case and a step supplied as arguments.

-- Top 100 #74: The induction principle
-- History: 1321 · Levi ben Gerson milestone.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The step proves an implication for every n, rather than checking a long finite list.
-- Scope: Proves natural-number induction for every predicate P using Lean’s inductive eliminator.
-- Source: https://lurch.plus/100/

theorem induction_principle (P : Nat → Prop)
    (base : P 0) (step : ∀ n, P n → P (n+1)) :
    ∀ n, P n := by
  intro n
  induction n with
  | zero => exact base
  | succ n ih => exact step n ih

-- A simple application: adding zero preserves n.
example : ∀ n : Nat, n+0 = n := by
  apply induction_principle
  · rfl
  · intro n _
    rfl

Explanation

`P : Nat → Prop`

A predicate assigns a proposition to each natural number. The theorem proves P n for every n from its base and successor cases.

`base · step`

base proves P 0. step takes a natural number n and a proof of P n, then produces a proof of P (n + 1).

`induction n with · ih`

Splits the proof into zero and successor cases. In the successor case, ih proves P n, so step n ih proves the next case.

Background and proof scope

1321 · Levi ben Gerson milestone

The step proves an implication for every n, rather than checking a long finite list.

Proves natural-number induction for every predicate P using Lean’s inductive eliminator.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Identify the type of ih in the successor case. Why is it exactly what step needs?