Bug in `fun_induction` tactic

Stream: lean4

[Frédéric Dupuis]

I found a strange bug in the fun_induction tactic:

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)

def ack' : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack' x 1
  | x+1, y+1 => ack' x (ack' (x+1) y)

theorem ack'_eq_ack_works (i x : Nat) : ack' i x = ack i x := by
  fun_induction ack with
  | case1 => sorry
  | case2 => sorry
  | case3 => sorry

theorem ack'_eq_ack_fails : ack' = ack := by
  ext i x
  fun_induction ack with   -- Could not find a suitable call of 'ack' in the goal
  | case1 => sorry
  | case2 => sorry
  | case3 => sorry

In the second example, fun_induction fails despite the fact that the goal is identical to the first example. Perhaps @Joachim Breitner could have a quick look?

[Kyle Miller]

Adding dsimp only right before fun_induction makes it go through. Maybe it's a metavariable instantiation issue?

Edit: Yes, there are metavariables:

import Lean

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)

def ack' : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack' x 1
  | x+1, y+1 => ack' x (ack' (x+1) y)

open Lean Elab Tactic in
elab "show_goal" : tactic => do
  withMainContext do
    logInfo m!"{(← getMainDecl).type}"

set_option pp.all true
set_option pp.instantiateMVars false

example : ack' = ack := by
  ext i x
  show_goal   -- @Eq.{?u.53900} (?β x) (?f x) (?g x)
  dsimp only
  show_goal   -- @Eq.{?u.53900} Nat (ack' i x) (ack i x)
  fun_induction ack with
  | case1 => sorry
  | case2 => sorry
  | case3 => sorry

[Joachim Breitner]

Thanks for the report and analysis. Note that fun_induction ack i x works, so the component that is broken is the “guess the function paramters” part. Reported at https://github.com/leanprover/lean4/issues/9844