strong induction without `induction'`

Stream: Is there code for X?

[Asei Inoue]

/-- fibonacci sequence -/
def fibonacci : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fibonacci n + fibonacci (n + 1)

/-- linear time fibonacci -/
def fib (n : Nat) : Nat :=
  (loop n).1
where
  loop : Nat → Nat × Nat
    | 0 => (0, 1)
    | n + 1 =>
      let p := loop n
      (p.2, p.1 + p.2)

@[simp]
theorem fib_add (n : Nat) : fib n + fib (n + 1) = fib (n + 2) := by rfl

example : fibonacci = fib := by
  ext n

  -- strong induction on `n`
  -- I would like to know if it is possible to do strong induction, as used here, with `induction` instead of `induction'`.
  induction' n using Nat.strong_induction_on with n ih
  match n with
  | 0 => rfl
  | 1 => rfl
  | n + 2 => simp_all [fibonacci]

[Ruben Van de Velde]

theorem fib_eq : ∀ (n : Nat), fibonacci n = fib n
  | 0 => rfl
  | 1 => rfl
  | n + 2 => by simp_all [fibonacci, fib_eq]

[Asei Inoue]

wao!!!

[Asei Inoue]

@Ruben Van de Velde Thank you very much! This is surprising...

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Ruben Van de Velde]

What happens here is that you can use a theorem while you're proving that same theorem, as long as you finish in finitely many steps. Lean is often smart enough to figure out that termination proof for you, though

[Asei Inoue]

In this case, is it possible to get out the inductive assumption without naming the theorem (i.e. with an example)?

def sum (n : Nat) : Rat :=
  match n with
  | 0 => 0
  | n + 1 => (n + 1) + sum n

theorem sum_exp (n : Nat) : sum n = n * (n + 1) / 2 := by
  match n with

  | 0 => rfl

  | n + 1 =>
    have ih := sum_exp n

    simp [sum, ih]

    ring

[Notification Bot]

Asei Inoue has marked this topic as unresolved.

[Eric Wieser]

The answer to your original question is

  induction n using Nat.strong_induction_on with
  | h n ih =>

[Eric Wieser]

Where h is the argument name in Nat.strong_induction_on

[Kyle Miller]

In the current dev version of Lean 4, there's now a way to do induction on the structure of the function itself, due to @Joachim Breitner.

/-- fibonacci sequence -/
def fibonacci : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fibonacci n + fibonacci (n + 1)
termination_by n => sizeOf n -- trick to get functional induction to work (causes it to be well-founded recursion)

-- In next Lean release. Creates `fibonacci.induct`
derive_functional_induction fibonacci

/-- linear time fibonacci -/
def fib (n : Nat) : Nat :=
  (loop n).1
where
  loop : Nat → Nat × Nat
    | 0 => (0, 1)
    | n + 1 =>
      let p := loop n
      (p.2, p.1 + p.2)

@[simp]
theorem fib_add (n : Nat) : fib n + fib (n + 1) = fib (n + 2) := by rfl

example : fibonacci = fib := by
  ext n
  induction n using fibonacci.induct
  /-
  ⊢ fibonacci 0 = fib 0
  -/
  · rfl
  /-
  ⊢ fibonacci 1 = fib 1
  -/
  · rfl
  /-
  n : Nat
  ih1 : fibonacci n = fib n
  ih2 : fibonacci (n + 1) = fib (n + 1)
  ⊢ fibonacci (Nat.succ (Nat.succ n)) = fib (Nat.succ (Nat.succ n))
  -/
  next n ih1 ih2 => simp [fibonacci, *]

[Kyle Miller]

(@Joachim Breitner Will there be a way to derive functional induction for definitions that are defined with plain recursion? I worked around it here by using an artificial termination_by.)

[Joachim Breitner]

Eric Wieser said:

The answer to your original question is

  induction n using Nat.strong_induction_on with
  | h n ih =>

Or

  induction n using Nat.strong_induction_on with
  | _ n ih =>

if you don’t care, or

  induction n using Nat.strong_induction_on
  next n ih =>

if you prefer next/case over the with | … syntax.

[Joachim Breitner]

Kyle Miller said:

(Joachim Breitner Will there be a way to derive functional induction for definitions that are defined with plain recursion? I worked around it here by using an artificial termination_by.)

Yes! I experimented with that on monday, and it seems doable, and is somewhere on my roadmap not too far down, so it will work eventually.