fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offs…

…ets (#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

@@ -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

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