test: remove workaround

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -178,7 +178,12 @@ protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
   thms ← addDeclToUnfold thms ``Bool.xor
   thms ← addDeclToUnfold thms ``Ne
   Simp.mkContext
-    (config := { arith := true, zeta := config.zeta, zetaDelta := config.zetaDelta, catchRuntime := false })
+    (config :=
+      { arith := true, zeta := config.zeta,
+        zetaDelta := config.zetaDelta,
+        catchRuntime := false,
+        -- `implicitDefEqProofs := true` a recurrent source of performance problems in the kernel
+        implicitDefEqProofs := false })
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
 

src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean

@@ -156,15 +156,16 @@ def simpDvd? (e : Expr) : MetaM (Option (Expr × Expr)) := do
       return some (rhs, mkExpectedPropHint h (mkPropEq lhs rhs))
 
 def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
-  let (e, atoms) ← toLinearExpr lhs
-  let p  := e.norm
-  let e' := p.toExpr
-  if e != e' then
-    -- We only return some if monomials were fused
-    let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (← toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
-    let rhs ← p.denoteExpr (atoms[·]!)
-    return some (rhs, mkExpectedPropHint h (mkIntEq lhs rhs))
-  else
-    return none
+  let (e, ctx) ← toLinearExpr lhs
+  withAbstractAtoms ctx ``Int fun ctx => do
+    let p  := e.norm
+    let e' := p.toExpr
+    if e != e' then
+      let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (← toContextExpr ctx) (toExpr e) (toExpr p) reflBoolTrue
+      let lhs ← e.denoteExpr (ctx[·]!)
+      let rhs ← p.denoteExpr (ctx[·]!)
+      return some (rhs, mkExpectedPropHint h (mkIntEq lhs rhs))
+    else
+      return none
 
 end Lean.Meta.Simp.Arith.Int

src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean

@@ -64,13 +64,15 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
 
 def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
   let (e, ctx) ← toLinearExpr input
-  let p  := e.toPoly
-  let p' := p.norm
-  let e' : LinearExpr := p'.toExpr
-  if e' == e then
-    return none
-  let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
-  let r ← e'.toArith ctx
-  return some (r, mkExpectedPropHint p (mkNatEq input r))
+  withAbstractAtoms ctx ``Nat fun ctx => do
+    let p  := e.toPoly
+    let p' := p.norm
+    let e' : LinearExpr := p'.toExpr
+    if e' == e then
+      return none
+    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
+    let l ← e.toArith ctx
+    let r ← e'.toArith ctx
+    return some (r, mkExpectedPropHint p (mkNatEq l r))
 
 end Lean.Meta.Simp.Arith.Nat

tests/lean/run/grind_cutsat_omega.lean

@@ -236,7 +236,6 @@ example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
 example : 2^7 < 165 := by grind
 example (x : Nat) (_ : x % 2^7 < 3) : x % 128 < 5 := by grind
 
-set_option debug.skipKernelTC true in -- TODO: kernel deep recursion
 example (a : Nat) :
     (((a + (2 ^ 64 - 1)) % 2 ^ 64 + 1) * 8 - 1 - (a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + 1) = 8 := by
   grind