Induction on the Natural Numbers

Induction on the Natural Numbers

In the previous entry of Babel, we wrote the natural numbers as an inductively defined type in Lean modelling the approach of Peano. On top of this structure we used pattern matching to write recursive definitions of addition and multiplication on this type. Key aspects of this code are repeated here to serve as a reminder of what was written. All of the library code on the natural numbers can be found here.

inductive ℕ where
  | zero : ℕ
  | succ : ℕ → ℕ

theorem succ_not_zero :
  ∀ x : ℕ, succ x ≠ zero :=
  by
    intro m
    intro h₁
    injection h₁

theorem succ_injective :
  ∀ m n : ℕ, succ m = succ n → m = n :=
  by
    intro m n
    intro h₁
    injection h₁

def add (m n : ℕ) : ℕ :=
  match n with
    | zero    => m
    | succ x  => succ (add m x)

def mul (m n : ℕ) : ℕ :=
  match n with
    | zero    => zero
    | succ x  => (mul m x) + m

 theorem add_zero :
  ∀ x : ℕ, x + zero = x :=
    by
      intro x
      rfl

 theorem add_succ :
  ∀ x y : ℕ, x + succ y = succ (x + y) :=
    by
      intro x y
      rfl

 theorem mul_zero :
  ∀ x : ℕ, x * zero = zero :=
    by
      intro x
      rfl

 theorem mul_succ :
  ∀ x y : ℕ, x * succ y = x * y + x :=
  by
    intro x y
    rfl

Our first theorems hardly deserve the title. They follow merely by computing additions and multiplications, or the details of them are hidden in the properties of inductively defined types. At the end of the previous entry, we saw a theorem that was a statement about something other than mere computation. Indeed, the tactic rfl did not fit the goal. Other theorems require the use of the induction axiom (schema). This does not need to be written by us, as all inductively defined types come built in with their own induction schema! Therefore the final axiom of Peano arithmetic is already available to us.

Induction

As an axiom (schema) of first-order logic, induction for an arbitrary unary predicate $P$, can be stated as follows:

\[[P(0) \land \forall x : ℕ, \ (P(x) \to P(succ \ x))] \rightarrow \forall y : ℕ, \ P(y)\]

This is an implication, whose antecedent is a conjunction of a proof that the predicate is true at 0 and a proof that for each natural number $x$, a proof of $P(x)$ allows for the construction of a proof of $P(succ \ x)$. The consequent of this implication is that the predicate must then be true at all natural numbers.

 theorem zero_add :
  ∀ x : ℕ, zero + x = x :=
    by
      intro x
      ...

Therefore, in order to prove this theorem, it is sufficient to use the induction schema of the inductively defined type of the natural numbers. Code that follows gives a template for such a proof by induction on the natural numbers. Comments (indicated by --) are added to show where the base case and induction step fit into the template.

 theorem zero_add :
  ∀ x : ℕ, zero + x = x :=
    by
      intro x
      induction x with
      -- Base case
      | zero      => ...
      -- Induction step
      | succ x ih => ...

Base Case

We are required to replace the … in the line zero => ... with a proof of the base case. This is the case that x = zero and therefore the claim of the base case is zero + zero = zero. There are a number of ways to close this goal, however this, again, is true by computation. For this reason it suffices to use rfl.

Induction Step

We are required to replace the … in the line succ x ih => ... with a proof of the equation zero + succ x = succ x. However, we have a proof ih - the induction hypothesis - of the equation zero + x = x to make use of in the proof.

theorem zero_add_induction (t : zero + x = x) :
   zero + succ x = succ x :=
    by
      ...

Notice that in order to use this theorem, one must supply a proof of the equation zero + x = x. Proofs are programs and hypotheses in proofs are the inputs of the corresponding program. Although the induction hypothesis is not immediately applicable - there is no instance of zero + x = x in the goal.

1 goal
x : ℕ
t : zero + x = x
⊢ zero + succ x = succ x

