feat: name the functional argument to brecOn in structural recursion (#12987)

This PR extracts the functional (lambda) passed to `brecOn` in
structural
recursion into a named `_f` helper definition (e.g. `foo._f`), similar
to
how well-founded recursion uses `._unary`. This way the functional shows
up
with a helpful name in kernel diagnostics rather than as an anonymous
lambda.

The `_f` definition is added with `.abbrev` kernel reducibility hints
and
the `@[reducible]` elaborator attribute, so the kernel unfolds it
eagerly
after `brecOn` iota-reduces. For inductive predicates, the previous
inline
lambda behavior is kept.

To ensure that parent definitions still get the correct reducibility
height
(since `getMaxHeight` ignores `.abbrev` definitions), each `_f`'s body
height is registered via a new `defHeightOverrideExt` environment
extension.
`getMaxHeight` checks this extension for all definitions, making the
height
computation transparent to the extraction.

This change improves code size (a bit). It may regress kernel reduction
times,
especially if a function defined by structural recursion is used in
kernel reduction
proofs on the hot path. Functions defined by structural recursion are
not particularly
fast to reduce anyways (due to the `.brecOn` construction), so already
now it may be
worth writing a kernel-reduction-friendly function manually (using the
recursor directly,
avoiding overloaded operations). This change will guide you in knowing
which function to
optimize.


🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -80,6 +80,32 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
       withRecFunsAsAxioms preDefs do
         mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
   trace[Elab.definition.structural] "FArgs: {FArgs}"
+
+  -- Extract the functionals into named `_f` helper definitions (e.g. `foo._f`) so they show up
+  -- with a helpful name in kernel diagnostics. The `_f` definitions are `.abbrev` so the kernel
+  -- unfolds them eagerly; their body heights are registered via `setDefHeightOverride` so that
+  -- `getMaxHeight` computes the correct height for parent definitions.
+  -- For inductive predicates, the previous inline behavior is kept.
+  let FArgs ←
+    if isIndPred then
+      pure FArgs
+    else
+      let us := preDefs[0]!.levelParams.map mkLevelParam
+      FArgs.mapIdxM fun idx fArg => do
+        let fName := preDefs[idx]!.declName ++ `_f
+        let fValue ← eraseRecAppSyntaxExpr (← mkLambdaFVars xs fArg)
+        let fType ← Meta.letToHave (← inferType fValue)
+        let fHeight := getMaxHeight (← getEnv) fValue
+        addDecl (.defnDecl {
+          name := fName, levelParams := preDefs[idx]!.levelParams,
+          type := fType, value := fValue,
+          hints := .abbrev,
+          safety := if preDefs[idx]!.modifiers.isUnsafe then .unsafe else .safe,
+          all := [fName] })
+        modifyEnv (setDefHeightOverride · fName fHeight)
+        setReducibleAttribute fName
+        return mkAppN (mkConst fName us) xs
+
   let brecOn := brecOnConst 0
   -- the indices and the major premise are not mentioned in the minor premises
   -- so using `default` is fine here

src/Lean/Environment.lean

@@ -2755,13 +2755,28 @@ def mkThmOrUnsafeDef [Monad m] [MonadEnv m] (thm : TheoremVal) : m Declaration :
   else
     return .thmDecl thm
 
+/-- Environment extension for overriding the height that `getMaxHeight` assigns to a definition.
+This is consulted for all definitions regardless of their reducibility hints. Currently used by
+structural recursion to ensure that parent definitions get the correct height even though the
+`_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
+builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
+  registerEnvExtension (pure {}) (asyncMode := .local)
+
+/-- Register a height override for a definition so that `getMaxHeight` uses it. -/
+def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=
+  defHeightOverrideExt.modifyState env fun m => m.insert declName height
+
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
+  let overrides := defHeightOverrideExt.getState env
   e.foldConsts 0 fun constName max =>
-    match env.findAsync? constName with
-    | some { kind := .defn, constInfo := info, .. } =>
-      match info.get.hints with
-      | ReducibilityHints.regular h => if h > max then h else max
-      | _                           => max
-    | _ => max
+    match overrides.find? constName with
+    | some h => if h > max then h else max
+    | none =>
+      match env.findAsync? constName with
+      | some { kind := .defn, constInfo := info, .. } =>
+        match info.get.hints with
+        | ReducibilityHints.regular h => if h > max then h else max
+        | _                           => max
+      | _ => max
 
 end Lean

src/Lean/Meta/Tactic/FunInd.lean

@@ -742,6 +742,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         let b' ← buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
         mkLambdaFVars #[x] b'
 
+  -- Unfold constant applications that take `oldIH` as an argument (e.g. `_f` auxiliary
+  -- definitions from structural recursion), so that we can see their body structure.
+  -- Similar to the case in `foldAndCollect`.
+  if e.getAppFn.isConst && e.getAppArgs.any (·.isFVarOf oldIH) then
+    if let some e' ← withTransparency .all (unfoldDefinition? e) then
+      return ← buildInductionBody toErase toClear goal oldIH newIH isRecCall e'
+
   liftM <| buildInductionCase oldIH newIH isRecCall toErase toClear goal e
 
 /--

stage0/src/stdlib_flags.h

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

tests/elab/Dorais1.lean

@@ -24,6 +24,6 @@ protected def Path.unmap : {t : Tree α} → Path (t.map f) → Path t
 | Tree.branch tl tr, Path.left _ _ p => Path.left tl tr (Path.unmap p)
 | Tree.branch tl tr, Path.right _ _ p => Path.right tl tr (Path.unmap p)
 
-#print Path.unmap
+#check @Path.unmap
 
 end map

tests/elab/Dorais1.lean.out.expected

@@ -1,13 +1 @@
-protected def Path.unmap.{u_1, u_2} : {α : Type u_1} →
-  {β : Type u_2} → (f : α → β) → {t : Tree α} → Path (Tree.map f t) → Path t :=
-fun {α} {β} f x x_1 =>
-  Tree.brecOn (motive := fun x => Path (Tree.map f x) → Path x) x
-    (fun x f_1 x_2 =>
-      (match (motive :=
-          (x : Tree α) → Path (Tree.map f x) → Tree.below (motive := fun x => Path (Tree.map f x) → Path x) x → Path x)
-          x, x_2 with
-        | Tree.leaf x, Path.term .(f x) => fun x_3 => Path.term x
-        | tl.branch tr, Path.left .(Tree.map f tl) .(Tree.map f tr) p => fun x => Path.left tl tr (x.1.1 p)
-        | tl.branch tr, Path.right .(Tree.map f tl) .(Tree.map f tr) p => fun x => Path.right tl tr (x.2.1 p))
-        f_1)
-    x_1
+@Path.unmap : {α : Type u_1} → {β : Type u_2} → (f : α → β) → {t : Tree α} → Path (Tree.map f t) → Path t

tests/elab/def6.lean

@@ -20,7 +20,7 @@ rfl
 theorem ex2 (n : Nat) (b1 b2 : Bool) (v1 v2 : BV n) : map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2) :=
 rfl
 
