fix: improve proof search in IndPredBelow

src/Lean/Meta/IndPredBelow.lean

@@ -233,10 +233,11 @@ def mkBelowDecl (ctx : Context) : MetaM Declaration := do
 partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
   m.withContext do
     let mTy ← m.getType
-    if depth = 0 then
-      trace[Meta.IndPredBelow.search] "searching for {mTy}: ran out of max depth"
-      return false
-    else
+    withTraceNodeBefore `Meta.IndPredBelow.search (do pure m!"searching for {mTy}") do
+      trace[Meta.IndPredBelow.search] "Search goal:{m}"
+      if depth = 0 then
+        trace[Meta.IndPredBelow.search] "ran out of max depth"
+        return false
       let lctx ← getLCtx
       let r ← lctx.anyM fun localDecl =>
         if localDecl.isAuxDecl then
@@ -245,11 +246,12 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
           commitWhen do
           let (mvars, _, t) ← forallMetaTelescope localDecl.type
           if (← isDefEq mTy t) then
-            trace[Meta.IndPredBelow.search] "searching for {mTy}: trying {mkFVar localDecl.fvarId} : {localDecl.type}"
-            m.assign (mkAppN localDecl.toExpr mvars)
-            mvars.allM fun v =>
-              v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1)
-          else return false
+            withTraceNodeBefore `Meta.IndPredBelow.search (do pure m!"trying {mkFVar localDecl.fvarId} : {localDecl.type}") do
+              m.assign (mkAppN localDecl.toExpr mvars)
+              mvars.allM fun v =>
+                v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1)
+          else
+            return false
       unless r do
         trace[Meta.IndPredBelow.search] "searching for {mTy} failed"
       return r
@@ -303,10 +305,10 @@ where
         args.back.withApp fun ctor _ => do
         let ctorName := ctor.constName!.updatePrefix below.constName!
         let ctor := mkConst ctorName below.constLevels!
-        let ctorInfo ← getConstInfoCtor ctorName
-        let (mvars, _, _) ← forallMetaTelescope ctorInfo.type
-        let ctor := mkAppN ctor mvars
-        m.apply ctor
+        let ms ← m.apply ctor
+        trace[Meta.IndPredBelow] "new goals {ms}"
+        pure ms.reverse
+
     return mss.foldr List.append []
 
   introNPRec (m : MVarId) : MetaM MVarId := do
@@ -322,12 +324,14 @@ where
 def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
   let type ← mkType
   let indVal := ctx.typeInfos[idx]!
-  let name := indVal.name ++ .mkSimple brecOnSuffix
+  let name := mkBRecOnName indVal.name
+  let value ← proveBrecOn ctx indVal type
+  trace[Meta.IndPredBelow] "brecOn value: {value}"
   return Declaration.thmDecl {
     name := name
     levelParams := indVal.levelParams
     type := type
-    value := ←proveBrecOn ctx indVal type }
+    value := value}
 where
   mkType : MetaM Expr :=
     forallTelescopeReducing ctx.headers[idx]! fun xs _ => do

tests/lean/run/1672.lean

@@ -0,0 +1,8 @@
+inductive TransClosure (r : α → α → Prop) : α → α → Prop
+  | extends : r a b → TransClosure r a b
+  | trans_left : r a b → TransClosure r b c → TransClosure r a c
+
+def trans' {a b c} : TransClosure r a b → TransClosure r b c → TransClosure r a c
+| .extends h₁       => .trans_left h₁
+| .trans_left h₁ h₂ => .trans_left h₁ ∘ trans' h₂
+termination_by structural t => t

tests/lean/run/1674.lean

@@ -5,3 +5,4 @@ inductive T : Prop where
 def inc: T → T
   | T.nil n => T.nil (n+1)
   | T.fn f => T.fn fun n => inc (f n)
+termination_by structural t => t

tests/lean/run/4751.lean

@@ -1,4 +1,4 @@
-inductive F: Prop where
+inductive F : Prop where
   | base
   | step (fn: Nat → F)