At this point we need to make use of another theorem before we are able to apply the induction hypothesis. As the righthand term in the sum is a successor, we can apply add_succ to act on the equation. That is, there is a step of computation to carry out. We use a tactic rw (read as “rewrite”) to apply theorems and hypotheses to the goal.

theorem zero_add_induction (t : zero + x = x) :
   zero + succ x = succ x :=
    by
      rw [add_succ]

This step of computaton updates the goal to a state in which the induction hypothesis can be applied.

1 goal
x : ℕ
t : zero + x = x
⊢ succ (zero + x) = succ x

Hypotheses are applied to the goal in the same manner as theorems, with the use of rw tactic. Furthermore, they can be nested inside the same brackets so long as they are separated by commas.

theorem zero_add_induction (t : zero + x = x) :
   zero + succ x = succ x :=
    by
      rw [add_succ,t]

Bringing it all together

Taking these steps together in the template for induction proofs, one writes:

 theorem zero_add :
  ∀ x : ℕ, zero + x = x :=
    by
      intro x
      induction x with
      | zero      => rfl
      | succ x ih => exact (zero_add_induction ih)

We are rewarded with the glorious No goals.

Comments on Steps of the Proof

• In the induction step we used add_succ to rewrite the goal. Notice that even though add_succ is a universally quantified statement, Lean was able to infer the correct instantiation of it to apply the relevant equation to the goal.

• Indeed, Lean is able to infer a lot. This inference means we don’t have to explicitly type every term, which clarifies the code significantly.

• As good as the type inference is, there have been times where Lean has not inferred the type I wanted and so explicit typing was necessary.

• It is not necessary to write a separate theorem for the induction step. One can simply write rw [add_succ,ih] in place of the function call. I chose to do it this way to highlight the fact that proofs are programs and hence can be called in other proofs… programs!

• All induction proofs follow this template.

Further Theorems on ℕ

rfl, induction, rw are sufficient for writing proofs for the following theorems. Have at it!

theorem zero_add :
  ∀ x : ℕ, zero + x = x := sorry

 theorem succ_add :
  ∀ x y : ℕ, (succ x) + y = succ (x + y) := sorry

 theorem add_assoc :
  ∀ x y z : ℕ, (x + y) + z = x + (y + z) := sorry

 theorem add_comm :
  ∀ x y : ℕ, x + y = y + x := sorry

 theorem add_left_cancel :
  ∀ x y z : ℕ, x + y = x + z → y = z := sorry

  theorem add_right_cancel :
  ∀ x y z : ℕ, y + x = z + x → y = z := sorry

 theorem mul_zero :
  ∀ x : ℕ, x * zero = zero := sorry

 theorem mul_succ :
  ∀ x y : ℕ, x * succ y = x * y + x := sorry

 theorem zero_mul :
  ∀ x : ℕ, zero * x = zero := sorry

 theorem succ_mul :
  ∀ x y : ℕ, (succ x) * y = (x * y) + y := sorry

 theorem mul_distl_add :
  ∀ x y z : ℕ, x * (y + z) = (x * y) + (x * z) := sorry

 theorem mul_assoc :
  ∀ x y z : ℕ, (x * y) * z = x * (y * z) := sorry

 theorem mul_comm :
  ∀ x y : ℕ, x * y = y * x := sorry

 theorem mul_distr_add :
  ∀ x y z : ℕ, (y + z) * x = (y * x) + (z * x) := sorry

In the next entry of Babel I will define some of the jargon related to proof assistants. In future entries I will write about the calc tactic, before explaining how I defined the integers in Lean.

Acknowledgments and Code

I came to terms with this content by playing the Natural Number Game, reading Theorem Proving in Lean 4, browsing Mathlib, and asking questions on Proof Assistants Stack Exchange. Thank you to everyone involved in each of those projects.

All of the code covered in this entry of Babel can be found here on my GitHub account.