-#print map2
+#check @map2
 
 def map2' : {n : Nat} →  BV n → BV n → BV n
 | _, nil,          nil          => nil

tests/elab/def6.lean.out.expected

@@ -1,10 +1 @@
-def map2 : (Bool → Bool → Bool) → {n : Nat} → BV n → BV n → BV n :=
-fun f x x_1 x_2 =>
-  BV.brecOn (motive := fun x x_3 => BV x → BV x) x_1
-    (fun x x_3 f_1 x_4 =>
-      (match (motive := (x : Nat) → (x_5 : BV x) → BV x → BV.below (motive := fun x x_7 => BV x → BV x) x_5 → BV x) x,
-          x_3, x_4 with
-        | .(0), nil, nil => fun x => nil
-        | .(n + 1), cons n b1 v1, cons .(n) b2 v2 => fun x => cons n (f b1 b2) (x.1 v2))
-        f_1)
-    x_2
+map2 : (Bool → Bool → Bool) → {n : Nat} → BV n → BV n → BV n

tests/elab/diagRec.lean

@@ -8,11 +8,11 @@ termination_by structural n
 info: 573147844013817084101
 ---
 trace: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 596, num: 2):
-    [reduction] Nat.rec ↦ 596
-    [reduction] HAdd.hAdd ↦ 196
-  [reduction] unfolded reducible declarations (max: 397, num: 1):
-    [reduction] Nat.casesOn ↦ 397
+  [reduction] unfolded declarations (max: 400, num: 1):
+    [reduction] Nat.rec ↦ 400
+  [reduction] unfolded reducible declarations (max: 201, num: 2):
+    [reduction] Nat.casesOn ↦ 201
+    [reduction] fib._f ↦ 199
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in

tests/elab/letToHaveCleanup.lean

@@ -71,23 +71,30 @@ def fnStructRec (n : Nat) : let α := Nat; α :=
 info: def fnStructRec : Nat →
   have α : Type := Nat;
   α :=
-fun n =>
-  Nat.brecOn n fun n f =>
-    (match (motive :=
-        (n : Nat) →
-          Nat.below n →
-            let α : Type := Nat;
-            α)
-        n with
-      | 0 => fun x => 0
-      | n.succ => fun x =>
-        id
-          (let m : Nat := n + 1;
-          m * x.1))
-      f
+fun n => Nat.brecOn n fnStructRec._f
 -/
 #guard_msgs in #print fnStructRec
 /--
