refactor: Predefinition.Structural code cleanup (leanprover#5850)

useful bits from the shelved leanprover#5849

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

@@ -114,8 +114,9 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
   The dictionary is built using the `PProd` (`And` for inductive predicates).
   We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
 private partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
-  withBelowDict below numIndParams positions fun Cs belowDict =>
-    toBelowAux Cs[fnIndex]! belowDict recArg below
+  withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
+    withBelowDict below numIndParams positions fun Cs belowDict =>
+      toBelowAux Cs[fnIndex]! belowDict recArg below
 
 private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
     (below : Expr) (e : Expr) : M Expr :=

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -4,18 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Util.HasConstCache
-import Lean.Meta.Match.Match
-import Lean.Meta.Tactic.Simp.Main
-import Lean.Meta.Tactic.Cleanup
-import Lean.Meta.ArgsPacker
-import Lean.Elab.Tactic.Basic
-import Lean.Elab.RecAppSyntax
+import Lean.Data.Array
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.Structural.BRecOn
 import Lean.Elab.PreDefinition.WF.Basic
-import Lean.Data.Array
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.ArgsPacker
+import Lean.Meta.ForEachExpr
+import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Tactic.Cleanup
+import Lean.Util.HasConstCache
 
 namespace Lean.Elab.WF
 open Meta

tests/lean/run/issue5836.lean

@@ -28,3 +28,56 @@ def Foo.bar_aux (m : Foo → Foo) : Option Foo → Option Foo
     | some x => bar m x
 termination_by structural x => x
 end
+
+-- similar
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter xs:
+  failed to eliminate recursive application
+    g ys
+-/
+#guard_msgs in
+def g (xs : List Nat) : Nat :=
+  match xs with
+  | [] => 0
+  | _::ys =>
+    match ys with
+    | []       => 1
+    | _::_::zs => g zs + 1
+    | _zs       => g ys + 2
+termination_by structural xs
+
+
+inductive Foo2 where
+  | none
+  | foo : (String → Foo2) → Foo2
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  failed to eliminate recursive application
+    map m (f₂ s)
+-/
+#guard_msgs in
+def Foo2.map (m : Foo2 → Foo2) : Foo2 → Foo2
+  | none => none
+  | .foo f => .foo fun s => match f s with
+    | none => none
+    | foo f₂ => .foo fun s => map m (f₂ s)
+termination_by structural x => x
+
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  failed to eliminate recursive application
+    map_tricky m (f₂ s)
+-/
+#guard_msgs in
+def Foo2.map_tricky (m : Foo2 → Foo2) : Foo2 → Foo2
+  | none => none
+  | .foo f => .foo fun s => match f s, f (s ++ s) with
+    | foo f₂, foo f₃ => .foo fun s => if s = "test" then map_tricky m (f₂ s) else map_tricky m (f₃ s)
+    | _, _ => none
+termination_by structural x => x