From 3701bee7771dbc6e375bed46c7a6e30822ea0f87 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 24 Jul 2024 10:14:25 +0200
Subject: [PATCH] test: test case for #4751 (#4819)

and tracing for `IndPredBelow.backwardsChaining`.
---
 src/Lean/Meta/IndPredBelow.lean | 37 ++++++++++++--------
 tests/lean/run/4751.lean        | 61 +++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+), 15 deletions(-)
 create mode 100644 tests/lean/run/4751.lean

diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 8e18fdc2a9..d9822f1ffa 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -230,22 +230,28 @@ def mkBelowDecl (ctx : Context) : MetaM Declaration := do
     ctx.typeInfos[0]!.isUnsafe
 
 partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
-  if depth = 0 then return false
-  else
-    m.withContext do
-    let lctx ← getLCtx
+  m.withContext do
     let mTy ← m.getType
-    lctx.anyM fun localDecl =>
-      if localDecl.isAuxDecl then
-        return false
-      else
-        commitWhen do
-        let (mvars, _, t) ← forallMetaTelescope localDecl.type
-        if ←isDefEq mTy t then
-          m.assign (mkAppN localDecl.toExpr mvars)
-          mvars.allM fun v =>
-            v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1)
-        else return false
+    if depth = 0 then
+      trace[Meta.IndPredBelow.search] "searching for {mTy}: ran out of max depth"
+      return false
+    else
+      let lctx ← getLCtx
+      let r ← lctx.anyM fun localDecl =>
+        if localDecl.isAuxDecl then
+          return false
+        else
+          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
+      unless r do
+        trace[Meta.IndPredBelow.search] "searching for {mTy} failed"
+      return r
 
 partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do
   let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -596,5 +602,6 @@ def mkBelow (declName : Name) : MetaM Unit := do
 builtin_initialize
   registerTraceClass `Meta.IndPredBelow
   registerTraceClass `Meta.IndPredBelow.match
+  registerTraceClass `Meta.IndPredBelow.search
 
 end Lean.Meta.IndPredBelow
diff --git a/tests/lean/run/4751.lean b/tests/lean/run/4751.lean
new file mode 100644
index 0000000000..2f48ce2eea
--- /dev/null
+++ b/tests/lean/run/4751.lean
@@ -0,0 +1,61 @@
+inductive F: Prop where
+  | base
+  | step (fn: Nat → F)
+
+-- set_option trace.Meta.IndPredBelow.search true
+set_option pp.proofs true
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #1:
+  could not solve using backwards chaining x✝¹ : F
+  x✝ : x✝¹.below
+  f : Nat → F
+  a✝¹ : ∀ (a : Nat), (f a).below
+  a✝ : Nat → True
+  ⊢ True
+-/
+#guard_msgs in
+def F.asdf1 : (f : F) → True
+  | base => trivial
+  | step f => F.asdf1 (f 0)
+termination_by structural f => f
+
+
+def TTrue (_f : F) := True
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #1:
+  could not solve using backwards chaining x✝¹ : F
+  x✝ : x✝¹.below
+  f : Nat → F
+  a✝¹ : ∀ (a : Nat), (f a).below
+  a✝ : ∀ (a : Nat), TTrue (f a)
+  ⊢ TTrue (f 0)
+-/
+#guard_msgs in
+def F.asdf2 : (f : F) → TTrue f
+  | base => trivial
+  | step f => F.asdf2 (f 0)
+termination_by structural f => f
+
+
+
+inductive ITrue (f : F) : Prop where | trivial
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #1:
+  could not solve using backwards chaining x✝¹ : F
+  x✝ : x✝¹.below
+  f : Nat → F
+  a✝¹ : ∀ (a : Nat), (f a).below
+  a✝ : ∀ (a : Nat), ITrue (f a)
+  ⊢ ITrue (f 0)
+-/
+#guard_msgs in
+def F.asdf3 : (f : F) → ITrue f
+  | base => .trivial
+  | step f => F.asdf3 (f 0)
+termination_by structural f => f