From 466ef74ccc024e334e9c78d9e008d3f7612f9ccf Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 26 Mar 2024 14:36:24 +0100
Subject: [PATCH] feat: functional induction for structural recursion (#3738)

This extends `derive_functional_induction` to work with structural
recursion as well.

It produces the less general, more concrete induction rule where the
induction hypothesis is
specialized for every argument of the recursive call, not just the the
one that the function
is recursing on.

Care is taken so that the induction principle and it's motive take the
arguments in the same
order as the original function.

While I was it, also makes sure that the order of the cases in the
induction principle matches
the order of recursive calls in the function better.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
---
 RELEASES.md                                   |  10 +-
 src/Lean/Meta/Match/MatcherApp/Transform.lean |   5 +-
 src/Lean/Meta/Tactic/FunInd.lean              | 463 ++++++++++++------
 tests/lean/run/funind_demo.lean               |   2 +-
 tests/lean/run/funind_expr.lean               |   2 +-
 tests/lean/run/funind_fewer_levels.lean       |  22 +-
 tests/lean/run/funind_structural.lean         | 230 +++++++++
 tests/lean/run/funind_tests.lean              |  83 ++--
 8 files changed, 623 insertions(+), 194 deletions(-)
 create mode 100644 tests/lean/run/funind_structural.lean

diff --git a/RELEASES.md b/RELEASES.md
index 81934c19b3ba..6625d29201f6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -23,9 +23,8 @@ v4.8.0 (development in progress)
 
 * New command `derive_functional_induction`:
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction
+  principle** is created that is tailored to proofs about that function. For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
@@ -41,6 +40,11 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
 * The termination checker now recognizes more recursion patterns without an
   explicit `termination_by`. In particular the idiom of counting up to an upper
   bound, as in
diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index 6715f05559bf..4d304e6d5922 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -291,7 +291,7 @@ def transform
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
     unless (← isTypeCorrect aux1) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux1}"
+      logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}"
       check aux1
     let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1)
 
@@ -299,7 +299,7 @@ def transform
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
     unless (← isTypeCorrect aux2) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux2}"
+      logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
       check aux2
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2)
 
@@ -339,7 +339,6 @@ def transform
     let aux := mkApp aux motive'
     let aux := mkAppN aux discrs'
     unless (← isTypeCorrect aux) do
-      -- check aux
       logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux)
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 8db1be3f1004..05c2de08fd68 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -14,13 +14,14 @@ import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.Command
+import Lean.Meta.Tactic.ElimInfo
 
 /-!
-This module contains code to derive, from the definition of a recursive function
-(or mutually recursive functions) defined by well-founded recursion, a
-**functional induction principle** tailored to proofs about that function(s). For
-example from:
+This module contains code to derive, from the definition of a recursive function (structural or
+well-founded, possibly mutual), a **functional induction principle** tailored to proofs about that
+function(s).
 
+For example from:
 ```
 def ackermann : Nat → Nat → Nat
   | 0, m => m + 1
@@ -59,7 +60,7 @@ by `MVarId.cleanup`).
 Mutual recursion is supported and results in multiple motives.
 
 
-## Implementation overview
+## Implementation overview (well-founded recursion)
 
 For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
@@ -129,6 +130,8 @@ For a non-mutual, unary function `foo` (or else for the `_unary` function), we
 
 The resulting term then becomes `foo.induct` at its inferred type.
 
+## Implementation overview (mutual/non-unary well-founded recursion)
+
 If `foo` is not unary and/or part of a mutual reduction, then the induction theorem for `foo._unary`
 (i.e. the unary non-mutual recursion function produced by the equation compiler)
 of the form
@@ -154,8 +157,30 @@ foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
   (x : a) → (y : b) → motive1 x y
 ```
 
+## Implementation overview (structural recursion)
+
+When handling structural recursion, the overall approach is the same, with the following
+differences:
+
+* Instead of `WellFounded.fix` we look for a `.brecOn` application, using `isBRecOnRecursor`
+
+  Despite its name, this function does *not* recognize the `.brecOn` of inductive *predicates*,
+  which we also do not support at this point.
+
+* The elaboration of structurally recursive function can handle extra arguments. We keep the
+  `motive` parameters in the original order.
+
+* The “induction hyothesis” in a `.brecOn` call is a `below x` term that contains all the possible
+  recursive calls, whic are projected out using `.fst.snd.…`. The `is_wf` flag that we pass down
+  tells us which form of induction hypothesis we are looking for.
+
+* If we have nested recursion (`foo n (foo m acc))`), then we need to infer the argument `m` of the
+  nested call `ih.fst.snd acc`. To do so reliably, we replace the `ih` with the “new `ih`”, which
+  will have type `motive m acc`, and since `motive` is a FVar we can then read off the arguments
+  off this nicely..
 -/
 
+
 set_option autoImplicit false
 
 namespace Lean.Tactic.FunInd
