What is wrong with my formalization?

Stream: new members

[Thuc Hoang]

I am trying to formalize a theorem about recursive function as below.

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

example (n : ℕ) (h1 : n ≠ 0) : g n = 2^n + (-1: ℤ)^n := by
    induction' n using Nat.strongRecOn with k IH
    rw [IH]

However I get stuck here and get this proof state, which seems to be a contradiction.

**k** : ℕ
**IH** : ∀ m < k, m ≠ 0 → g m = 2 ^ m + (-1) ^ m
**h1** : k ≠ 0
**⊢** k < k

What's wrong with my formalization?

[Daniel Weber]

rw can be non-reversible when you use something with preconditions, like IH here - you're trying to apply the induction hypothesis to g k, so it's asking you to prove k < k, as that's the precondition for it

[Daniel Weber]

You should also change g to

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

as then the patterns don't intersect, which is easier to work with

[Thuc Hoang]

Thanks for the suggestion. I follow your advice and get stuck at this step.

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

example (n : ℕ) (h1 : n ≠ 0) : g n = 2^n + (-1: ℤ)^n := by
    match n with
    | 0 => exact False.elim (h1 rfl)
    | 1 => simp [g]
    | 2 => simp [g]
    | n+3 =>
        simp [g]
        sorry

I want to replace the definition of g (n + 2) + 2 * g (n + 1) in the goal but don't know how to do it. Do you have any hints/suggestion how I should move forward?

[Ilmārs Cīrulis]

One should use induction here, I believe.

[Ilmārs Cīrulis]

I will try to make example.

[Daniel Weber]

If you use a theorem/lemma instead of an example you can simply rewrite using it

[Ilmārs Cīrulis]

Wow, indeed.

import Mathlib

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

theorem THM (n : ℕ) (h1 : n ≠ 0) : g n = 2^n + (-1: ℤ)^n := by
    match n with
    | 0 => exact False.elim (h1 rfl)
    | 1 => simp [g]
    | 2 => simp [g]
    | n+3 =>
        simp [g]
        rw [THM, THM]
        . ring
        . omega
        . omega

[Kevin Buzzard]

Your life would be much easier if you defined g 0 to be 2 and then you wouldn't have to go as far as n + 3 in the definition and the problem would not have arisen at all (and you would not need to exclude the case n = 0 either)