Induction starting from n=3 instead of n=1

Stream: Is there code for X?

[Vasily Ilin]

How can I use 0,1,2 as base cases here?

import Mathlib

example (f : ℕ → ℤ) (h0: f 1 = 1) (h1: f 2 = 5)
  (h : ∀ n > 2, f (n + 1) = f n + 2 * f (n - 1)) :
  ∀ n ≥ 1, f n = 2^n + (-1)^n := by
  intro n hn

[Riccardo Brasca]

Are you sure of the statement? h says "for all n bigger than 2 we have that f (n+1) = ..., in particular I don't see any assumption about f 3.

[Vasily Ilin]

I mean that I want to use 0,1,2 as base cases and n>2 as the inductive case

[Riccardo Brasca]

Anyway we have Nat.le_induction and friends for various induction principles.

[Riccardo Brasca]

Vasily Ilin said:

I mean that I want to use 0,1,2 as base cases and n>2 as the inductive case

My question is: are you sure the theorem is true, as stated?

[Vasily Ilin]

Yes, I found le_induction but didn't figure out how to use it. It just gave me the standard base case of 0

[Vasily Ilin]

I think it's true, yea. What's your concern?

[Riccardo Brasca]

How do you deduce something about f 3?

[Riccardo Brasca]

import Mathlib

def f : ℕ → ℤ
| 0 => 1
| 1 => 1
| 2 => 5
| 3 => 54
| n + 4 => f (n + 3) + 2 * f (n + 2)

example : (f 1 = 1) ∧ (f 2 = 5) ∧ (∀ n > 2, f (n + 1) = f n + 2 * f (n - 1))
    ∧ ¬(∀ n ≥ 1, f n = 2^n + (-1)^n) := by
  refine ⟨rfl, rfl, fun n hn ↦ ?_, ?_⟩
  · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hn
    rw [show 2 + k + 1 + 1 = k + 4 by omega, f]
    congrm f ?_ + 2 * f ?_ <;> omega
  · simp only [ge_iff_le, Int.reduceNeg, not_forall, Classical.not_imp]
    exact ⟨3, by decide, fun h ↦ by simp [f] at h⟩

shows it is false

[Vasily Ilin]

I might have made a small error somewhere in translating the statement. But I'm just asking about starting the proof, using not just n=0 as the base case but also 1 and 2

[Riccardo Brasca]

You can use Nat.le_induction or something around.

[Riccardo Brasca]

Here I don't think you need induction, so something like

example (f : ℕ → ℤ) (h0: f 1 = 1) (h1: f 2 = 5)
    (h : ∀ n > 2, f (n + 1) = f n + 2 * f (n - 1)) :
    ∀ n ≥ 1, f n = 2^n + (-1)^n
  | 0 => by omega
  | 1 => by simp [h0]
  | 2 => by simp [h1]
  | a+3 => by sorry

[Riccardo Brasca]

But again, it's really better to try to prove something true (maybe you want ∀ n ≥ 2 in h?).

[Riccardo Brasca]

In  Nat.le_induction you can write '(m := 37)' to start at 37.

[Riccardo Brasca]

Well, it's not even needed. Is

example (f : ℕ → ℤ) (h0: f 1 = 1) (h1: f 2 = 5)
    (h : ∀ n > 2, f (n + 1) = f n + 2 * f (n - 1)) :
    ∀ n ≥ 1, f n = 2^n + (-1)^n := by
  intro n hn
  induction n, hn using Nat.le_induction with
  | base => simp [h0]
  | succ a ha hf =>
    sorry

what are you looking for?

[Riccardo Brasca]

I think the difficulty here is that you want to:

• treat 0, 1, and 2 by hand
• use Nat.le_induction in the remaining cases

The best way is for sure to use match for the first three cases, and then use induction.

[Riccardo Brasca]

Or, even better, just use structural induction

[Riccardo Brasca]

I mean this

import Mathlib

lemma foo (f : ℕ → ℤ) (h0: f 1 = 1) (h1: f 2 = 5)
    (h : ∀ n ≥ 2, f (n + 1) = f n + 2 * f (n - 1)) :
    ∀ n ≥ 1, f n = 2^n + (-1)^n
| 0 => by omega
| 1 => by simp [h0]
| 2 => by simp [h1]
| a+3 => fun _ ↦ by
    rw [show a+3=a+2+1 by omega, h (a+2) (by omega), foo f h0 h1 h (a+2) (by omega),
      show a+2-1 = a+1 by omega, foo f h0 h1 h (a+1) (by omega)]
    ring

[Riccardo Brasca]

Note that:

• I've modified your h to h : ∀ n ≥ 2, f (n + 1) = f n + 2 * f (n - 1), with greater or equal, so the statement is true.
• when I say "structural induction" I mean I use foo in the proof of foo itself. Lean is smart enough to understand that I am proving something about a+3, so I can use the same for a+2 and a+1.

[Kyle Miller]

Some tips to complement Riccardo's:

One way to do induction from a later starting point is a pattern like

obtain _ | _ | n := n
· sorry -- case 0
· sorry -- case 1
induction n
· sorry -- case 2
· sorry -- induction step

Another is to use strong induction and put the cases inside

induction n using Nat.strongRecOn with
| _ n ih =>
  obtain _ | _ | _ | n := n
  · sorry -- case 0
  · sorry -- case 1
  · sorry -- case 2
  · sorry -- induction step

Strong induction subsumes the previous pattern.

Structural induction (what Riccardo suggests) is even more powerful. Lean will figure out which induction scheme you're using automatically.

[Vasily Ilin]

Thank you, both. I ended up with this:

example (f : ℕ → ℤ) (h0: f 1 = 1) (h1: f 2 = 5)
  (h : ∀ n ≥ 2, f (n + 1) = f n + 2 * f (n - 1)) :
  ∀ n ≥ 1, f n = 2^n + (-1)^n := by
  intro n hn
  induction n using Nat.strongRecOn with
  | _ n ih =>
    obtain _ | _ | _ | n := n
    · omega -- case 0
    · simp [h0] -- case 1
    · simp [h1] -- case 2
    · simp [h, ih]
      ring