@@ -172,26 +197,75 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [
   let b := b.instantiate1 (.fvar x)
   k x b
 
-/-- Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an error is thrown. -/
-partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
+/-- Structural recursion only: recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd`. -/
+partial def isPProdProj (oldIH newIH : FVarId) (e : Expr) : MetaM (Option Expr) := do
+  if e.isAppOfArity ``PProd.fst 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.fst #[e'])
+    else
+      return none
+  else if e.isAppOfArity ``PProd.snd 3 then
+    if let some e' ← isPProdProj oldIH newIH e.appArg! then
+      return some (← mkAppM ``PProd.snd #[e'])
+    else
+      return none
+  else if e.isFVarOf oldIH then
+    return some (mkFVar newIH)
+  else
+    return none
+
+/--
+Structural recursion only:
+Recognizes `oldIH.fst.snd a₁ a₂` and returns `newIH.fst.snd` and `#[a₁, a₂]`.
+-/
+def isPProdProjWithArgs (oldIH newIH : FVarId) (e : Expr) : MetaM (Option (Expr × Array Expr)) := do
+  if e.isAppOf ``PProd.fst || e.isAppOf ``PProd.snd then
+    let arity := e.getAppNumArgs
+    unless 3 ≤ arity do return none
+    let args := e.getAppArgsN (arity - 3)
+    if let some e' ← isPProdProj oldIH newIH (e.stripArgsN (arity - 3)) then
+      return some (e', args)
+  return none
+
+/--
+Replace calls to oldIH back to calls to the original function. At the end, if `oldIH` occurs, an
+error is thrown.
+
+The `newIH` will not show up in the output of `foldCalls`, we use it as a helper to infer the
+argument of nested recursive calls when we have structural recursion.
+-/
+partial def foldCalls (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM Expr := do
   unless e.containsFVar oldIH do
     return e
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, _proof] := e.getAppArgs | unreachable!
-    let arg' ← foldCalls fn oldIH arg
-    return .app fn arg'
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, _proof] := e.getAppArgs | unreachable!
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      return .app fn arg'
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let t ← whnf (← inferType e')
+      let e' ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        mkLambdaFVars xs (fn.beta t'.getAppArgs)
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let e' := e'.beta args'
+      unless ← isTypeCorrect e' do
+        throwError m!"foldCalls: type incorrect after replacing recursive call:{indentExpr e'}"
+      return e'
 
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun _motiveArgs motiveBody => do
           let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
-          foldCalls fn oldIH body)
+          foldCalls is_wf fn oldIH newIH body)
         (onAlt := fun _altType alt => do
           removeLamda alt fun oldIH alt => do
-            foldCalls fn oldIH alt)
+            foldCalls is_wf fn oldIH newIH alt)
         (onRemaining := fun _ => pure #[])
       return matcherApp'.toExpr
 
@@ -203,43 +277,43 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "foldCalls: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← foldCalls fn oldIH e'
+    return ← foldCalls is_wf fn oldIH newIH e'
 
   if let some (n, t, v, b) := e.letFun? then
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFun x v' b'
 
   match e with
   | .app e1 e2 =>
-    return .app (← foldCalls fn oldIH e1) (← foldCalls fn oldIH e2)
+    return .app (← foldCalls is_wf fn oldIH newIH e1) (← foldCalls is_wf fn oldIH newIH e2)
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkLambdaFVars #[x] body'
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let body' ← foldCalls fn oldIH (body.instantiate1 x)
+      let body' ← foldCalls is_wf fn oldIH newIH (body.instantiate1 x)
       mkForallFVars #[x] body'
 
   | .letE n t v b _ =>
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← foldCalls fn oldIH (b.instantiate1 x)
+      let b' ← foldCalls is_wf fn oldIH newIH (b.instantiate1 x)
       mkLetFVars  #[x] b'
 
   | .mdata m b =>
-    return .mdata m (← foldCalls fn oldIH b)
+    return .mdata m (← foldCalls is_wf fn oldIH newIH b)
 
   | .proj t i e =>
-    return .proj t i (← foldCalls fn oldIH e)
+    return .proj t i (← foldCalls is_wf fn oldIH newIH e)
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -248,35 +322,56 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do
     throwError m!"collectIHs: cannot eliminate unsaturated call to induction hypothesis"
 
 
--- Non-tail-positions: Collect induction hypotheses
--- (TODO: Worth folding with `foldCalls`, like before?)
--- (TODO: Accumulated with a left fold)
-partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
+/-
+In non-tail-positions, we collect the induction hypotheses from all the recursive calls.
+-/
+-- We could run `collectIHs` and `foldCalls` together, and save a few traversals. Not sure if it
+-- worth the extra code complexity.
+-- Also, this way of collecting arrays is not as efficient as a left-fold, but we do not expect
+-- large arrays here.
+partial def collectIHs (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Array Expr) := do
   unless e.containsFVar oldIH do
     return #[]
 
-  if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
-    let #[arg, proof] := e.getAppArgs  | unreachable!
+  if is_wf then
+    if e.getAppNumArgs = 2 && e.getAppFn.isFVarOf oldIH then
+      let #[arg, proof] := e.getAppArgs  | unreachable!
+
+      let arg' ← foldCalls is_wf fn oldIH newIH arg
+      let proof' ← foldCalls is_wf fn oldIH newIH proof
+      let ihs ← collectIHs is_wf fn oldIH newIH arg
 
-    let arg' ← foldCalls fn oldIH arg
-    let proof' ← foldCalls fn oldIH proof
-    let ihs ← collectIHs fn oldIH newIH arg
+      return ihs.push (mkApp2 (.fvar newIH) arg' proof')
+  else
+    if let some (e', args) ← isPProdProjWithArgs oldIH newIH e then
+      let args' ← args.mapM (foldCalls is_wf fn oldIH newIH)
+      let ihs ← args.concatMapM (collectIHs is_wf fn oldIH newIH)
+      let t ← whnf (← inferType e')
+      let arity ← forallTelescopeReducing t fun xs t' => do
+        unless t'.getAppFn.isFVar do -- we expect an application of the `motive` FVar here
+          throwError m!"Unexpected type {t} of {e}: Reduced to application of {t'.getAppFn}"
+        pure xs.size
+      let e' := mkAppN e' args'[:arity]
+      let eTyp ← inferType e'
+      -- The inferred type that comes out of motive projections has beta redexes
+      let eType' := eTyp.headBeta
+      return ihs.push (← mkExpectedTypeHint e' eType')
 
-    return ihs.push (mkApp2 (.fvar newIH) arg' proof')
 
   if let some (n, t, v, b) := e.letFun? then
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
+
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
 
       let matcherApp' ← matcherApp.transform
-        (onParams := foldCalls fn oldIH)
+        (onParams := foldCalls is_wf fn oldIH newIH)
         (onMotive := fun xs _body => do
           -- Remove the old IH that was added in mkFix
           let eType ← newIH.getType
@@ -294,7 +389,7 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let altIHs ← collectIHs fn oldIH' newIH'.fvarId! alt
+              let altIHs ← collectIHs is_wf fn oldIH' newIH'.fvarId! alt
               let altIH ← mkAndIntroN altIHs
               mkLambdaFVars #[newIH'] altIH)
         (onRemaining := fun _ => pure #[mkFVar newIH])
@@ -310,40 +405,40 @@ partial def collectIHs (fn : Expr) (oldIH newIH : FVarId) (e : Expr) : MetaM (Ar
     let e' ← withTransparency .all do whnf e
     if e == e' then
       throwError "collectIHs: cannot reduce application of {e.getAppFn} in {indentExpr e} "
-    return ← collectIHs fn oldIH newIH e'
+    return ← collectIHs is_wf fn oldIH newIH e'
 
   if e.getAppArgs.any (·.isFVarOf oldIH) then
     throwError "collectIHs: could not collect recursive calls from call {indentExpr e}"
 
   match e with
   | .letE n t v b _ =>
-    let ihs1 ← collectIHs fn oldIH newIH v
-    let v' ← foldCalls fn oldIH v
+    let ihs1 ← collectIHs is_wf fn oldIH newIH v
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t v' fun x => do
-      let ihs2 ← collectIHs fn oldIH newIH (b.instantiate1 x)
+      let ihs2 ← collectIHs is_wf fn oldIH newIH (b.instantiate1 x)
       let ihs2 ← ihs2.mapM (mkLetFVars (usedLetOnly := true) #[x] ·)
       return ihs1 ++ ihs2
 
   | .app e1 e2 =>
-    return (← collectIHs fn oldIH newIH e1) ++ (← collectIHs fn oldIH newIH e2)
+    return (← collectIHs is_wf fn oldIH newIH e1) ++ (← collectIHs is_wf fn oldIH newIH e2)
 
   | .proj _ _ e =>
-    return ← collectIHs fn oldIH newIH e
+    return ← collectIHs is_wf fn oldIH newIH e
 
   | .forallE n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .lam n t body bi =>
-    let t' ← foldCalls fn oldIH t
+    let t' ← foldCalls is_wf fn oldIH newIH t
     return ← withLocalDecl n bi t' fun x => do
-      let ihs ← collectIHs fn oldIH newIH (body.instantiate1 x)
+      let ihs ← collectIHs is_wf fn oldIH newIH (body.instantiate1 x)
       ihs.mapM (mkLambdaFVars (usedOnly := true) #[x])
 
   | .mdata _m b =>
-    return ← collectIHs fn oldIH newIH b
+    return ← collectIHs is_wf fn oldIH newIH b
 
   | .sort .. | .lit .. | .const .. | .mvar .. | .bvar .. =>
     unreachable! -- cannot contain free variables, so early exit above kicks in
@@ -393,9 +488,9 @@ abbrev M α := StateT (Array MVarId) MetaM α
 
 
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypthesis.  -/
-def buildInductionCase (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
+def buildInductionCase (is_wf : Bool) (fn : Expr) (oldIH newIH : FVarId) (toClear toPreserve : Array FVarId)
     (goal : Expr) (IHs : Array Expr) (e : Expr) : M Expr := do
-  let IHs := IHs ++ (← collectIHs fn oldIH newIH e)
+  let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH e)
   let IHs ← deduplicateIHs IHs
 
   let mvar ← mkFreshExprSyntheticOpaqueMVar goal (tag := `hyp)
@@ -448,30 +543,45 @@ Builds an expression of type `goal` by replicating the expression `e` into its t
 where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
 as `MVars` as it goes.
 -/
-partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
+partial def buildInductionBody (is_wf : Bool) (fn : Expr) (toClear toPreserve : Array FVarId)
     (goal : Expr) (oldIH newIH : FVarId) (IHs : Array Expr) (e : Expr) : M Expr := do
   -- logInfo m!"buildInductionBody {e}"
 
-  if e.isDIte then
-    let #[_α, c, h, t, f] := e.getAppArgs | unreachable!
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH c)
-    let c' ← foldCalls fn oldIH c
-    let h' ← foldCalls fn oldIH h
+  -- if-then-else cause case split:
+  match_expr e with
+  | ite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
+    let t' ← withLocalDecl `h .default c' fun h => do
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      mkLambdaFVars #[h] t'
+    let f' ← withLocalDecl `h .default (mkNot c') fun h => do
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      mkLambdaFVars #[h] f'
+    let u ← getLevel goal
+    return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | dite _α c h t f =>
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH c)
+    let c' ← foldCalls is_wf fn oldIH newIH c
+    let h' ← foldCalls is_wf fn oldIH newIH h
     let t' ← withLocalDecl `h .default c' fun h => do
       let t ← instantiateLambda t #[h]
-      let t' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
+      let t' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs t
       mkLambdaFVars #[h] t'
     let f' ← withLocalDecl `h .default (mkNot c') fun h => do
       let f ← instantiateLambda f #[h]
-      let f' ← buildInductionBody fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
+      let f' ← buildInductionBody is_wf fn toClear (toPreserve.push h.fvarId!) goal oldIH newIH IHs f
       mkLambdaFVars #[h] f'
     let u ← getLevel goal
     return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
+  | _ =>
 
+  -- match and casesOn application cause case splitting
   if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
     -- Collect IHs from the parameters and discrs of the matcher
     let paramsAndDiscrs := matcherApp.params ++ matcherApp.discrs
-    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs fn oldIH newIH ·))
+    let IHs := IHs ++ (← paramsAndDiscrs.concatMapM (collectIHs is_wf fn oldIH newIH ·))
 
     -- Calculate motive
     let eType ← newIH.getType
@@ -483,13 +593,13 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
     if matcherApp.remaining.size == 1 && matcherApp.remaining[0]!.isFVarOf oldIH then
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := (foldCalls fn oldIH ·))
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
           removeLamda alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
-              let alt' ← buildInductionBody fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
+              let alt' ← buildInductionBody is_wf fn (toClear.push newIH'.fvarId!) toPreserve goal' oldIH' newIH'.fvarId! IHs alt
               mkLambdaFVars #[newIH'] alt')
         (onRemaining := fun _ => pure #[.fvar newIH])
       return matcherApp'.toExpr
@@ -502,29 +612,29 @@ partial def buildInductionBody (fn : Expr) (toClear toPreserve : Array FVarId)
 
       let matcherApp' ← matcherApp.transform (useSplitter := true)
         (addEqualities := mask.map not)
-        (onParams := (foldCalls fn oldIH ·))
+        (onParams := (foldCalls is_wf fn oldIH newIH ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
         (onAlt := fun expAltType alt => do
-          buildInductionBody fn toClear toPreserve expAltType oldIH newIH IHs alt)
+          buildInductionBody is_wf fn toClear toPreserve expAltType oldIH newIH IHs alt)
       return matcherApp'.toExpr
 
   if let .letE n t v b _ := e then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLetDecl n t' v' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFVars #[x] b'
 
   if let some (n, t, v, b) := e.letFun? then
-    let IHs := IHs ++ (← collectIHs fn oldIH newIH v)
-    let t' ← foldCalls fn oldIH t
-    let v' ← foldCalls fn oldIH v
+    let IHs := IHs ++ (← collectIHs is_wf fn oldIH newIH v)
+    let t' ← foldCalls is_wf fn oldIH newIH t
+    let v' ← foldCalls is_wf fn oldIH newIH v
     return ← withLocalDecl n .default t' fun x => do
-      let b' ← buildInductionBody fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
+      let b' ← buildInductionBody is_wf fn toClear toPreserve goal oldIH newIH IHs (b.instantiate1 x)
       mkLetFun x v' b'
 
-  buildInductionCase fn oldIH newIH toClear toPreserve goal IHs e
+  liftM <| buildInductionCase is_wf fn oldIH newIH toClear toPreserve goal IHs e
 
 /--
 Given an expression `e` with metavariables
@@ -555,17 +665,86 @@ def abstractIndependentMVars (mvars : Array MVarId) (x : FVarId) (e : Expr) : Me
         mvar.assign x
       mkLambdaFVars xs (← instantiateMVars e)
 
-partial def findFixF {α} (name : Name) (e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
-  lambdaTelescope e fun params body => do
-    if body.isAppOf ``WellFounded.fixF then
-      k params body
-    else if body.isAppOf ``WellFounded.fix then
-      findFixF name (← unfoldDefinition body) fun args e' => k (params ++ args) e'
-    else
-      throwError m!"Function {name} does not look like a function defined by well-founded " ++
-        m!"recursion.\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
-        m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
-        "function."
+/--
+This function looks that the body of a recursive function and looks for either users of
+`fix`, `fixF` or a `.brecOn`, and abstracts over the differences between them. It passes
+to the continuation
+
+* whether we are using well-founded recursion
+* the fixed parameters of the function body
+* the varying parameters of the function body (this includes both the targets of the
+  recursion and extra parameters passed to the recursor)
+* the position of the motive/induction hypothesis in the body's arguments
+* the body, as passed to the recursor. Expected to be a lambda that takes the
+  varying paramters and the motive
+* a function to re-assemble the call with a new Motive. The resulting expression expects
+  the new body next, so that the expected type of the body can be inferred
+* a function to finish assembling the call with the new body.
+-/
+def findRecursor {α} (name : Name) (varNames : Array Name) (e : Expr)
+    (k :(is_wf : Bool) →
+        (fixedParams : Array Expr) →
+        (varyingParams : Array Expr) →
+        (motivePosInBody : Nat) →
+        (body : Expr) →
+        (mkAppMotive : Expr → MetaM Expr) →
+        (mkAppBody : Expr → Expr → Expr) →
+        MetaM α) :
+    MetaM α := do
+  -- Uses of WellFounded.fix can be partially applied. Here we eta-expand the body
+  -- to avoid dealing with this
+  let e ← lambdaTelescope e fun params body => do mkLambdaFVars params (← etaExpand body)
+  lambdaTelescope e fun params body => body.withApp fun f args => do
+    MatcherApp.withUserNames params varNames do
+      if not f.isConst then err else
+      if isBRecOnRecursor (← getEnv) f.constName! then
+        let elimInfo ← getElimExprInfo f
+        let targets : Array Expr := elimInfo.targetsPos.map (args[·]!)
+        let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]!
+        let extraArgs : Array Expr := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size + 1:]
+
+        let fixedParams := params.filter fun x => !(targets.contains x || extraArgs.contains x)
+        let varyingParams := params.filter fun x => targets.contains x || extraArgs.contains x
+        unless params == fixedParams ++ varyingParams do
+          throwError "functional induction: unexpected order of fixed and varying parameters:{indentExpr e}"
+        -- we assume the motive's universe parameter is the first
+        unless 1 ≤ f.constLevels!.length do
+          throwError "functional induction: unexpected recursor: {f} has no universe parameters"
+        let us := f.constLevels!.set 0 levelZero
+
+        let value := mkAppN (.const f.constName us) (args[:elimInfo.motivePos])
+        k false fixedParams varyingParams targets.size body
+          (fun newMotive => do
+            -- We may have to reorder the parameters for motive before passing it to brec
+            let brecMotive ← mkLambdaFVars targets
+              (← mkForallFVars extraArgs (mkAppN newMotive varyingParams))
+            return mkAppN (mkApp value brecMotive) targets)
+          (fun value newBody => mkAppN (.app value newBody) extraArgs)
+      else if Name.isSuffixOf `brecOn f.constName! then
+        throwError m!"Function {name} is defined in a way not supported by functional induction, " ++
+          "for example by recursion over an inductive predicate."
+      else match_expr body with
+      | WellFounded.fixF α rel _motive body target acc =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fixF [f.constLevels![0]!, levelZero]
+        k true params.pop #[params.back] 1 body
+          (fun newMotive => pure (mkApp3 value α rel newMotive))
+          (fun value newBody => mkApp2 value newBody acc)
+      | WellFounded.fix α _motive rel wf body target =>
+        unless params.back == target do
+          throwError "functional induction: expected the target as last parameter{indentExpr e}"
+        let value := .const ``WellFounded.fix [f.constLevels![0]!, levelZero]
+        k true params.pop #[target] 1 body
+          (fun newMotive => pure (mkApp4 value α newMotive rel wf))
+          (fun value newBody => mkApp2 value newBody target)
+      | _ => err
+  where
+    err := throwError m!"Function {name} does not look like a function defined by recursion." ++
+      m!"\nNB: If {name} is not itself recursive, but contains an inner recursive " ++
+      m!"function (via `let rec` or `where`), try `{name}.go` where `go` is name of the inner " ++
+      "function."
+
 
 /--
 Given a definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle
@@ -576,62 +755,60 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
   if ← hasConst inductName then return inductName
 
   let info ← getConstInfoDefn name
-  findFixF name info.value fun params body => body.withApp fun f fixArgs => do
-    -- logInfo f!"{fixArgs}"
-    unless params.size > 0 do
-      throwError "Value of {name} is not a lambda application"
-    unless f.isConstOf ``WellFounded.fixF do
-      throwError "Term isn’t application of {``WellFounded.fixF}, but of {f}"
-    let #[argType, rel, _motive, body, arg, acc] := fixArgs |
-      throwError "Application of WellFounded.fixF has wrong arity {fixArgs.size}"
-    unless ← isDefEq arg params.back do
-      throwError "fixF application argument {arg} is not function argument "
-    let [argLevel, _motiveLevel] := f.constLevels! | unreachable!
-
-    let motiveType ← mkArrow argType (.sort levelZero)
-    withLocalDecl `motive .default motiveType fun motive => do
-
-    let e' := mkApp3 (.const ``WellFounded.fixF [argLevel, levelZero]) argType rel motive
-    let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) params.pop
-    let (body', mvars) ← StateT.run (s := {}) <| forallTelescope (← inferType e').bindingDomain! fun xs _ => do
-      let #[param, genIH] := xs | unreachable!
-      -- open body with the same arg
-      let body ← instantiateLambda body #[param]
-      removeLamda body fun oldIH body => do
-        let body' ← buildInductionBody fn #[genIH.fvarId!] #[] (.app motive param) oldIH genIH.fvarId! #[] body
-        if body'.containsFVar oldIH then
-          throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
-        mkLambdaFVars #[param, genIH] body'
-
-    let e' := mkApp3 e' body' arg acc
-
-    let e' ← mkLambdaFVars #[params.back] e'
-    let e' ← abstractIndependentMVars mvars motive.fvarId! e'
-    let e' ← mkLambdaFVars #[motive] e'
-
-    -- We could pass (usedOnly := true) below, and get nicer induction principles that
-    -- do do not mention odd unused parameters.
-    -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
-    -- that derives them from an function application in the goal) is harder, as
-    -- one would have to infer or keep track of which parameters to pass.
-    -- So for now lets just keep them around.
-    let e' ← mkLambdaFVars (binderInfoForMVars := .default) params.pop e'
-    let e' ← instantiateMVars e'
-
-    let eTyp ← inferType e'
-    let eTyp ← elimOptParam eTyp
-    -- logInfo m!"eTyp: {eTyp}"
-    unless (← isTypeCorrect e') do
-      logError m!"failed to derive induction priciple:{indentExpr e'}"
-      check e'
 
-    let params := (collectLevelParams {} eTyp).params
-    -- Prune unused level parameters, preserving the original order
-    let us := info.levelParams.filter (params.contains ·)
+  let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName)
 
-    addDecl <| Declaration.thmDecl
-      { name := inductName, levelParams := us, type := eTyp, value := e' }
-    return inductName
+  let e' ← findRecursor name varNames info.value
+    fun is_wf fixedParams varyingParams motivePosInBody body mkAppMotive mkAppBody => do
+      let motiveType ← mkForallFVars varyingParams (.sort levelZero)
+      withLocalDecl `motive .default motiveType fun motive => do
+      let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) fixedParams
+      let e' ← mkAppMotive motive
+      check e'
+      let (body', mvars) ← StateT.run (s := {}) do
+        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+          let arity := varyingParams.size + 1
+          if xs.size ≠ arity then
+            throwError "expected recursor argument to take {arity} parameters, got {xs}" else
+          let targets : Array Expr := xs[:motivePosInBody]
+          let genIH := xs[motivePosInBody]!
+          let extraParams := xs[motivePosInBody+1:]
+          -- open body with the same arg
+          let body ← instantiateLambda body targets
+          removeLamda body fun oldIH body => do
+            let body ← instantiateLambda body extraParams
+            let body' ← buildInductionBody is_wf fn #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! #[] body
+            if body'.containsFVar oldIH then
+              throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}"
+            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+      let e' := mkAppBody e' body'
+      let e' ← mkLambdaFVars varyingParams e'
+      let e' ← abstractIndependentMVars mvars motive.fvarId! e'
+      let e' ← mkLambdaFVars #[motive] e'
+
+      -- We could pass (usedOnly := true) below, and get nicer induction principles that
+      -- do do not mention odd unused parameters.
+      -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
+      -- that derives them from an function application in the goal) is harder, as
+      -- one would have to infer or keep track of which parameters to pass.
+      -- So for now lets just keep them around.
+      let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e'
+      instantiateMVars e'
+
+  unless (← isTypeCorrect e') do
+    logError m!"failed to derive induction priciple:{indentExpr e'}"
+    check e'
+
+  let eTyp ← inferType e'
+  let eTyp ← elimOptParam eTyp
+  -- logInfo m!"eTyp: {eTyp}"
+  let params := (collectLevelParams {} eTyp).params
+  -- Prune unused level parameters, preserving the original order
+  let us := info.levelParams.filter (params.contains ·)
+
+  addDecl <| Declaration.thmDecl
+    { name := inductName, levelParams := us, type := eTyp, value := e' }
+  return inductName
 
 /--
 In the type of `value`, reduces
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index acaa5621e526..bfae65dc85cf 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -27,7 +27,7 @@ derive_functional_induction Tree.rev
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
 -/
 #guard_msgs in
 #check Tree.rev.induct
diff --git a/tests/lean/run/funind_expr.lean b/tests/lean/run/funind_expr.lean
index 0161fef6298e..3d6177baf509 100644
--- a/tests/lean/run/funind_expr.lean
+++ b/tests/lean/run/funind_expr.lean
@@ -70,7 +70,7 @@ info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), mot
       (∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
           a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False) →
         motive a → motive b → motive (a.and b))
-  (x : Expr) : motive x
+  (e : Expr) : motive e
 -/
 #guard_msgs in
 #check Expr.typeCheck.induct
diff --git a/tests/lean/run/funind_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean
index 111ee45f4ac2..79a5c9b30005 100644
--- a/tests/lean/run/funind_fewer_levels.lean
+++ b/tests/lean/run/funind_fewer_levels.lean
@@ -4,6 +4,26 @@ This test checks if the functional induction principle has fewer universe parame
 if the original function has a parameter that disappears.
 -/
 
+namespace Structural
+def foo.{u} : Nat → PUnit.{u}
+| 0 => .unit
+| n+1 => foo n
+
+derive_functional_induction foo
+/--
+info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
+-/
+#guard_msgs in
+#check foo.induct
+
+example : foo n = .unit := by
+  induction n using foo.induct with
+  | case1 => unfold foo; rfl
+  | case2 n ih => unfold foo; exact ih
+
+end Structural
+
 namespace WellFounded
 def foo.{u,v} {α : Type v} : List α  → PUnit.{u}
 | [] => .unit
@@ -13,7 +33,7 @@ termination_by xs => xs
 derive_functional_induction foo
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (x : List α) : motive x
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
new file mode 100644
index 000000000000..d91cec333b47
--- /dev/null
+++ b/tests/lean/run/funind_structural.lean
@@ -0,0 +1,230 @@
+import Lean.Elab.Command
+
+/-!
+This module tests functional induction principles on *structurally* recursive functions.
+-/
+
+def fib : Nat → Nat
+  | 0 | 1 => 0
+  | n+2 => fib n + fib (n+1)
+
+derive_functional_induction fib
+/--
+info: 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
+
+
+def binary : Nat → Nat → Nat
+  | 0, acc | 1, acc => 1 + acc
+  | n+2, acc => binary n (binary (n+1) acc)
+
+derive_functional_induction binary
+/--
+info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
+  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
+  ∀ (a a_1 : Nat), motive a a_1
+-/
+#guard_msgs in
+#check binary.induct
+
+
+-- Different parameter order
+def binary' : Bool → Nat → Bool
+  | acc, 0 | acc , 1 => not acc
+  | acc, n+2 => binary' (binary' acc (n+1)) n
+
+derive_functional_induction binary'
+/--
+info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
+  (case2 : ∀ (acc : Bool), motive acc 1)
+  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) :
+  ∀ (a : Bool) (a_1 : Nat), motive a a_1
+-/
+#guard_msgs in
+#check binary'.induct
+
+def zip {α β} : List α → List β → List (α × β)
+  | [], _ => []
+  | _, [] => []
+  | x::xs, y::ys => (x, y) :: zip xs ys
+
+derive_functional_induction zip
+/--
+info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
+  (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (x : List α), (x = [] → False) → motive x [])
+  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
+  ∀ (a : List α) (a_1 : List β), motive a a_1
+-/
+#guard_msgs in
+#check zip.induct
+
+/-- Lets try ot use it! -/
+theorem zip_length {α β} (xs : List α) (ys : List β) :
+    (zip xs ys).length = xs.length.min ys.length := by
+  induction xs, ys using zip.induct
+  case case1 => simp [zip]
+  case case2 => simp [zip]
+  case case3 =>
+    simp [zip, *]
+    simp [Nat.min_def]
+    split<;>split<;> omega
+
+theorem zip_get?  {α β} (as : List α) (bs : List β) :
+    (List.zip as bs).get? i = match as.get? i, bs.get? i with
+      | some a, some b => some (a, b) | _, _ => none := by
+  induction as, bs using zip.induct generalizing i
+    <;> cases i <;> simp_all
+
+-- 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)
+
+derive_functional_induction Finn.min
+/--
+info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
+  (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
+  (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
+  (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
+  {n : Nat} (m : Nat) : ∀ (a f : Finn n), motive x m a f
+-/
+#guard_msgs in
+#check Finn.min.induct
+
+
+inductive Even : Nat → Prop where
+| zero : Even 0
+| plus2 : Even n → Even (n + 2)
+
+def idEven : Even n → Even n
+| .zero => .zero
+| .plus2 p => .plus2 (idEven p)
+/--
+error: Function idEven is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
+-/
+#guard_msgs in
+derive_functional_induction idEven
+
+
+-- Acc.brecOn is not recognized by isBRecOnRecursor:
+-- run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Acc.brecOn}"
+def idAcc : Acc p x → Acc p x
+  | Acc.intro x f => Acc.intro x (fun y h => idAcc (f y h))
+/--
+error: Function idAcc is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
+-/
+#guard_msgs in
+derive_functional_induction idAcc
+
+namespace TreeExample
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+
+def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
+  match t with
+  | leaf => node leaf k v leaf
+  | node left key value right =>
+    if k < key then
+      node (left.insert k v) key value right
+    else if key < k then
+      node left key value (right.insert k v)
+    else
+      node left k v right
+
+derive_functional_induction Tree.insert
+
+/--
+info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
+  (case1 : ∀ (k : Nat) (v : β), motive Tree.leaf k v)
+  (case2 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      k < key → motive left k v → motive (left.node key value right) k v)
+  (case3 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → key < k → motive right k v → motive (left.node key value right) k v)
+  (case4 :
+    ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β),
+      ¬k < key → ¬key < k → motive (left.node key value right) k v)
+  (t : Tree β) (k : Nat) (v : β) : motive t k v
+-/
+#guard_msgs in
+#check Tree.insert.induct
+
+end TreeExample
+
+namespace Term
+
+inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
+  | nil  : HList β []
+  | cons : β i → HList β is → HList β (i::is)
+
+inductive Member : α → List α → Type
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+
+def HList.get : HList β is → Member i is → β i
+  | .cons a as, .head => a
+  | .cons _ as, .tail h => as.get h
+
+inductive Ty where
+  | nat
+  | fn : Ty → Ty → Ty
+
+@[reducible] def Ty.denote : Ty → Type
+  | nat    => Nat
+  | fn a b => a.denote → b.denote
+
+inductive Term : List Ty → Ty → Type
+  | var   : Member ty ctx → Term ctx ty
+  | const : Nat → Term ctx .nat
+  | plus  : Term ctx .nat → Term ctx .nat → Term ctx .nat
+  | app   : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
+  | lam   : Term (.cons dom ctx) ran → Term ctx (.fn dom ran)
+  | let   : Term ctx ty₁ → Term (.cons ty₁ ctx) ty₂ → Term ctx ty₂
+
+def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
+  | .var h,     env => env.get h
+  | .const n,   _   => n
+  | .plus a b,  env => a.denote env + b.denote env
+  -- the following recursive call is interesting: Here the `ty.denote` for `f`'s type
+  -- becomes a function, and thus the recursive call takes an extra argument
+  -- But in the induction principle, we have `motive f` here, which does not
+  -- take an extra argument, so we have to be careful to not pass too many arguments to it
+  | .app f a,   env => f.denote env (a.denote env)
+  | .lam b,     env => fun x => b.denote (.cons x env)
+  | .let a b,   env => b.denote (.cons (a.denote env) env)
+
+derive_functional_induction Term.denote
+
+/--
+info: Term.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)
+  (case1 : ∀ (a : List Ty) (ty : Ty) (h : Member ty a) (env : HList Ty.denote a), motive (Term.var h) env)
+  (case2 : ∀ (a : List Ty) (n : Nat) (x : HList Ty.denote a), motive (Term.const n) x)
+  (case3 :
+    ∀ (a : List Ty) (a_1 b : Term a Ty.nat) (env : HList Ty.denote a),
+      motive a_1 env → motive b env → motive (a_1.plus b) env)
+  (case4 :
+    ∀ (a : List Ty) (ty dom : Ty) (f : Term a (dom.fn ty)) (a_1 : Term a dom) (env : HList Ty.denote a),
+      motive a_1 env → motive f env → motive (f.app a_1) env)
+  (case5 :
+    ∀ (a : List Ty) (dom ran : Ty) (b : Term (dom :: a) ran) (env : HList Ty.denote a),
+      (∀ (x : dom.denote), motive b (HList.cons x env)) → motive b.lam env)
+  (case6 :
+    ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
+      motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
+  {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1
+-/
+#guard_msgs in
+#check Term.denote.induct
+
+end Term
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 88344d4cbcc4..0ca606cc950e 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -11,8 +11,8 @@ derive_functional_induction ackermann
 /--
 info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
   (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
-  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ))
-  (x : Nat × Nat) : motive x
+  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ)) :
+  ∀ (a : Nat × Nat), motive a
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -49,7 +49,7 @@ derive_functional_induction Tree.rev
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
 -/
 #guard_msgs in
 #check Tree.rev.induct
@@ -64,7 +64,7 @@ termination_by n => n
 derive_functional_induction fib
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check fib.induct
@@ -79,8 +79,8 @@ termination_by n => n
 derive_functional_induction have_tailrec
 
 /--
-info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
-  (x : Nat) : motive x
+info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
+  (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check have_tailrec.induct
@@ -96,8 +96,8 @@ termination_by n => n
 derive_functional_induction have_non_tailrec
 
 /--
-info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check have_non_tailrec.induct
@@ -116,8 +116,8 @@ info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 :
     ∀ (n : Nat),
       let h2 := ⋯;
-      motive n → motive n.succ)
-  (x : Nat) : motive x
+      motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check let_tailrec.induct
@@ -133,8 +133,8 @@ termination_by n => n
 derive_functional_induction let_non_tailrec
 
 /--
-info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check let_non_tailrec.induct
@@ -154,7 +154,7 @@ derive_functional_induction with_ite_tailrec
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -175,7 +175,7 @@ derive_functional_induction with_ite_non_tailrec
 
 /--
 info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_ite_non_tailrec.induct
@@ -191,9 +191,8 @@ termination_by n
 derive_functional_induction with_dite_non_tailrec
 
 /--
-info: with_dite_non_tailrec.induct (motive : Nat → Prop)
-(case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
-  (x : Nat) : motive x
+info: with_dite_non_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check with_dite_non_tailrec.induct
@@ -208,9 +207,8 @@ termination_by n
 derive_functional_induction with_dite_tailrec
 
 /--
-info: with_dite_tailrec.induct (motive : Nat → Prop)
-(case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
-  (case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (x : Nat) : motive x
+info: with_dite_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
+  (case2 : ∀ (x : Nat), ¬x - 1 < x → motive x) (n : Nat) : motive n
 -/
 #guard_msgs in
 #check with_dite_tailrec.induct
@@ -227,7 +225,7 @@ derive_functional_induction with_match_refining_tailrec
 
 /--
 info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
-  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (x : Nat) : motive x
+  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_refining_tailrec.induct
@@ -278,7 +276,7 @@ derive_functional_induction with_other_match_tailrec
 /--
 info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_other_match_tailrec.induct
@@ -331,8 +329,8 @@ termination_by n => n
 derive_functional_induction with_match_non_tailrec
 
 /--
-info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_non_tailrec.induct
@@ -355,8 +353,8 @@ info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : mo
       (match n with
         | 0 => motive 0
         | m => motive m) →
-        motive n.succ)
-  (x : Nat) : motive x
+        motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_match_non_tailrec_refining.induct
@@ -373,8 +371,8 @@ derive_functional_induction with_overlap
 
 /--
 info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
-  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) (x : Nat) :
-  motive x
+  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) :
+  ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check with_overlap.induct
@@ -392,7 +390,7 @@ derive_functional_induction unary
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check unary.induct
@@ -443,7 +441,7 @@ info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
         | 1 => True
         | n.succ.succ => motive n ∧ motive (n + 1)) →
         motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check match_non_tail.induct
@@ -469,7 +467,7 @@ derive_functional_induction foo
 
 /--
 info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -492,7 +490,7 @@ info: AsPattern.bar.induct (motive : Nat → Prop)
         | 0 => True
         | x@h:n.succ => motive n) →
         motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check bar.induct
@@ -526,7 +524,7 @@ decreasing_by
 derive_functional_induction foo
 /--
 info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -544,7 +542,7 @@ termination_by xs => xs
 derive_functional_induction foo
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check foo.induct
@@ -560,7 +558,7 @@ termination_by xs => xs
 derive_functional_induction bar
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
 #check bar.induct
@@ -579,12 +577,13 @@ derive_functional_induction foo
 /--
 info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check foo.induct
 
 
+set_option linter.unusedVariables false in
 def bar : Nat → Nat
   | 0 => 0
   | n+1 => match _h : n, bar n with
@@ -597,7 +596,7 @@ derive_functional_induction bar
 /--
 info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
   (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0))
-  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (x : Nat) : motive x
+  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check bar.induct
@@ -679,7 +678,7 @@ derive_functional_induction unary
 
 /--
 info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (n : Nat) : motive n
 -/
 #guard_msgs in
 #check unary.induct
@@ -745,7 +744,7 @@ info: Dite.foo.induct (motive : Nat → Prop)
     ∀ (x : Nat),
       let j := x - 1;
       ¬j < x → motive x)
-  (x : Nat) : motive x
+  (n : Nat) : motive n
 -/
 #guard_msgs in
 #check foo.induct
@@ -824,11 +823,11 @@ where
   termination_by as.size - i
 
 /--
-error: Function Errors.takeWhile does not look like a function defined by well-founded recursion.
+error: Function Errors.takeWhile does not look like a function defined by recursion.
 NB: If Errors.takeWhile is not itself recursive, but contains an inner recursive function (via `let rec` or `where`), try `Errors.takeWhile.go` where `go` is name of the inner function.
 -/
 #guard_msgs in
-derive_functional_induction takeWhile -- Cryptic error message
+derive_functional_induction takeWhile
 
 derive_functional_induction takeWhile.foo
 
@@ -853,7 +852,7 @@ derive_functional_induction foo
 /--
 info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ)
-  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (x : Nat) : motive x
+  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
 #check foo.induct