fix: disable buggy optimization

This PR combines the simplification and unfold-reducible-constants
steps in `grind` to ensure that no potential normalization steps are
missed.

Closes #9610

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

@@ -23,10 +23,17 @@ namespace Lean.Meta.Grind
 def simpCore (e : Expr) : GrindM Simp.Result := do profileitM Exception "grind simp" (← getOptions) do
   let simp ← modifyGet fun s => (s.simp, { s with simp := {} })
   let ctx := (← readThe Context).simp
-  let m := (← get).scState.map
-  let skipIfInShareCommon : Simp.Simproc := fun e => if m.contains { expr := e } then return .done { expr := e } else return .continue
+  /-
+  Remark: we used to use `skipIfInShareCommon` as an additional filter to avoid re-visiting expressions
+  that have already been fully processed by `grind`. The idea was to use the `inShareCommon` test since
+  the last step of the `grind` normalizer is `shareCommon`.
+  However, this optimization was incorrect because there are other places in the `grind` code base that
+  use `shareCommon`.
+  -/
+  -- let m := (← get).scState.map
+  -- let skipIfInShareCommon : Simp.Simproc := fun e => if m.contains { expr := e } then return .done { expr := e } else return .continue
   let methods := (← readThe Context).simpMethods
-  let methods := { methods with pre := skipIfInShareCommon >> methods.pre }
+  -- let methods := { methods with pre := skipIfInShareCommon >> methods.pre }
   let (r, simp) ← Simp.mainCore e ctx simp (methods := methods)
   modify fun s => { s with simp }
   return r
@@ -39,25 +46,6 @@ def dsimpCore (e : Expr) : GrindM Expr := do profileitM Exception "grind dsimp"
   modify fun s => { s with simp }
   return r
 
-/--
-Unfolds all `reducible` declarations occurring in `e`.
-Similar to `unfoldReducible`, but uses `alreadyInternalized` as an extra filter
--/
-def unfoldReducible' (e : Expr) : GoalM Expr := do
-  if !(← isUnfoldReducibleTarget e) then return e
-  let pre (e : Expr) : GoalM TransformStep := do
-    -- We used to use `inShareCommon` here, but it was to correct.
-    -- `inShareCommon` is used in terms that have not been preprocessed (e.g., proofs).
-    if (← alreadyInternalized e) then return .done e
-    let .const declName _ := e.getAppFn | return .continue
-    unless (← isReducible declName) do return .continue
-    if isGrindGadget declName then return .continue
-    -- See comment at isUnfoldReducibleTarget.
-    if (← getEnv).isProjectionFn declName then return .continue
-    let some v ← unfoldDefinition? e | return .continue
-    return .visit v
-  Core.transform e (pre := pre)
-
 /--
 Preprocesses `e` using `grind` normalization theorems and simprocs,
 and then applies several other preprocessing steps.
@@ -66,7 +54,6 @@ def preprocess (e : Expr) : GoalM Simp.Result := do
   let e ← instantiateMVars e
   let r ← simpCore e
   let e' := r.expr
-  let e' ← unfoldReducible' e'
   let e' ← abstractNestedProofs e'
   let e' ← markNestedSubsingletons e'
   let e' ← eraseIrrelevantMData e'

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

@@ -138,6 +138,9 @@ builtin_simproc_decl reduceCtorEqCheap (_ = _) := fun e => do
   withLocalDeclD `h e fun h =>
     return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
 
+builtin_dsimproc_decl unfoldReducibleSimproc (_) := fun e => do
+  unfoldReducibleStep e
+
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← Simp.getSEvalSimprocs
@@ -165,6 +168,7 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← s.add ``simpOr (post := true)
   let s ← s.add ``simpDIte (post := true)
   let s ← s.add ``pushNot (post := false)
+  let s ← s.add ``unfoldReducibleSimproc (post := false)
   return #[s]
 
 private def addDeclToUnfold (s : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do

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

@@ -65,20 +65,25 @@ def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
     else
       return false
 
+/--
+Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
+Performs a single step.
+-/
+def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
+  let .const declName _ := e.getAppFn | return .continue
+  unless (← isReducible declName) do return .continue
+  if isGrindGadget declName then return .continue
+  -- See comment at isUnfoldReducibleTarget.
+  if (← getEnv).isProjectionFn declName then return .continue
+  let some v ← unfoldDefinition? e | return .continue
+  return .visit v
+
 /--
 Unfolds all `reducible` declarations occurring in `e`.
 -/
 def unfoldReducible (e : Expr) : MetaM Expr := do
   if !(← isUnfoldReducibleTarget e) then return e
-  let pre (e : Expr) : MetaM TransformStep := do
-    let .const declName _ := e.getAppFn | return .continue
-    unless (← isReducible declName) do return .continue
-    if isGrindGadget declName then return .continue
-    -- See comment at isUnfoldReducibleTarget.
-    if (← getEnv).isProjectionFn declName then return .continue
-    let some v ← unfoldDefinition? e | return .continue
-    return .visit v
-  Core.transform e (pre := pre)
+  Core.transform e (pre := unfoldReducibleStep)
 
 /--
 Unfolds all `reducible` declarations occurring in the goal's target.

tests/lean/run/grind_9610.lean

@@ -0,0 +1,9 @@
+set_option warn.sorry false
+abbrev sixteen : UInt32 := 16
+
+theorem foo (x: UInt32) :
+    x.toNat ≤ sixteen.toNat := by sorry
+
+theorem aa (x : UInt32) :
+  x.toNat ≤ sixteen.toNat := by
+  grind [foo]