feat: fun_induction foo (no arguments) (leanprover#7101)

This PR implements `fun_induction foo`, which is like `fun_induction foo
x y z`, only that it picks the arguments to use from a unique suitable
call to `foo` in the goal.

Author: nomeata

Diff for: src/Init/Tactics.lean

@@ -917,6 +917,14 @@ induction y₁, ... yₘ using f.induct x₁ ... xₙ
 where the arguments of `f` are used as arguments to `f.induct` or targets of the induction, as
 appropriate.
 
+The form
+```
+fun_induction f
+```
+(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
+these arguments. An application of `f` is eligible if it is saturated and the arguments that will
+become targets are free variables.
+
 The forms `fun_induction f x y generalizing z₁ ... zₙ` and
 `fun_induction f x y with | case1 => tac₁ | case2 x' ih => tac₂` work like with `induction.`
 -/
@@ -938,6 +946,14 @@ cases y, ... using f.fun_cases x ...
 where the arguments of `f` are used as arguments to `f.fun_cases` or targets of the case analysis, as
 appropriate.
 
+The form
+```
+fun_cases f
+```
+(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
+these arguments. An application of `f` is eligible if it is saturated and the arguments that will
+become targets are free variables.
+
 The form `fun_cases f x y with | case1 => tac₁ | case2 x' ih => tac₂` works like with `cases`.
 -/
 syntax (name := funCases) "fun_cases " term (inductionAlts)? : tactic

Diff for: src/Lean/Elab/Tactic/Induction.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.ElimInfo
 import Lean.Meta.Tactic.FunIndInfo
 import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.FunIndCollect
 import Lean.Meta.GeneralizeVars
 import Lean.Elab.App
 import Lean.Elab.Tactic.ElabTerm
@@ -819,12 +820,33 @@ def evalInduction : Tactic := fun stx =>
     let targets ← withMainContext <| addImplicitTargets elimInfo targets
     evalInductionCore stx elimInfo targets toTag
 
+
+/--
+Elaborates the `foo args` of `fun_induction` or `fun_cases`, inferring the args if omitted from the goal
+-/
+def elabFunTargetCall (cases : Bool) (stx : Syntax) : TacticM Expr := do
+  match stx with
+  | `($id:ident) =>
+    let fnName ← realizeGlobalConstNoOverload id
+    let some _ ← getFunIndInfo? cases fnName |
+      let theoremKind := if cases then "induction" else "cases"
+      throwError "no functional {theoremKind} theorem for '{.ofConstName fnName}', or function is mutually recursive "
+    let candidates ← FunInd.collect fnName (← getMainGoal)
+    if candidates.isEmpty then
+      throwError "could not find suitable call of '{.ofConstName fnName}' in the goal"
+    if candidates.size > 1 then
+      throwError "found more than one suitable call of '{.ofConstName fnName}' in the goal. \
+        Please include the desired arguments."
+    pure candidates[0]!
+  | _ =>
+    elabTerm stx none
+
 /--
 Elaborates the `foo args` of `fun_induction` or `fun_cases`, returning the `ElabInfo` and targets.
 -/
 private def elabFunTarget (cases : Bool) (stx : Syntax) : TacticM (ElimInfo × Array Expr) := do
   withRef stx <| withMainContext do
-    let funCall ← elabTerm stx none
+    let funCall ← elabFunTargetCall cases stx
     funCall.withApp fun fn funArgs => do
     let .const fnName fnUs := fn |
       throwError "expected application headed by a function constant"

Diff for: src/Lean/Meta/Tactic/FunIndCollect.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.FunIndInfo
+
+/-!
+Support for collecting function calls that could be used for `fun_induction` or `fun_cases`.
+Used by `fun_induction foo`, and the `Calls` structure is also used by `try?`.
+-/
+
+namespace Lean.Meta.FunInd
+
+structure Call where
+  /- The full function call -/
+  expr : Expr
+  /- Used to avoid adding calls that differ only in dropped arguments -/
+  relevantArgs : Expr
+  deriving Hashable, BEq
+
+structure SeenCalls where
+  /-- the full calls -/
+  calls : Array Expr
+  /-- only relevant arguments -/
+  seen : Std.HashSet (Array Expr)
+
+instance : EmptyCollection SeenCalls where
+  emptyCollection := ⟨#[], {}⟩
+
+def SeenCalls.push (e : Expr) (declName : Name) (args : Array Expr) (calls : SeenCalls) :
+    MetaM SeenCalls := do
+  let some funIndInfo ← getFunIndInfo? (cases := false) declName | return calls
+  if funIndInfo.params.size != args.size then return calls
+  let mut keys := #[]
+  for arg in args, kind in funIndInfo.params do
+    if kind matches .target then
+      if !arg.isFVar then return calls
+    unless kind matches .dropped do
+      keys := keys.push arg
+  if calls.seen.contains keys then return calls
+  return { calls := calls.calls.push e, seen := calls.seen.insert keys }
+
+namespace Collector
+
+abbrev M := ReaderT Name <| StateRefT SeenCalls MetaM
+
+def saveFunInd (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
+  set (← (← get).push e declName args)
+
+def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
+  saveFunInd e declName args
+
+unsafe abbrev Cache := PtrSet Expr
+
+unsafe def visit (e : Expr) : StateRefT Cache M Unit := do
+  unless (← get).contains e do
+    modify fun s => s.insert e
+    match e with
+      | .const _ _        => pure ()
+      | .forallE _ d b _  => visit d; visit b
+      | .lam _ d b _      => visit d; visit b
+      | .mdata _ b        => visit b
+      | .letE _ t v b _   => visit t; visit v; visit b
+      | .app ..           => e.withApp fun f args => do
+        if let .const declName _ := f then
+          if declName = (← read) then
+            unless e.hasLooseBVars do -- TODO: We can allow them in `.dropped` arguments
+              visitApp e declName args
+        else
+          visit f
+        args.forM visit
+      | .proj _ _ b       => visit b
+      | _                 => return ()
+
+unsafe def main (needle : Name) (mvarId : MVarId) : MetaM (Array Expr) := mvarId.withContext do
+  let (_, s) ← go |>.run mkPtrSet |>.run needle |>.run {}
+  return s.calls
+where
+  go : StateRefT Cache M Unit := do
+    for localDecl in (← getLCtx) do
+      unless localDecl.isAuxDecl do
+        if let some val := localDecl.value? then
+          visit val
+        else
+          visit localDecl.type
+    visit (← mvarId.getType)
+
+end Collector
+
+def collect (needle : Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+  unsafe Collector.main needle mvarId
+
+end Lean.Meta.FunInd

Diff for: tests/lean/run/funInduction.lean

@@ -168,13 +168,6 @@ error: Expected fully applied application of 'ackermann' with 2 arguments, but f
 example : P (ackermann n m) := by
   fun_induction ackermann n
 
-/--
-error: Expected fully applied application of 'ackermann' with 2 arguments, but found 0 arguments
--/
-#guard_msgs in
-example : P (ackermann n m) := by
-  fun_induction ackermann
-
 end Ex2
 
 namespace Ex3