From 2bfcb1f25c7d51d5b4d3da88b46151e623463993 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 1 Jul 2025 09:31:58 -0700
Subject: [PATCH] fix: expand pattern offset gadget in constant patterns
 (#9130)

This PR fixes unexpected occurrences of the `Grind.offset` gadget in
ground patterns. See new test
---
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 17 ++++++++-
 tests/lean/run/grind_hyper_ex.lean            | 37 +++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_hyper_ex.lean

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index faee756dd2..c90f2229f2 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -40,6 +40,21 @@ def isOffsetPattern? (pat : Expr) : Option (Expr × Nat) := Id.run do
   let .lit (.natVal k) := k | none
   return some (pat, k)
 
+/--
+`detectOffsets` inverse.
+This function is used to expand `mkOffsetPattern` occurring in a constant pattern.
+-/
+private def expandOffsetPatterns (pat : Expr) : CoreM Expr := do
+  let pre (e : Expr) := do
+    match e with
+    | .letE .. | .lam .. | .forallE .. => return .done e
+    | _ =>
+      let some (e, k) := isOffsetPattern? e
+        | return .continue e
+      if k == 0 then return .continue e
+      return .continue <| mkNatAdd e (mkNatLit k)
+  Core.transform pat (pre := pre)
+
 def mkEqBwdPattern (u : List Level) (α : Expr) (lhs rhs : Expr) : Expr :=
   mkApp3 (mkConst ``Grind.eqBwdPattern u) α lhs rhs
 
@@ -627,7 +642,7 @@ where
       if arg.hasMVar then
         pure dontCare
       else
-        pure <| mkGroundPattern arg
+        return mkGroundPattern (← expandOffsetPatterns arg)
     else match arg with
       | .bvar idx =>
         if inSupport && (← foundBVar idx) then
diff --git a/tests/lean/run/grind_hyper_ex.lean b/tests/lean/run/grind_hyper_ex.lean
new file mode 100644
index 0000000000..157f0b5a2c
--- /dev/null
+++ b/tests/lean/run/grind_hyper_ex.lean
@@ -0,0 +1,37 @@
+abbrev ℕ :=  Nat
+
+def hyperoperation : ℕ → ℕ → ℕ → ℕ
+  | 0, _, k => k + 1
+  | 1, m, 0 => m
+  | 2, _, 0 => 0
+  | _ + 3, _, 0 => 1
+  | n + 1, m, k + 1 => hyperoperation n m (hyperoperation (n + 1) m k)
+
+attribute [local grind] hyperoperation
+
+@[grind =]
+theorem hyperoperation_zero (m k : ℕ) : hyperoperation 0 m k = k + 1 := by
+  grind
+
+@[grind =]
+theorem hyperoperation_recursion (n m k : ℕ) :
+    hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k) := by
+  grind
+
+@[grind =]
+theorem hyperoperation_one (m k : ℕ) : hyperoperation 1 m k = m + k := by
+  induction k with grind
+
+@[grind =]
+theorem hyperoperation_two (m k : ℕ) : hyperoperation 2 m k = m * k := by
+  induction k with grind
+
+@[grind =]
+theorem hyperoperation_three (m k : ℕ) : hyperoperation 3 m k = m ^ k := by
+  -- TODO: add support for Nat.pow_succ
+  induction k with grind [Nat.pow_succ] -- Ouch, this is a bad `grind` lemma.
+
+@[grind =] theorem hyperoperation_ge_three_one (n k : ℕ) : hyperoperation (n + 3) 1 k = 1 := by
+  induction n generalizing k with
+  | zero => grind
+  | succ n ih => cases k <;> grind