Skip to main content

Challenge 14: For all n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴

Also available in:

Español

Prove that, for all \(n \in ℕ\), \(2n + 9 ≤ 2^{n+4}\).

To do so, complete the following Lean 4 theory:

import Mathlib.Tactic

variable (n : ℕ)

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by sorry

1. Proof in natural language

By induction on \(n\).

Base case: for \(n = 0\) we have: \[ \begin{array}{ll} 2 \times 0 + 9 &= 9 \\ &≤ 16 \\ &= 2^{0+4} \end{array} \]

Inductive step: assuming the induction hypothesis \[ 2k + 9 ≤ 2^{k+4} \tag{IH} \] we have to prove that \[ 2(k+1) + 9 ≤ 2^{(k+1)+4} \]

Since \(k \geq 0\), we have \[ 2 ≤ 2^{k+4} \tag{1} \] Indeed, \[ \begin{array}{ll} 2 &≤ 16 \\ &= 2^{4} \\ &≤ 2^{k+4} \end{array} \]

Finally, \[ \begin{array}{llll} 2(k + 1) + 9 &= (2k + 9) + 2 \\ &≤ 2^{k+4} + 2 &&\text{[by IH]} \\ &≤ 2^{k+4} + 2^{k+4} &&\text{[by (1)]} \\ &= 2 \times 2^{k+4} \\ &= 2^{(k+1)+4} \end{array} \]

2. Proofs in Lean 4

import Mathlib.Tactic

variable (n : ℕ)

-- Proof 1
-- =======

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4)
    grind
  | succ k HI =>
    -- k : ℕ
    -- HI : 2 * k + 9 ≤ 2 ^ (k + 4)
    -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4)
    grind

-- Proof 2
-- =======

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by
  induction n <;> grind

-- Proof 3
-- =======

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4)
    grind
  | succ k HI =>
    -- k : ℕ
    -- HI : 2 * k + 9 ≤ 2 ^ (k + 4)
    -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4)
    calc 2 * (k + 1) + 9
         = (2 * k + 9) + 2           := by grind
    _    ≤ 2 ^ (k + 4) + 2           := by grind
    _    ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := by grind
    _    = 2 * 2 ^ (k + 4)           := by grind
    _    = 2 ^ (k + 1 + 4)           := by grind

-- Proof 4
-- =======

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4)
    norm_num
  | succ k HI =>
    -- k : ℕ
    -- HI : 2 * k + 9 ≤ 2 ^ (k + 4)
    -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4)
    calc 2 * (k + 1) + 9
         = (2 * k + 9) + 2           := by ring
    _    ≤ 2 ^ (k + 4) + 2           := Nat.add_le_add_right HI 2
    _    ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := Nat.add_le_add_left (by bound) (2 ^ (k + 4))
    _    = 2 * 2 ^ (k + 4)           := by ring
    _    = 2 ^ (k + 1 + 4)           := by ring

-- Proof 5
-- =======

example : 2 * n + 9 ≤ 2 ^ (n + 4) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * 0 + 9 ≤ 2 ^ (0 + 4)
    calc 2 * 0 + 9
         = 9           := by norm_num
    _    ≤ 16          := by norm_num
    _    = 2 ^ (0 + 4) := by norm_num
  | succ k HI =>
    -- k : ℕ
    -- HI : 2 * k + 9 ≤ 2 ^ (k + 4)
    -- ⊢ 2 * (k + 1) + 9 ≤ 2 ^ (k + 1 + 4)
    have h1 : 2 ≤ 2 ^ (k + 4) := by
      calc 2
           ≤ 16          := by norm_num
      _    = 2 ^ 4       := by norm_num
      _    ≤ 2 ^ (k + 4) := Nat.pow_le_pow_of_le one_lt_two (Nat.le_add_left 4 k)
    calc 2 * (k + 1) + 9
         = (2 * k + 2) + 9           := congrArg (· + 9) (Nat.mul_succ 2 k)
    _    = (2 * k + 9) + 2           := Nat.add_right_comm (2 * k) 2 9
    _    ≤ 2 ^ (k + 4) + 2           := Nat.add_le_add_right HI 2
    _    ≤ 2 ^ (k + 4) + 2 ^ (k + 4) := Nat.add_le_add_left h1 (2 ^ (k + 4))
    _    = 2 * 2 ^ (k + 4)           := (Nat.two_mul (2 ^ (k + 4))).symm
    _    = 2 ^ (k + 1 + 4)           := Nat.pow_succ'.symm


-- Lemmas used
-- ===========

variable (k m : ℕ)
#check (Nat.add_le_add_left : n ≤ m → ∀ k, k + n ≤ k + m)
#check (Nat.add_le_add_right : n ≤ m → ∀ k, n + k ≤ m + k)
#check (Nat.add_left_inj : m + n = k + n ↔ m = k)
#check (Nat.le_add_left n m : n ≤ m + n)
#check (Nat.pow_succ' : m ^ n.succ = m * m ^ n)
#check (Nat.two_mul n : 2 * n = n + n)
#check (one_le_two : 1 ≤ 2)
#check (pow_le_pow_right'  : 1 ≤ k → n ≤ m → k ^ n ≤ k ^ m)

The following video explains step by step how the solutions are built:

You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.

3. Collaborative solutions

Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:

  • Write your proof in live.lean-lang.org and check that it compiles without errors.
  • Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean
   -- your proof
```

Comments