From a3b76aa825237965ecbe34708b5cfcd225f64e4c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 18 Feb 2025 13:27:21 +0100
Subject: [PATCH] feat: `fun_induction foo` (no arguments) (#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.
---
 src/Init/Tactics.lean                   |  16 ++
 src/Lean/Elab/Tactic/Induction.lean     |  24 +-
 src/Lean/Meta/Tactic/FunIndCollect.lean |  97 +++++++
 tests/lean/run/funInduction.lean        |   7 -
 tests/lean/run/funinduction_ident.lean  | 328 ++++++++++++++++++++++++
 5 files changed, 464 insertions(+), 8 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/FunIndCollect.lean
 create mode 100644 tests/lean/run/funinduction_ident.lean

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index d6ccac17fb..c3bd90299d 100644
--- a/src/Init/Tactics.lean
+++ b/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 --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 1e7f3a8b47..f765c07c8a 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/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 --git a/src/Lean/Meta/Tactic/FunIndCollect.lean b/src/Lean/Meta/Tactic/FunIndCollect.lean
new file mode 100644
index 0000000000..2d99f0a711
--- /dev/null
+++ b/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 --git a/tests/lean/run/funInduction.lean b/tests/lean/run/funInduction.lean
index 85838a6ba4..7c02848209 100644
--- a/tests/lean/run/funInduction.lean
+++ b/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
diff --git a/tests/lean/run/funinduction_ident.lean b/tests/lean/run/funinduction_ident.lean
new file mode 100644
index 0000000000..b3318a4fe8
--- /dev/null
+++ b/tests/lean/run/funinduction_ident.lean
@@ -0,0 +1,328 @@
+namespace ListEx
+
+theorem map_id (xs : List α) : List.map id xs = xs := by
+  fun_induction List.map <;> simp_all only [List.map, id]
+
+-- This works because collect ignores `.dropped` arguments
+
+theorem map_map (f : α → β) (g : β → γ) xs :
+  List.map g (List.map f xs) = List.map (g ∘ f) xs := by
+  fun_induction List.map <;> simp_all only [List.map, Function.comp]
+
+-- This should genuinely not work, but have a good error message
+
+/--
+error: found more than one suitable call of 'List.append' in the goal. Please include the desired arguments.
+-/
+#guard_msgs in
+theorem append_assoc :
+  List.append xs (List.append ys zs) = List.append (List.append xs ys) zs := by
+  fun_induction List.append <;> simp_all only [List.append]
+
+end ListEx
+
+namespace Ex1
+
+variable (P : Nat → Prop)
+
+def ackermann : (Nat × Nat) → Nat
+  | (0, m) => m + 1
+  | (n+1, 0) => ackermann (n, 1)
+  | (n+1, m+1) => ackermann (n, ackermann (n + 1, m))
+termination_by p => p
+
+/--
+error: tactic 'fail' failed
+case case1
+P : Nat → Prop
+m✝ : Nat
+⊢ P (ackermann (0, m✝))
+
+case case2
+P : Nat → Prop
+n✝ : Nat
+ih1✝ : P (ackermann (n✝, 1))
+⊢ P (ackermann (n✝.succ, 0))
+
+case case3
+P : Nat → Prop
+n✝ m✝ : Nat
+ih2✝ : P (ackermann (n✝ + 1, m✝))
+ih1✝ : P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
+⊢ P (ackermann (n✝.succ, m✝.succ))
+-/
+#guard_msgs in
+example : P (ackermann p) := by
+  fun_induction ackermann
+  fail
+
+/--
+error: tactic 'fail' failed
+case case1
+P : Nat → Prop
+m✝ : Nat
+⊢ P (ackermann (0, m✝))
+
+case case2
+P : Nat → Prop
+n✝ : Nat
+⊢ P (ackermann (n✝.succ, 0))
+
+case case3
+P : Nat → Prop
+n✝ m✝ : Nat
+⊢ P (ackermann (n✝.succ, m✝.succ))
+-/
+#guard_msgs in
+example : P (ackermann p) := by
+  fun_cases ackermann
+  fail
+
+/-- error: could not find suitable call of 'ackermann' in the goal -/
+#guard_msgs in
+example : P (ackermann (n, m)) := by
+  fun_induction ackermann
+
+end Ex1
+
+namespace Ex2
+
+variable (P : Nat → Prop)
+
+def ackermann : Nat → Nat → Nat
+  | 0, m => m + 1
+  | n+1, 0 => ackermann n 1
+  | n+1, m+1 => ackermann n (ackermann (n + 1) m)
+termination_by n m => (n, m)
+
+/--
+error: unsolved goals
+case case1
+P : Nat → Prop
+m✝ : Nat
+⊢ P (ackermann 0 m✝)
+
+case case2
+P : Nat → Prop
+n✝ : Nat
+ih1✝ : P (ackermann n✝ 1)
+⊢ P (ackermann n✝.succ 0)
+
+case case3
+P : Nat → Prop
+n✝ m✝ : Nat
+ih2✝ : P (ackermann (n✝ + 1) m✝)
+ih1✝ : P (ackermann n✝ (ackermann (n✝ + 1) m✝))
+⊢ P (ackermann n✝.succ m✝.succ)
+-/
+#guard_msgs in
+example : P (ackermann n m) := by
+  fun_induction ackermann
+
+end Ex2
+
+namespace Ex3
+
+variable (P : List α → Prop)
+
+def ackermann {α} (inc : List α) : List α → List α → List α
+  | [], ms => ms ++ inc
+  | _::ns, [] => ackermann inc ns inc
+  | n::ns, _::ms => ackermann inc ns (ackermann inc (n::ns) ms)
+termination_by ns ms => (ns, ms)
+
+/--
+error: unsolved goals
+case case1
+α : Type u_1
+P : List α → Prop
+inc ms✝ : List α
+⊢ P (ackermann inc [] ms✝)
+
+case case2
+α : Type u_1
+P : List α → Prop
+inc : List α
+head✝ : α
+ns✝ : List α
+ih1✝ : P (ackermann inc ns✝ inc)
+⊢ P (ackermann inc (head✝ :: ns✝) [])
+
+case case3
+α : Type u_1
+P : List α → Prop
+inc : List α
+n✝ : α
+ns✝ : List α
+head✝ : α
+ms✝ : List α
+ih2✝ : P (ackermann inc (n✝ :: ns✝) ms✝)
+ih1✝ : P (ackermann inc ns✝ (ackermann inc (n✝ :: ns✝) ms✝))
+⊢ P (ackermann inc (n✝ :: ns✝) (head✝ :: ms✝))
+-/
+#guard_msgs in
+example : P (ackermann inc n m) := by
+  fun_induction ackermann
+
+end Ex3
+
+namespace Structural
+
+variable (P : Nat → Prop)
+
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n+2 => fib n + fib (n+1)
+termination_by structural x => x
+
+/--
+error: tactic 'fail' failed
+case case1
+P : Nat → Prop
+⊢ P (fib 0)
+
+case case2
+P : Nat → Prop
+⊢ P (fib 1)
+
+case case3
+P : Nat → Prop
+n✝ : Nat
+ih2✝ : P (fib n✝)
+ih1✝ : P (fib (n✝ + 1))
+⊢ P (fib n✝.succ.succ)
+-/
+#guard_msgs in
+example : P (fib n) := by
+  fun_induction fib
+  fail
+
+/-- error: could not find suitable call of 'fib' in the goal -/
+#guard_msgs in
+example : n ≤ fib (n + 2) := by
+  fun_induction fib
+
+end Structural
+
+namespace StructuralWithOmittedParam
+
+variable (P : Nat → Prop)
+
+variable (inc : Nat)
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => inc
+  | n+2 => fib n + fib (n+1)
+termination_by structural x => x
+
+/--
+info: StructuralWithOmittedParam.fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
+-/
+#guard_msgs in
+#check fib.induct -- NB: No inc showing up
+
+/--
+error: tactic 'fail' failed
+case case1
+P : Nat → Prop
+inc : Nat
+⊢ P (fib 2 0)
+
+case case2
+P : Nat → Prop
+inc : Nat
+⊢ P (fib 2 1)
+
+case case3
+P : Nat → Prop
+inc n✝ : Nat
+ih2✝ : P (fib 2 n✝)
+ih1✝ : P (fib 2 (n✝ + 1))
+⊢ P (fib 2 n✝.succ.succ)
+-/
+#guard_msgs in
+example : P (fib 2 n) := by
+  fun_induction fib
+  fail
+
+end StructuralWithOmittedParam
+
+namespace StructuralIndices
+
+-- Testing recursion on an indexed data type
+inductive Finn : Nat → Type where
+  | fzero : {n : Nat} → Finn n
+  | fsucc : {n : Nat} → Finn n → Finn (n+1)
+
+def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
+  | fzero, _ => fzero
+  | _, fzero => fzero
+  | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
+termination_by structural i => i
+
+def Finn.min' (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
+  | fzero, _ => fzero
+  | _, fzero => fzero
+  | fsucc i, fsucc j => fsucc (Finn.min' (not x) (m + 1) i j)
+termination_by structural _ j => j
+
+def Finn.min'' (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
+  | fzero, _ => fzero
+  | _, fzero => fzero
+  | fsucc i, fsucc j => fsucc (Finn.min'' (not x) (m + 1) i j)
+termination_by structural n
+
+def Finn.le : Finn n → Finn n → Bool
+  | fzero, _ => true
+  | _, fzero => false
+  | fsucc i, fsucc j => Finn.le i j
+
+theorem Finn.min_le_right₀ : (Finn.min x m i j).le j := by
+  induction x, m, i, j using @Finn.min.induct <;> simp_all [Finn.min, Finn.le]
+
+theorem Finn.min_le_right : (Finn.min x m i j).le j := by
+  fun_induction Finn.min <;> simp_all [Finn.min, Finn.le]
+
+theorem Finn.min_le_right' : (Finn.min' x m i j).le j := by
+  fun_induction Finn.min' <;> simp_all [Finn.min', Finn.le]
+
+theorem Finn.min_le_right'' : (Finn.min'' x m i j).le j := by
+  fun_induction Finn.min'' <;> simp_all [Finn.min'', Finn.le]
+
+end StructuralIndices
+
+namespace Nonrec
+
+def foo := 1
+
+/-- error: no functional cases theorem for 'foo', or function is mutually recursive -/
+#guard_msgs in
+example : True := by
+  fun_induction foo
+
+end Nonrec
+
+namespace Mutual
+
+inductive Tree (α : Type u) : Type u where
+  | node : α → (Bool → List (Tree α)) → Tree α
+
+-- Recursion over nested inductive
+
+mutual
+def Tree.size : Tree α → Nat
+  | .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false)
+termination_by structural t => t
+def Tree.size_aux : List (Tree α) → Nat
+  | [] => 0
+  | t :: ts => size t + size_aux ts
+end
+
+/-- error: no functional cases theorem for 'Tree.size', or function is mutually recursive -/
+#guard_msgs in
+example (t : Tree α) : True := by
+  fun_induction Tree.size
+
+end Mutual