+info: @[reducible] def fnStructRec._f : (n : Nat) →
+  Nat.below n →
+    have α : Type := Nat;
+    α :=
+fun n f =>
+  (match (motive :=
+      (n : Nat) →
+        Nat.below n →
+          let α : Type := Nat;
+          α)
+      n with
+    | 0 => fun x => 0
+    | n.succ => fun x =>
+      id
+        (let m : Nat := n + 1;
+        m * x.1))
+    f
+-/
+#guard_msgs in #print fnStructRec._f
+/--
 info: fnStructRec.eq_def (n : Nat) :
   fnStructRec n =
     match n with
@@ -140,19 +147,7 @@ info: id
 -/
 #guard_msgs in #unfold1 fnStructRec 1
 /--
-info: Nat.brecOn 1 fun n f =>
-  (match (motive :=
-      (n : Nat) →
-        Nat.below n →
-          let α : Type := Nat;
-          α)
-      n with
-    | 0 => fun x => 0
-    | n.succ => fun x =>
-      id
-        (let m : Nat := n + 1;
-        m * x.1))
-    f
+info: Nat.brecOn 1 fnStructRec._f
 -/
 #guard_msgs in
 set_option smartUnfolding false in

tests/elab/ppMotives.lean

@@ -1,11 +1,16 @@
+def myAdd : Nat → Nat → Nat
+  | 0, m => m
+  | n+1, m => (myAdd n m).succ
+
 set_option pp.motives.pi false
 
-#print Nat.add
+#print myAdd._f
 
 set_option pp.motives.pi true
 
-#print Nat.add
+#print myAdd._f
 
+set_option linter.unusedVariables false in
 theorem ex : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a
   | α, _, rfl, a => HEq.refl a
 

tests/elab/ppMotives.lean.out.expected

@@ -1,21 +1,15 @@
-@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat :=
-fun x x_1 =>
-  Nat.brecOn x_1
-    (fun x f x_2 =>
-      (match x_2, x with
-        | a, Nat.zero => fun x => a
-        | a, b.succ => fun x => (x.1 a).succ)
-        f)
-    x
-@[implicit_reducible] protected def Nat.add : Nat → Nat → Nat :=
-fun x x_1 =>
-  Nat.brecOn (motive := fun x => Nat → Nat) x_1
-    (fun x f x_2 =>
-      (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
-        | a, Nat.zero => fun x => a
-        | a, b.succ => fun x => (x.1 a).succ)
-        f)
-    x
+@[reducible] def myAdd._f : (x : Nat) → Nat.below x → Nat → Nat :=
+fun x f x_1 =>
+  (match x, x_1 with
+    | 0, m => fun x => m
+    | n.succ, m => fun x => (x.1 m).succ)
+    f
+@[reducible] def myAdd._f : (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat → Nat :=
+fun x f x_1 =>
+  (match (motive := (x : Nat) → Nat → Nat.below (motive := fun x => Nat → Nat) x → Nat) x, x_1 with
+    | 0, m => fun x => m
+    | n.succ, m => fun x => (x.1 m).succ)
+    f
 theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a :=
 fun x x_1 x_2 x_3 =>
   match x, x_1, x_2, x_3 with

tests/elab/structuralMutual.lean

@@ -70,6 +70,26 @@ theorem B_size_eq3 : B.empty.size = 0  := rfl
 #guard_msgs in
 #check B.size.eq_3
 
+-- `_f` definitions show up in diagnostics
+/--
+info: 3
+---
+trace: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 8, num: 4):
+    [reduction] A.rec ↦ 8
+    [reduction] Add.add ↦ 3
+    [reduction] HAdd.hAdd ↦ 3
+    [reduction] OfNat.ofNat ↦ 2
+  [reduction] unfolded reducible declarations (max: 4, num: 2):
+    [reduction] A.casesOn ↦ 4
+    [reduction] A.size._f ↦ 4
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+set_option diagnostics true in
+set_option diagnostics.threshold 1 in
+#reduce A.size (.self (.self (.self .empty)))
+
 -- Smart unfolding works
 
 /--
@@ -512,13 +532,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 544:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 564:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
 #6  ?  ?  =  ?
 #7  ?  ?  ?  =
 #8  ?  =  ?  ?
-Call from ManyCombinations.g to ManyCombinations.f at 547:15-29:
+Call from ManyCombinations.g to ManyCombinations.f at 567:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
 #2  _  _  _  ?

tests/elab/structuralNamedF.lean

