21 - Simple Induction

Induction is a powerful idea that can dramatically simplify some proofs that would otherwise be quite hairy.

Here we'll see how simple induction can unlock a not-so-simple task.

Task

Prove the following is true for every natural number $n$,

$$2^n\ge n+1$$

It is not immediately obvious how to do this in our head. 

Maths

Let's introduce the idea of induction. To prove a proposition $P$ is true for any natural number n, we need to show two things:

• Base case: $P$ is true for $n=0$.
• Inductive step: $P$ true for $n$ implies $P$ true for $(n+1)$.

The following illustrates how these two things together allow us to prove $P(n)$ is true for all n. We can see why some describe induction as knocking over dominoes.

For our task, let $P(n)$ be the proposition $2^n\ge n+1$. We need to show both the base case and the inductive step.

The base case $P(0)$ is the proposition $2^0\ge 0+1$. Because $2^0=1\ge 1$, the base case $P(0)$ is true.

The inductive step is the implication $P(n)⟹P(n+1)$. To prove this implication, we assume $P(n)$ is true and derive $P(n+1)$. That is, we assume $2^n\ge n+1$ and derive $2^{n+1}\ge (n+1)+1$.

• Let's start with $2^{n+1}=2\cdot 2^n$.
• By assumption $2^n\ge n+1$, so $2\cdot 2^n\ge 2\cdot (n+1)$.
• Expanding $2\cdot (n+1)=(n+1)+n+1$ lets us see $(n+1)+n+1\ge (n+1)+1$. This is because $n$ can't be negative.
• Putting all this together, we have $2^{n+1}\ge (n+1)+1$.

In the inductive step, the assumption that $P(n)$ is true is called the induction hypothesis.

We have shown the base case $P(0)$ and the inductive step $P(n)⟹P(n+1)$ are true, and so, by induction, we can say $P(n)$ is true for all natural numbers $n$.

Let's write this out in a form that takes us towards a Lean proof.

$$\begin{array}{rlrl}P(n):2^n& \ge n+1& & \text{proof objective}\\ & & & \\ \text{base case }P(0)& & & \\ & & & \\ 2^0& =1& & \\ & \ge 0+1& & \text{so }P(0)\text{ is true}\\ & & & \\ \text{inductive step }P(n)& ⟹P(n+1)& & \\ & & & \\ \text{(1)}& P(n):2^n& \ge n+1& & \text{induction hypothesis}& & & \\ 2^{n+1}& =2\cdot 2^n& & \\ & \ge 2\cdot (n+1)& & \text{by }(\text{1})\\ & =(n+1)+1+n& & \\ & \ge (n+1)+1& & \text{so }P(n+1)\text{ is true}\\ & & & \\ ◻& P(n):2^n& \ge n+1& & \text{by induction}\end{array}$$

Code

The following Lean program proves, by induction, that $2^n\ge n+1$ for all natural numbers $n$.

-- 21 - Simple Induction

import Mathlib.Tactic

example {n : ℕ} : 2^n ≥ n + 1 := by
  induction n with
  | zero =>
    norm_num
  | succ n ih =>
    calc
      2^(n + 1) = 2 * 2^n := by ring
      _ ≥ 2 * (n + 1) := by rel [ih]
      _ = (n + 1) + 1 + n := by ring
      _ ≥ (n + 1) + 1 := by norm_num

The proof header is as we'd expect, but the rest of the proof has a structure we've not seen before.

The induction is started using induction n with which tells Lean we want to do induction on the variable n. We need to specify the variable because some tasks may have more than one variable.

After that we have two sections, starting with | zero => for the base case, and | succ n ih => for the inductive step.

• The code indented under | zero => is the proof of the base case 2 ^ 0 ≥ 0 + 1, which here can be resolved by norm_num.
• The code indented under | succ n ih => is the proof of the inductive step 2 ^ (n + 1) ≥ n + 1 + 1, which here requires a calc section. The inductive hypothesis is established as ih.

Infoview

Placing the cursor before induction n with shows the original proof goal.

⊢ 2 ^ n ≥ n + 1

Moving the cursor to the start of the next line | zero => shows the goal for the base case.

⊢ 2 ^ 0 ≥ 0 + 1

Placing the curser just before | succ n ih => shows the goal for the inductive step, and also the inductive hypothesis ih.

ih : 2 ^ n ≥ n + 1
⊢ 2 ^ (n + 1) ≥ n + 1 + 1

---

Exercise

Write a Lean program to prove, by induction, that

$$3^n\ge n+1$$

for any natural number $n$.