From 23236ef5203c2ed9105fcaf39ddb61bf5f25efde Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 1 Dec 2024 10:04:32 -0800
Subject: [PATCH] fix: have `Lean.Meta.isConstructorApp'?` be aware of `n + k`
 Nat offsets (#6270)

This PR fixes a bug that could cause the `injectivity` tactic to fail in
reducible mode, which could cause unfolding lemma generation to fail
(used by tactics such as `unfold`). In particular,
`Lean.Meta.isConstructorApp'?` was not aware that `n + 1` is equivalent
to `Nat.succ n`.

Closes #5064
---
 src/Lean/Meta/CtorRecognizer.lean | 24 +++++++++++++++++++++---
 tests/lean/run/5064.lean          | 27 +++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/5064.lean

diff --git a/src/Lean/Meta/CtorRecognizer.lean b/src/Lean/Meta/CtorRecognizer.lean
index afde2e4c2d..c7d251037b 100644
--- a/src/Lean/Meta/CtorRecognizer.lean
+++ b/src/Lean/Meta/CtorRecognizer.lean
@@ -35,11 +35,27 @@ def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
 
 /--
 Similar to `isConstructorApp?`, but uses `whnf`.
+It also uses `isOffset?` for `Nat`.
+
+See also `Lean.Meta.constructorApp'?`.
 -/
 def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
-  if let some r ← isConstructorApp? e then
+  if let some (_, k) ← isOffset? e then
+    if k = 0 then
+      return none
+    else
+      let .ctorInfo val ← getConstInfo ``Nat.succ | return none
+      return some val
+  else if let some r ← isConstructorApp? e then
     return r
-  isConstructorApp? (← whnf e)
+  else try
+    /-
+    We added the `try` block here because `whnf` fails at terms `n ^ m`
+    when `m` is a big numeral, and `n` is a numeral. This is a little bit hackish.
+    -/
+    isConstructorApp? (← whnf e)
+  catch _ =>
+    return none
 
 /--
 Returns `true`, if `e` is constructor application of builtin literal defeq to
@@ -70,7 +86,9 @@ def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) :
 
 /--
 Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
-It also `isOffset?`
+It also uses `isOffset?` for `Nat`.
+
+See also `Lean.Meta.isConstructorApp'?`.
 -/
 def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
   if let some (e, k) ← isOffset? e then
diff --git a/tests/lean/run/5064.lean b/tests/lean/run/5064.lean
new file mode 100644
index 0000000000..6df9de8622
--- /dev/null
+++ b/tests/lean/run/5064.lean
@@ -0,0 +1,27 @@
+/-!
+# Make sure `injection` tactic can handle `0 = n + 1`
+https://github.com/leanprover/lean4/issues/5064
+-/
+
+/-!
+Motivating example from #5064.
+This failed when generating the splitter theorem for `thingy`.
+-/
+
+def thingy : List (Nat ⊕ Nat) → List Bool
+  | Sum.inr (_n + 2) :: l => thingy l
+  | _ => []
+  termination_by l => l.length
+
+/-- info: ⊢ [] = [] -/
+#guard_msgs in
+theorem thingy_empty : thingy [] = [] := by
+  unfold thingy
+  trace_state
+  rfl
+
+/-!
+Test using `injection` directly.
+-/
+example (n : Nat) (h : 0 = n + 1) : False := by
+  with_reducible injection h