2
$\begingroup$

When trying to solve this example from "The Mechanics of Proof":

def a : ℕ → ℤ
  | 0 => 2
  | 1 => 1
  | n + 2 => a (n + 1) + 2 * a n

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
  two_step_induction n with k IH1 IH2
  . calc a 0 = 2 := by rw [a]
      _ = 2 ^ 0 + (-1) ^ 0 := by numbers
  . calc a 1 = 1 := by rw [a]
      _ = 2 ^ 1 + (-1) ^ 1 := by numbers
  calc
    a (k + 2)
      = a (k + 1) + 2 * a k := by rw [a]
    _ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [IH1, IH2]
    _ = (2 : ℤ) ^ (k + 2) + (-1) ^ (k + 2) := by ring

using only Mathlib, I am struggling to obtain the inductive hypothesis for the 2nd induction step. For now I have

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
  induction n with
  | zero => simp [a]; rfl
  | succ k ik => cases k with
    | zero => simp [a]; rfl
    | succ k => calc
        a (k + 2) = a (k + 1) + 2 * a k := rfl
        _ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik]; sorry
        _ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring

But here I only have one inductive hypothesis. Where would I get the other hypothesis (in the example above, we have ih1 and ih2) from?

$\endgroup$
1

1 Answer 1

2
$\begingroup$

You can put induction principle Nat.twoStepInduction into the induction' tactic. (The norm_num tactic is a good replacement for the numbers tactic in Mechanics of Proof, although as you noticed, rfl also works in this case.)

import Mathlib

def a : ℕ → ℤ
  | 0 => 2
  | 1 => 1
  | n + 2 => a (n + 1) + 2 * a n

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
  induction' n using Nat.twoStepInduction with k IH1 IH2
  . calc a 0 = 2 := by rw [a]
      _ = 2 ^ 0 + (-1) ^ 0 := by rfl  -- or norm_num
  . calc a 1 = 1 := by rw [a]
      _ = 2 ^ 1 + (-1) ^ 1 := by rfl  -- or norm_num
  . calc
      a (k + 2)
        = a (k + 1) + 2 * a k := by rw [a]
      _ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [IH1, IH2]
      _ = (2 : ℤ) ^ (k + 2) + (-1) ^ (k + 2) := by ring

You can also use Nat.twoStepInduction with the built in induction tactic as follows:

example (n : ℕ) : a n = 2 ^ n + (-1) ^ n := by
  induction n using Nat.twoStepInduction
  . rfl
  . rfl
  . case _ k ik1 ik2 => calc
    a (k + 2) = a (k + 1) + 2 * a k := rfl
    _ = (2 ^ (k + 1) + (-1) ^ (k + 1)) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik1, ik2] 
    _ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring

I found the induction principle Nat.twoStepInduction via moogle.ai.


To see why you need Nat.twoStepInduction, this is how you would prove it with normal induction. Notice we are not proving the original statement by induction, but instead the conjunction of both the n and n+1 cases at the same time! That gives us the necessary induction hypotheses to do the induction, and it is what the induction principle Nat.twoStepInduction automates.

example (n : Nat) : a n = 2 ^ n + (-1) ^ n := by
  -- prove the `n` and `n+1` cases simultaneously by induction
  have aux_lemma :
      a n = 2 ^ n + (-1) ^ n /\
      a (n + 1) = 2 ^ (n + 1) + (-1) ^ (n + 1) := by
    induction n with
    | zero =>
      constructor
      . rfl
      . rfl
    | succ k ik =>
      constructor
      . exact ik.2
      . calc
        a (k + 2) = a (k + 1) + 2 * (a k) := rfl
        _ = 2 ^ (k + 1) + (-1) ^ (k + 1) + 2 * (2 ^ k + (-1) ^ k) := by rw [ik.1, ik.2]
        _ = 2 ^ (k + 2) + (-1) ^ (k + 2) := by ring

  -- we just need the `n` case in the end
  exact aux_lemma.1
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.