induction (cleanly) for this recurrence

Stream: new members

[Nathan]

import Mathlib.Data.Int.Init

example (f : ℤ → ℤ) (f0 : f 0 = 1) (f1 : f 1 = 2)
    (r : ∀ x, f x = 2 * f (x - 1) - f (x - 2) + 2) :
    ∀ x, f x = x * x + 1 := by
  sorry

How can I prove this cleanly with induction? I only need positive values, so the goal can be changed to ∀ x, x ≥ 0 → f x = x * x + 1 or ∀ x : ℕ, f x = x * x + 1 if it makes the proof easier.

I tried doing it with Nat.strong_induction_on but I had trouble casting between ints and nats. So I started to wonder if casting could be avoided.

[Aaron Liu]

here's my attempt

import Mathlib.Data.Int.Init

example (f : ℤ → ℤ) (f0 : f 0 = 1) (f1 : f 1 = 2)
    (r : ∀ x, f x = 2 * f (x - 1) - f (x - 2) + 2) :
    ∀ x : ℕ, f x = x * x + 1 := by
  intro x
  induction x using Nat.strongRecOn with | ind n ih
  cases n with
  | zero => simpa using f0
  | succ n =>
    cases n with
    | zero => simpa using f1
    | succ n => grind

[Nathan]

thanks

[Jakub Nowak]

There's also Int.strongRec:

import Mathlib.Data.Int.Init

example (f : ℤ → ℤ) (f0 : f 0 = 1) (f1 : f 1 = 2)
    (r : ∀ x, f x = 2 * f (x - 1) - f (x - 2) + 2) :
    ∀ x, 0 ≤ x → f x = x * x + 1 := by
  intro x
  induction x using Int.strongRec (m := 0) with
  | lt n hn => grind
  | ge n hn ih => grind

[Jakub Nowak]

It would be nice to have strong version of Int.inductionOn', this would be useful here to prove this for all x, not just positive.

[Nathan]

oh, looks like this one is avoiding the casting

[Nathan]

i'm never sure what syntax to use for induction, is there a reference?

[Nathan]

like for example, i wouldn't have known how to do (m := 0)

[Nathan]

what if you did want to prove it for all x, how could you do it?

[Jakub Nowak]

Nathan said:

like for example, i wouldn't have known how to do (m := 0)

This syntax is not specific to induction. m is an argument of Int.strongRec and I've used (m := 0) to set this argument. If you don't set this argument, then Lean won't be able to deduce what it should be in this case. If you check the context under the comment in this code:

import Mathlib.Data.Int.Init

example (f : ℤ → ℤ) (f0 : f 0 = 1) (f1 : f 1 = 2)
    (r : ∀ x, f x = 2 * f (x - 1) - f (x - 2) + 2) :
    ∀ x, 0 ≤ x → f x = x * x + 1 := by
  intro x
  induction x using Int.strongRec with
  | lt n hn =>
    -- cursor here
  | ge n hn ih => sorry

then, you will see that the type of hn is n < ?m.68. ?m.68 is an mvar (a hole for things Lean wasn't able to deduce).

[Jakub Nowak]

Nathan said:

i'm never sure what syntax to use for induction, is there a reference?

There's https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#induction. You can see the same if you hover over induction in the editor.

[Nathan]

thanks

[Jakub Nowak]

Nathan said:

what if you did want to prove it for all x, how could you do it?

We should probably add Int.strongRecOn' to mathlib. With it, it's simple:

import Mathlib.Data.Int.Init

def Int.strongRecOn' {motive : ℤ → Sort*} (z b : ℤ) (zero : motive b)
    (above : (n : ℤ) → b < n → (∀ k, b ≤ k → k < n → motive k) → motive n)
    (below : (n : ℤ) → n < b → (∀ k, k ≤ b → n < k → motive k) → motive n) : motive z :=
  if h : z < b then by
    refine below z h (z.inductionOn' b ?_ ?_ ?_)
    · intro k hk hk'
      exfalso
      lia
    · intro n hn ih k hk hk'
      exfalso
      lia
    · intro n hn ih k hk hk'
      if h' : k < b then
        refine below k h' ?_
        intro k₂ hk₂ hk₂'
        exact ih k₂ hk₂ (by lia)
      else
        exact (by lia : b = k) ▸ zero
  else if h : b < z then by
    refine above z h (z.inductionOn' b ?_ ?_ ?_)
    · intro k hk hk'
      exfalso
      lia
    · intro n hn ih k hk hk'
      if h' : b < k then
        refine above k h' ?_
        intro k₂ hk₂ hk₂'
        exact ih k₂ hk₂ (by lia)
      else
        exact (by lia : b = k) ▸ zero
    · intro n hn ih k hk hk'
      exfalso
      lia
  else
    (by lia : b = z) ▸ zero

example (f : ℤ → ℤ) (f0 : f 0 = 1) (f1 : f 1 = 2)
    (r : ∀ x, f x = 2 * f (x - 1) - f (x - 2) + 2) :
    ∀ x, f x = x * x + 1 := by
  intro x
  induction x using Int.strongRecOn' (b := 0) with
  | zero => grind
  | above n hn ih => grind
  | below n hn ih => grind

[Kevin Buzzard]

There's also a lightbulb for induction -- click on it and you'll get the option to automatically generate the correct syntax

[Ruben Van de Velde]

Kevin Buzzard said:

There's also a lightbulb for induction -- click on it and you'll get the option to automatically generate the correct syntax

Not for the induction line itself, though, which is the most annoying if you have a weird(-ish) induction principle