@@ -0,0 +1,77 @@
+-- Test that structural recursion creates a named `_f` helper definition
+-- for the functional passed to `brecOn`.
+
+-- Simple case: single function
+def addAdjacent : List Nat → List Nat
+  | []       => []
+  | [a]      => [a]
+  | a::b::as => (a+b) :: addAdjacent as
+
+-- The `_f` helper should exist in the environment
+/-- info: addAdjacent._f : (x : List Nat) → List.below x → List Nat -/
+#guard_msgs in #check @addAdjacent._f
+
+-- Verify computation still works
+/-- info: [3, 7] -/
+#guard_msgs in #eval addAdjacent [1, 2, 3, 4]
+
+-- Mutual recursion: each function gets its own `_f`
+mutual
+  def even : Nat → Bool
+    | 0 => true
+    | n + 1 => odd n
+
+  def odd : Nat → Bool
+    | 0 => false
+    | n + 1 => even n
+end
+
+/-- info: even._f : (x : Nat) → Nat.below x → Bool -/
+#guard_msgs in #check @even._f
+
+/-- info: odd._f : (x : Nat) → Nat.below x → Bool -/
+#guard_msgs in #check @odd._f
+
+/-- info: true -/
+#guard_msgs in #eval even 4
+
+/-- info: true -/
+#guard_msgs in #eval odd 3
+
+-- With fixed parameters
+def myMap (f : α → β) : List α → List β
+  | []    => []
+  | x::xs => f x :: myMap f xs
+
+/-- info: @myMap._f : {α : Type u_1} → {β : Type u_2} → (α → β) → (x : List α) → List.below x → List β -/
+#guard_msgs in #check @myMap._f
+
+-- The `_f` helper shows up with a helpful name in kernel diagnostics
+def fib (n : Nat) :=
+  match n with
+  | 0 | 1 => 1
+  | x+2 => fib x + fib (x+1)
+termination_by structural n
+
+/--
+trace: [diag] Diagnostics
+  [reduction] unfolded declarations (max: 79, num: 4):
+    [reduction] Nat.rec ↦ 79
+    [reduction] Add.add ↦ 41
+    [reduction] HAdd.hAdd ↦ 41
+    [reduction] fib ↦ 40
+  [reduction] unfolded reducible declarations (max: 79, num: 1):
+    [reduction] Nat.casesOn ↦ 79
+  [kernel] unfolded declarations (max: 80, num: 6):
+    [kernel] Nat.rec ↦ 80
+    [kernel] Nat.casesOn ↦ 77
+    [kernel] fib._f ↦ 39
+    [kernel] fib.match_1 ↦ 39
+    [kernel] Add.add ↦ 36
+    [kernel] HAdd.hAdd ↦ 36
+  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+set_option diagnostics true in
+set_option diagnostics.threshold 10 in
+theorem fib_20 : fib 20 = 10946 := rfl

tests/elab/unusedLet.lean.out.expected

@@ -2,11 +2,4 @@ def pro : Bool :=
 have x := 42;
 false
 def f : Nat → Nat :=
-fun x =>
-  Nat.brecOn x fun x f =>
-    (match (motive := (x : Nat) → Nat.below x → Nat) x with
-      | 0 => fun x => 1
-      | n.succ => fun x =>
-        let y := 42;
-        2 * x.1)
-      f
+fun x => Nat.brecOn x f._f

tests/elab_bench/string_simp_ne.lean

@@ -19,7 +19,7 @@ open Lean Elab Command in
 /-- Generate `example : s₁ ≠ s₂ := by simp` where s₁ = n×'a'++"x" and s₂ = n×'a'++"y". -/
 elab "#bench_string_ne_suffix " n:num : command => do
   let n := n.getNat
-  let pfx := String.mk (List.replicate n 'a')
+  let pfx := String.ofList (List.replicate n 'a')
   let s1 := pfx ++ "x"
   let s2 := pfx ++ "y"
   elabCommand (← `(#time example : ($(Syntax.mkStrLit s1) : String) ≠ ($(Syntax.mkStrLit s2) : String) := by simp))
@@ -29,7 +29,7 @@ open Lean Elab Command in
     Strings differ at the first character — tests O(1) inequality proof. -/
 elab "#bench_string_ne_prefix " n:num : command => do
   let n := n.getNat
-  let sfx := String.mk (List.replicate n 'a')
+  let sfx := String.ofList (List.replicate n 'a')
   let s1 := "x" ++ sfx
   let s2 := "y" ++ sfx
   elabCommand (← `(#time example : ($(Syntax.mkStrLit s1) : String) ≠ ($(Syntax.mkStrLit s2) : String) := by simp))
@@ -38,7 +38,7 @@ open Lean Elab Command in
 /-- Generate `example : s = s := by simp` with s = n×'a'. -/
 elab "#bench_string_eq " n:num : command => do
   let n := n.getNat
-  let s := String.mk (List.replicate n 'a')
+  let s := String.ofList (List.replicate n 'a')
   elabCommand (← `(#time example : ($(Syntax.mkStrLit s) : String) = ($(Syntax.mkStrLit s) : String) := by simp))
 
 -- Ne: shared prefix of increasing length (differ at last character)