feat: fun_induction to unfold function application in the goal (#8104)

This PR makes `fun_induction` and `fun_cases` (try to) unfold the
function application of interest in the goal. The old behavior can be
enabled with `set_option tactic.fun_induction.unfolding false`. For
`fun_cases` this does not work yet when the function’s result type
depends on one of the arguments, see issue #8296.

src/Init/Data/Int/Linear.lean

@@ -16,6 +16,10 @@ import Init.Data.Int.Gcd
 import Init.Data.RArray
 import Init.Data.AC
 
+-- bootstrapping aid
+#guard_msgs(drop error) in
+set_option tactic.fun_induction.unfolding false
+
 namespace Int.Linear
 
 /-! Helper definitions and theorems for constructing linear arithmetic proofs. -/

src/Init/Grind/CommRing/Poly.lean

@@ -12,6 +12,10 @@ import Init.Data.Ord
 import Init.Data.RArray
 import Init.Grind.CommRing.Basic
 
+-- bootstrapping aid
+#guard_msgs(drop error) in
+set_option tactic.fun_induction.unfolding false
+
 namespace Lean.Grind
 namespace CommRing
 

src/Init/Tactics.lean

@@ -940,8 +940,8 @@ You can use `with` to provide the variables names for each constructor.
 syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic
 
 /--
-The `fun_induction` tactic is a convenience wrapper of the `induction` tactic when using a functional
-induction principle.
+The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the the
+functional induction principle.
 
 The tactic invocation
 ```
@@ -949,10 +949,10 @@ fun_induction f x₁ ... xₙ y₁ ... yₘ
 ```
 where `f` is a function defined by non-mutual structural or well-founded recursion, is equivalent to
 ```
-induction y₁, ... yₘ using f.induct x₁ ... xₙ
+induction y₁, ... yₘ using f.induct_unfolding x₁ ... xₙ
 ```
-where the arguments of `f` are used as arguments to `f.induct` or targets of the induction, as
-appropriate.
+where the arguments of `f` are used as arguments to `f.induct_unfolding` or targets of the
+induction, as appropriate.
 
 The form
 ```
@@ -964,6 +964,10 @@ 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.`
+
+Under `set_option tactic.fun_induction.unfolding true` (the default), `fun_induction` uses the
+`f.induct_unfolding` induction principle, which will try to automatically unfold the call to `f` in
+the goal. With `set_option tactic.fun_induction.unfolding false`, it uses `f.induct` instead.
 -/
 syntax (name := funInduction) "fun_induction " term
   (" generalizing" (ppSpace colGt term:max)+)? (inductionAlts)? : tactic
@@ -978,10 +982,10 @@ fun_cases f x ... y ...`
 ```
 is equivalent to
 ```
-cases y, ... using f.fun_cases x ...
+cases y, ... using f.fun_cases_unfolding x ...
 ```
-where the arguments of `f` are used as arguments to `f.fun_cases` or targets of the case analysis, as
-appropriate.
+where the arguments of `f` are used as arguments to `f.fun_cases_unfolding` or targets of the case
+analysis, as appropriate.
 
 The form
 ```
@@ -992,6 +996,10 @@ these arguments. An application of `f` is eligible if it is saturated and the ar
 become targets are free variables.
 
 The form `fun_cases f x y with | case1 => tac₁ | case2 x' ih => tac₂` works like with `cases`.
+
+Under `set_option tactic.fun_induction.unfolding true` (the default), `fun_induction` uses the
+`f.fun_cases_unfolding` theorem, which will try to automatically unfold the call to `f` in
+the goal. With `set_option tactic.fun_induction.unfolding false`, it uses `f.fun_cases` instead.
 -/
 syntax (name := funCases) "fun_cases " term (inductionAlts)? : tactic
 

src/Lean/Elab/Tactic/Induction.lean

@@ -887,6 +887,16 @@ def evalInduction : Tactic := fun stx =>
     evalInductionCore stx elimInfo targets toTag
 
 
+register_builtin_option tactic.fun_induction.unfolding : Bool := {
+  defValue := true
+  group    := "tactic"
+  descr    := "if set to 'true', then 'fun_induction' and 'fun_cases' will use the “unfolding \
+    functional induction (resp. cases) principle” ('….induct_unfolding'/'….fun_cases_unfolding'), \
+    which will attempt to replace the function goal of interest in the goal with the appropriate \
+    right-hand-side in each case. If 'false', the regular “functional induction principle” \
+    ('….induct'/'….fun_cases') is used."
+}
+
 /--
 Elaborates the `foo args` of `fun_induction` or `fun_cases`, inferring the args if omitted from the goal
 -/
@@ -894,10 +904,11 @@ 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"
+    let unfolding := tactic.fun_induction.unfolding.get (← getOptions)
+    let some funIndInfo ← getFunIndInfo? (cases := cases) (unfolding := unfolding) fnName |
+      let theoremKind := if cases then "cases" else "induction"
       throwError "no functional {theoremKind} theorem for '{.ofConstName fnName}', or function is mutually recursive "
-    let candidates ← FunInd.collect fnName (← getMainGoal)
+    let candidates ← FunInd.collect funIndInfo (← getMainGoal)
     if candidates.isEmpty then
       throwError "could not find suitable call of '{.ofConstName fnName}' in the goal"
     if candidates.size > 1 then
@@ -916,8 +927,9 @@ private def elabFunTarget (cases : Bool) (stx : Syntax) : TacticM (ElimInfo × A
     funCall.withApp fun fn funArgs => do
     let .const fnName fnUs := fn |
       throwError "expected application headed by a function constant"
-    let some funIndInfo ← getFunIndInfo? cases fnName |
-      let theoremKind := if cases then "induction" else "cases"
+    let unfolding := tactic.fun_induction.unfolding.get (← getOptions)
+    let some funIndInfo ← getFunIndInfo? (cases := cases) (unfolding := unfolding) fnName |
+      let theoremKind := if cases then "cases" else "induction"
       throwError "no functional {theoremKind} theorem for '{.ofConstName fnName}', or function is mutually recursive "
     if funArgs.size != funIndInfo.params.size then
       throwError "Expected fully applied application of '{.ofConstName fnName}' with \

src/Lean/Meta/Tactic/FunInd.lean

@@ -1034,6 +1034,7 @@ where doRealize (inductName : Name) := do
     { name := inductName, levelParams := us, type := eTyp, value := e' }
 
   setFunIndInfo {
+      funName := name
       funIndName := inductName
       levelMask := usMask
       params := paramMask.map (cond · .param .dropped) ++ #[.target]
@@ -1063,9 +1064,9 @@ def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct :
 For a (non-mutual!) definition of `name`, uses the `FunIndInfo` associated with the `unaryInduct` and
 derives the one for the n-ary function.
 -/
-def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
+def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (funName : Name) (unaryInduct : Name) : MetaM Unit := do
   assert!  fixedParamPerms.perms.size = 1 -- only non-mutual for now
-  let funIndName := getFunInductName (unfolding := unfolding) name
+  let funIndName := getFunInductName (unfolding := unfolding) funName
   unless funIndName = unaryInduct do
     let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct
       | throwError "Expected {unaryInduct} to have FunIndInfo"
@@ -1081,7 +1082,7 @@ def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (na
         params := params.push .target
     assert! j + 1 = unaryFunIndInfo.params.size
 
-    setFunIndInfo { unaryFunIndInfo with funIndName, params }
+    setFunIndInfo { unaryFunIndInfo with funName, funIndName, params }
 
 /--
 In the type of `value`, reduces
@@ -1442,6 +1443,7 @@ where doRealize inductName := do
         params := params.push .target
 
     setFunIndInfo {
+      funName := names[0]!
       funIndName := inductName, levelMask := usMask, params := params
     }
 
@@ -1514,6 +1516,7 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
       { name := casesName, levelParams := us, type := eTyp, value := e' }
 
     setFunIndInfo {
+      funName := name
       funIndName := casesName
       levelMask := usMask
       params := .replicate motiveArity .target

src/Lean/Meta/Tactic/FunIndCollect.lean

@@ -34,9 +34,8 @@ instance : EmptyCollection SeenCalls where
 def SeenCalls.isEmpty  (sc : SeenCalls) : Bool :=
   sc.calls.isEmpty
 
-def SeenCalls.push (e : Expr) (declName : Name) (args : Array Expr) (calls : SeenCalls) :
+def SeenCalls.push (e : Expr) (funIndInfo : FunIndInfo) (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
@@ -44,7 +43,7 @@ def SeenCalls.push (e : Expr) (declName : Name) (args : Array Expr) (calls : See
       if !arg.isFVar then return calls
     unless kind matches .dropped do
       keys := keys.push arg
-  let key := (declName, keys)
+  let key := (funIndInfo.funName, keys)
   if calls.seen.contains key then return calls
   return { calls := calls.calls.push e, seen := calls.seen.insert key }
 
@@ -65,13 +64,13 @@ def SeenCalls.uniques (calls : SeenCalls) : NameSet := Id.run do
 
 namespace Collector
 
-abbrev M := ReaderT Name <| StateRefT SeenCalls MetaM
+abbrev M := ReaderT FunIndInfo <| StateRefT SeenCalls MetaM
 
-def saveFunInd (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
-  set (← (← get).push e declName args)
+def saveFunInd (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) : M Unit := do
+  set (← (← get).push e funIndInfo args)
 
-def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
-  saveFunInd e declName args
+def visitApp (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) : M Unit := do
+  saveFunInd e funIndInfo args
 
 unsafe abbrev Cache := PtrSet Expr
 
@@ -86,16 +85,16 @@ unsafe def visit (e : Expr) : StateRefT Cache M Unit := do
       | .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
+          if declName = (← read).funName then
             unless e.hasLooseBVars do -- TODO: We can allow them in `.dropped` arguments
-              visitApp e declName args
+              visitApp e (← read) 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
+unsafe def main (needle : FunIndInfo) (mvarId : MVarId) : MetaM (Array Expr) := mvarId.withContext do
   let (_, s) ← go |>.run mkPtrSet |>.run needle |>.run {}
   return s.calls
 where
@@ -110,7 +109,7 @@ where
 
 end Collector
 
-def collect (needle : Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+def collect (needle : FunIndInfo) (mvarId : MVarId) : MetaM (Array Expr) := do
   unsafe Collector.main needle mvarId
 
 end Lean.Meta.FunInd

src/Lean/Meta/Tactic/FunIndInfo.lean

@@ -30,6 +30,7 @@ A `FunIndInfo` indicates how a function's arguments map to the arguments of the
 The size of `params` also indicates the arity of the function.
 -/
 structure FunIndInfo where
+  funName : Name
   funIndName : Name
   /--
   `true` means that the corresponding level parameter of the function is also a level param
@@ -59,13 +60,13 @@ def getMutualInductName (declName : Name) (unfolding : Bool := false) : Name :=
   else
     declName ++ `mutual_induct
 
-def getFunInduct? (cases : Bool) (declName : Name) : CoreM (Option Name) := do
+def getFunInduct? (unfolding : Bool) (cases : Bool) (declName : Name) : CoreM (Option Name) := do
   let .defnInfo _ ← getConstInfo declName | return none
   try
     let thmName := if cases then
-      getFunCasesName declName
+      getFunCasesName (unfolding := unfolding) declName
     else
-      getFunInductName declName
+      getFunInductName (unfolding := unfolding) declName
     let result ← realizeGlobalConstNoOverloadCore thmName
     return some result
   catch _ =>
@@ -78,8 +79,8 @@ def setFunIndInfo (funIndInfo : FunIndInfo) : CoreM Unit := do
 def getFunIndInfoForInduct?  (inductName : Name) : CoreM (Option FunIndInfo) := do
   return funIndInfoExt.find? (← getEnv) inductName
 
-def getFunIndInfo? (cases : Bool) (funName : Name) : CoreM (Option FunIndInfo) := do
-  let some inductName ← getFunInduct? cases funName | return none
+def getFunIndInfo? (cases : Bool) (unfolding : Bool) (funName : Name) : CoreM (Option FunIndInfo) := do
+  let some inductName ← getFunInduct? (cases := cases) (unfolding := unfolding) funName | return none
   getFunIndInfoForInduct? inductName
 
 end Lean.Meta

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -100,9 +100,10 @@ def visitConst (declName : Name) : M Unit := do
 
 def saveFunInd (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
   if (← isEligible declName) then
-    let sc := (← get).funIndCandidates
-    let sc' ← sc.push e declName args
-    modify fun s => { s with funIndCandidates := sc' }
+    if let some funIndInfo ← getFunIndInfo? (cases := false) (unfolding := true) declName then
+      let sc := (← get).funIndCandidates
+      let sc' ← sc.push e funIndInfo args
+      modify fun s => { s with funIndCandidates := sc' }
 
 open LibrarySearch in
 def saveLibSearchCandidates (e : Expr) : M Unit := do

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/grind/grind_ite_funinduction.lean

@@ -183,8 +183,7 @@ theorem normalize_correct (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by
   fun_induction normalize
   rotate_left
-  · unfold normalize
-    -- Note this error disappears if we remove the unused `h` from the match above.
+  · -- Note this error disappears if we remove the unused `h` from the match above.
     -- Fails with
     -- [issue] type error constructing proof for IfExpr.normalize.match_1.eq_1
     --   when assigning metavariable ?h_1 with

tests/lean/run/funInduction.lean

@@ -1,5 +1,3 @@
-import Lean
-
 namespace Ex1
 
 variable (P : Nat → Prop)
@@ -15,20 +13,20 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
 ih1✝ : P (ackermann (n✝, 1))
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 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))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann p) := by
@@ -40,17 +38,17 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 case case3
 P : Nat → Prop
 n✝ m✝ : Nat
-⊢ P (ackermann (n✝.succ, m✝.succ))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann p) := by
@@ -62,20 +60,20 @@ error: unsolved goals
 case case1
 P : Nat → Prop
 n m m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n m n✝ : Nat
 ih1✝ : P (ackermann (n✝, 1))
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 case case3
 P : Nat → Prop
 n m n✝ m✝ : Nat
 ih2✝ : P (ackermann (n✝ + 1, m✝))
 ih1✝ : P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
-⊢ P (ackermann (n✝.succ, m✝.succ))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann (n, m)) := by
@@ -86,17 +84,17 @@ error: unsolved goals
 case case1
 P : Nat → Prop
 n m m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n m n✝ : Nat
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 case case3
 P : Nat → Prop
 n m n✝ m✝ : Nat
-⊢ P (ackermann (n✝.succ, m✝.succ))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann (n, m)) := by
@@ -142,20 +140,20 @@ error: unsolved goals
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann 0 m✝)
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
 ih1✝ : P (ackermann n✝ 1)
-⊢ P (ackermann n✝.succ 0)
+⊢ P (ackermann n✝ 1)
 
 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)
+⊢ P (ackermann n✝ (ackermann (n✝ + 1) m✝))
 -/
 #guard_msgs in
 example : P (ackermann n m) := by
@@ -186,7 +184,7 @@ case case1
 α : Type u_1
 P : List α → Prop
 inc ms✝ : List α
-⊢ P (ackermann inc [] ms✝)
+⊢ P (ms✝ ++ inc)
 
 case case2
 α : Type u_1
@@ -195,7 +193,7 @@ inc : List α
 head✝ : α
 ns✝ : List α
 ih1✝ : P (ackermann inc ns✝ inc)
-⊢ P (ackermann inc (head✝ :: ns✝) [])
+⊢ P (ackermann inc ns✝ inc)
 
 case case3
 α : Type u_1
@@ -207,7 +205,7 @@ 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✝))
+⊢ P (ackermann inc ns✝ (ackermann inc (n✝ :: ns✝) ms✝))
 -/
 #guard_msgs in
 example : P (ackermann inc n m) := by
@@ -243,18 +241,18 @@ termination_by structural x => x
 error: tactic 'fail' failed
 case case1
 P : Nat → Prop
-⊢ P (fib 0)
+⊢ P 0
 
 case case2
 P : Nat → Prop
-⊢ P (fib 1)
+⊢ P 1
 
 case case3
 P : Nat → Prop
 n✝ : Nat
 ih2✝ : P (fib n✝)
 ih1✝ : P (fib (n✝ + 1))
-⊢ P (fib n✝.succ.succ)
+⊢ P (fib n✝ + fib (n✝ + 1))
 -/
 #guard_msgs in
 example : P (fib n) := by
@@ -322,19 +320,19 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 inc : Nat
-⊢ P (fib 2 0)
+⊢ P 0
 
 case case2
 P : Nat → Prop
 inc : Nat
-⊢ P (fib 2 1)
+⊢ P 2
 
 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)
+⊢ P (fib 2 n✝ + fib 2 (n✝ + 1))
 -/
 #guard_msgs in
 example : P (fib 2 n) := by
@@ -391,7 +389,7 @@ namespace Nonrec
 
 def foo := 1
 
-/-- error: no functional cases theorem for 'foo', or function is mutually recursive -/
+/-- error: no functional induction theorem for 'foo', or function is mutually recursive -/
 #guard_msgs in
 example : True := by
   fun_induction foo
@@ -415,7 +413,7 @@ def Tree.size_aux : List (Tree α) → Nat
   | t :: ts => size t + size_aux ts
 end
 
-/-- error: no functional cases theorem for 'Tree.size', or function is mutually recursive -/
+/-- error: no functional induction theorem for 'Tree.size', or function is mutually recursive -/
 #guard_msgs in
 example (t : Tree α) : True := by
   fun_induction Tree.size t

tests/lean/run/fun_cases.lean

@@ -9,8 +9,8 @@ info: Option.map.fun_cases.{u_1, u_2} (motive : {α : Type u_1} → {β : Type u
 
 example (x : Option Nat) (f : Nat → Nat) : (x.map f).isSome = x.isSome := by
   cases f, x using Option.map.fun_cases
-  case case1 x => simp [-Option.isSome_map']
-  case case2 =>   simp [-Option.isSome_map']
+  case case1 x => simp
+  case case2 =>   simp
 
 /--
 info: List.map.fun_cases.{u, v} (motive : {α : Type u} → {β : Type v} → (α → β) → List α → Prop)
@@ -30,3 +30,19 @@ info: List.find?.fun_cases.{u} (motive : {α : Type u} → (α → Bool) → Lis
 -/
 #guard_msgs in
 #check List.find?.fun_cases
+
+
+-- This tests shows that its not so easy to post-hoc recognize that `x` could be a parameter, but
+-- `y` should be a target of the `fun_cases` principle (or the other way around)
+def areTheseTargetsUnchanged (x y : Nat) : Bool :=
+  if _ : x = y then
+    true
+  else
+    false
+
+/--
+info: areTheseTargetsUnchanged.fun_cases (motive : Nat → Nat → Prop) (case1 : ∀ (y : Nat), motive y y)
+  (case2 : ∀ (x y : Nat), ¬x = y → motive x y) (x y : Nat) : motive x y
+-/
+#guard_msgs in
+#check areTheseTargetsUnchanged.fun_cases

tests/lean/run/funinduction_ident.lean

@@ -14,14 +14,27 @@ def append : (xs ys : List α) → List α
 namespace ListEx
 
 theorem map_id (xs : List α) : map id xs = xs := by
-  fun_induction map <;> simp_all only [map, id]
+  fun_induction map <;> simp_all only [id]
 
--- This works because collect ignores `.dropped` arguments
+-- This would work with the non-unfolding functional induction lemma, because there the function
+-- argument to `map` is `.dropped`. But since we use the unfolding lemma it doesn't anymore:
 
+/--
+error: found more than one suitable call of 'map' in the goal. Please include the desired arguments.
+-/
+#guard_msgs in
 theorem map_map (f : α → β) (g : β → γ) xs :
   map g (map f xs) = map (g ∘ f) xs := by
   fun_induction map <;> simp_all only [map, Function.comp]
 
+-- With `set_option tactic.fun_induction.unfolding false` this works, because the function
+-- argument to `map` is ignored when checking for a unique suitable call.
+
+theorem map_map' (f : α → β) (g : β → γ) xs :
+  map g (map f xs) = map (g ∘ f) xs := by
+  set_option tactic.fun_induction.unfolding false in
+  fun_induction map <;> simp_all only [map, Function.comp]
+
 -- This should genuinely not work, but have a good error message
 
 /--
@@ -49,20 +62,20 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
 ih1✝ : P (ackermann (n✝, 1))
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 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))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann p) := by
@@ -74,17 +87,17 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann (0, m✝))
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
-⊢ P (ackermann (n✝.succ, 0))
+⊢ P (ackermann (n✝, 1))
 
 case case3
 P : Nat → Prop
 n✝ m✝ : Nat
-⊢ P (ackermann (n✝.succ, m✝.succ))
+⊢ P (ackermann (n✝, ackermann (n✝ + 1, m✝)))
 -/
 #guard_msgs in
 example : P (ackermann p) := by
@@ -113,20 +126,20 @@ error: unsolved goals
 case case1
 P : Nat → Prop
 m✝ : Nat
-⊢ P (ackermann 0 m✝)
+⊢ P (m✝ + 1)
 
 case case2
 P : Nat → Prop
 n✝ : Nat
 ih1✝ : P (ackermann n✝ 1)
-⊢ P (ackermann n✝.succ 0)
+⊢ P (ackermann n✝ 1)
 
 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)
+⊢ P (ackermann n✝ (ackermann (n✝ + 1) m✝))
 -/
 #guard_msgs in
 example : P (ackermann n m) := by
@@ -150,7 +163,7 @@ case case1
 α : Type u_1
 P : List α → Prop
 inc ms✝ : List α
-⊢ P (ackermann inc [] ms✝)
+⊢ P (ms✝ ++ inc)
 
 case case2
 α : Type u_1
@@ -159,7 +172,7 @@ inc : List α
 head✝ : α
 ns✝ : List α
 ih1✝ : P (ackermann inc ns✝ inc)
-⊢ P (ackermann inc (head✝ :: ns✝) [])
+⊢ P (ackermann inc ns✝ inc)
 
 case case3
 α : Type u_1
@@ -171,7 +184,7 @@ 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✝))
+⊢ P (ackermann inc ns✝ (ackermann inc (n✝ :: ns✝) ms✝))
 -/
 #guard_msgs in
 example : P (ackermann inc n m) := by
@@ -193,18 +206,18 @@ termination_by structural x => x
 error: tactic 'fail' failed
 case case1
 P : Nat → Prop
-⊢ P (fib 0)
+⊢ P 0
 
 case case2
 P : Nat → Prop
-⊢ P (fib 1)
+⊢ P 1
 
 case case3
 P : Nat → Prop
 n✝ : Nat
 ih2✝ : P (fib n✝)
 ih1✝ : P (fib (n✝ + 1))
-⊢ P (fib n✝.succ.succ)
+⊢ P (fib n✝ + fib (n✝ + 1))
 -/
 #guard_msgs in
 example : P (fib n) := by
@@ -241,19 +254,19 @@ error: tactic 'fail' failed
 case case1
 P : Nat → Prop
 inc : Nat
-⊢ P (fib 2 0)
+⊢ P 0
 
 case case2
 P : Nat → Prop
 inc : Nat
-⊢ P (fib 2 1)
+⊢ P 2
 
 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)
+⊢ P (fib 2 n✝ + fib 2 (n✝ + 1))
 -/
 #guard_msgs in
 example : P (fib 2 n) := by
@@ -310,7 +323,7 @@ namespace Nonrec
 
 def foo := 1
 
-/-- error: no functional cases theorem for 'foo', or function is mutually recursive -/
+/-- error: no functional induction theorem for 'foo', or function is mutually recursive -/
 #guard_msgs in
 example : True := by
   fun_induction foo
@@ -333,7 +346,7 @@ def Tree.size_aux : List (Tree α) → Nat
   | t :: ts => size t + size_aux ts
 end
 
-/-- error: no functional cases theorem for 'Tree.size', or function is mutually recursive -/
+/-- error: no functional induction theorem for 'Tree.size', or function is mutually recursive -/
 #guard_msgs in
 example (t : Tree α) : True := by
   fun_induction Tree.size

tests/lean/run/grind_heapsort.lean

@@ -1,3 +1,4 @@
+import Lean
 set_option grind.warning false
 
 /-
@@ -45,24 +46,8 @@ def siftDown (a : Array Int) (root : Nat) (e : Nat) (h : e ≤ a.size := by grin
     a
 termination_by e - root
 
-/-
-Function induction for `siftDown` yields three cases, but we only have
-one equation lemma (`siftDown.eq_1`). This mismatch can complicate proofs
-by leading to loops in `simp`. `grind` also gets lost on case-analysis.
-
-Another issue: function induction does not erase `autoParam` from hypotheses.
-
-Remark: while editing this comment, `siftDown` above was being recompiled by Lean :(
--/
-#check siftDown.induct
-#check siftDown.eq_1
-
-example : (siftDown a root e h).size = a.size := by
-   -- faster than the following theorem since unfolds siftDown only in the target
-   fun_induction siftDown <;> unfold siftDown <;> grind
-
 @[grind] theorem siftDown_size : (siftDown a root e h).size = a.size := by
-   fun_induction siftDown <;> grind (splits := 9) [siftDown]
+   fun_induction siftDown <;> grind
 
 def heapify (a : Array Int) : Array Int :=
   let start := parent (a.size - 1) + 1

tests/lean/run/grind_ite.lean

@@ -154,7 +154,7 @@ theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by
-  fun_induction normalize with (unfold normalize <;> grind (gen := 8) (splits := 8))
+  fun_induction normalize <;> grind (gen := 8) (splits := 8)
 
 /-
 We recall the statement of the if-normalization problem.

tests/lean/run/grind_try_trace.lean

@@ -146,13 +146,13 @@ def map (f : α → β) : List α → List β
 
 /--
 info: Try these:
-• (fun_induction map) <;> grind [= map]
-• (fun_induction map) <;> grind only [map]
+• (fun_induction map f xs) <;> grind [= map]
+• (fun_induction map f xs) <;> grind only [map]
 -/
 #guard_msgs (info) in
 theorem map_map (f : α → β) (g : β → γ) xs :
   map g (map f xs) = map (fun x => g (f x)) xs := by
-  try? -- NB: Multiple calls to `xs.map`, but they differ only in ignore arguments
+  try?
 
 
 def foo : Nat → Nat
@@ -160,10 +160,16 @@ def foo : Nat → Nat
   | x+1 => foo x - 1
 
 /--
-info: Try this: ·
-  fun_induction foo
-  · grind [= foo]
-  · sorry
+info: Try these:
+• · fun_induction foo
+    · simp
+    · sorry
+• · fun_induction foo
+    · grind
+    · sorry
+• · fun_induction foo
+    · simp_all
+    · sorry
 -/
 #guard_msgs (info) in
 example : foo x > 0 := by
@@ -190,8 +196,8 @@ info: Try these:
 • (fun_induction bla) <;> grind
 • (fun_induction bla) <;> simp_all
 • (fun_induction bla) <;> simp [*]
-• (fun_induction bla) <;> simp only [bla, List.length_reverse, *]
-• (fun_induction bla) <;> grind only [List.length_reverse, bla]
+• (fun_induction bla) <;> simp only [List.length_reverse, *]
+• (fun_induction bla) <;> grind only [List.length_reverse]
 -/
 #guard_msgs (info) in
 example : (bla xs ys).length = ys.length := by

tests/lean/run/issue7550.lean

@@ -35,13 +35,13 @@ hfuel✝ : x✝ < fuel✝.succ
 h✝ : 0 < y ∧ y ≤ x✝
 this✝ : x✝ - y < x✝
 ih1✝ : Bug.divCore (x✝ - y) y fuel✝ ⋯ = 42
-⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
+⊢ Bug.divCore (x✝ - y) y fuel✝ ⋯ + 1 = 42
 
 case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : ¬(0 < y ∧ y ≤ x✝)
-⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
+⊢ 0 = 42
 -/
 #guard_msgs(error) in
 protected theorem divCore_eq_div : Bug.divCore x y fuel h = 42 := by
@@ -56,17 +56,17 @@ hfuel✝ : x✝ < fuel✝.succ
 h✝ : 0 < y ∧ y ≤ x✝
 this✝ : x✝ - y < x✝
 ih1✝ : Bug.divCore (x✝ - y) y fuel✝ ⋯ = 42
-⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
+⊢ Bug.divCore (x✝ - y) y fuel✝ ⋯ + 1 = 42
 
 case case2
 x y fuel x✝ fuel✝ : Nat
 hfuel✝ : x✝ < fuel✝.succ
 h✝ : ¬(0 < y ∧ y ≤ x✝)
-⊢ Bug.divCore x✝ y fuel✝.succ hfuel✝ = 42
+⊢ 0 = 42
 -/
 #guard_msgs in
 protected theorem divCore_eq_div' : Bug.divCore x y fuel h = 42 := by
-  induction x, fuel, h using Bug.divCore.induct y
+  induction x, fuel, h using Bug.divCore.induct_unfolding y
   fail
 
 end Bug

tests/lean/run/issue8293.lean

@@ -0,0 +1,57 @@
+set_option linter.unusedVariables false
+
+inductive MyVec (α : Type u) : Nat → Type u where
+  | nil : MyVec α 0
+  | cons : α → MyVec α n → MyVec α (n + 1)
+
+def test (f : Unit → MyVec α n) : Nat :=
+  match f () with
+  | .nil => 52
+  | .cons _ _ => 421
+
+/--
+info: test.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
+  (case1 :
+    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
+      f () = MyVec.nil →
+        motive f
+          (match 0, f (), f with
+          | .(0), MyVec.nil, f => 52
+          | .(n + 1), MyVec.cons a a_1, f => 421))
+  (case2 :
+    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
+      f () = MyVec.cons a a_1 →
+        motive f
+          (match n + 1, f (), f with
+          | .(0), MyVec.nil, f => 52
+          | .(n + 1), MyVec.cons a a_2, f => 421))
+  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
+-/
+#guard_msgs(pass trace, all) in
+#check test.fun_cases_unfolding
+
+def alsoTest (f : Unit → MyVec α n) : Nat :=
+  match h : f () with
+  | .nil => 52
+  | .cons _ _ => 421
+
+/--
+info: alsoTest.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
+  (case1 :
+    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
+      f () = MyVec.nil →
+        motive f
+          (match h : 0, h : f (), f with
+          | .(0), MyVec.nil, f_1 => 52
+          | .(n + 1), MyVec.cons a a_1, f_1 => 421))
+  (case2 :
+    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
+      f () = MyVec.cons a a_1 →
+        motive f
+          (match h : n + 1, h : f (), f with
+          | .(0), MyVec.nil, f_1 => 52
+          | .(n_1 + 1), MyVec.cons a a_2, f_1 => 421))
+  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
+-/
+#guard_msgs(pass trace, all) in
+#check alsoTest.fun_cases_unfolding