chore: audit and standardize grind E-graph internalization entry points

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

@@ -147,9 +147,8 @@ where
       let identityType := mkApp3 (mkConst ``Std.LawfulIdentity [u]) α op neutral
       if let some identityInst ← synthInstance? identityType then
         let neutral ← instantiateExprMVars neutral
-        let neutral ← preprocessLight neutral
-        internalize neutral (← getGeneration op)
-        pure (some identityInst, some neutral)
+        let r ← preprocessAndInternalize neutral (← getGeneration op)
+        pure (some identityInst, some r.expr)
       else
         pure (none, none)
     let id := (← get').structs.size

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -378,6 +378,8 @@ private def diseqToEq (a b : Expr) : RingM Unit := do
   modifyCommRing fun s => { s with invSet := s.invSet.insert e }
   let eInv ← pre <| mkApp (← getInvFn) e
   let lhs ← pre <| mkApp2 (← getMulFn) e eInv
+  -- Note: cannot use `preprocessAndInternalize` here; the expression form is tightly coupled
+  -- with the CommRing solver's proof reconstruction.
   internalize lhs gen none
   trace[grind.debug.ring.rabinowitsch] "{lhs}"
   pushEq lhs (← getOne) <| mkApp5 (mkConst ``Grind.CommRing.diseq_to_eq [ring.u]) ring.type fieldInst a b (← mkDiseqProof a b)
@@ -390,6 +392,8 @@ private def diseqZeroToEq (a b : Expr) : RingM Unit := do
   modifyCommRing fun s => { s with invSet := s.invSet.insert a }
   let aInv ← pre <| mkApp (← getInvFn) a
   let lhs ← pre <| mkApp2 (← getMulFn) a aInv
+  -- Note: cannot use `preprocessAndInternalize` here; the expression form is tightly coupled
+  -- with the CommRing solver's proof reconstruction.
   internalize lhs gen none
   trace[grind.debug.ring.rabinowitsch] "{lhs}"
   pushEq lhs (← getOne) <| mkApp4 (mkConst ``Grind.CommRing.diseq0_to_eq [ring.u]) ring.type fieldInst a (← mkDiseqProof a b)

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -231,6 +231,8 @@ private def propagateNonlinearDiv (x : Var) : GoalM Bool := do
   let c' ← if let some a ← getIntValue? a then
     pure { p := .add 1 x (.num (-(a/k))), h := .div k none c : EqCnstr }
   else
+    -- Note: cannot easily use `preprocessAndInternalize` here; the term is tightly coupled with
+    -- the cutsat polynomial solver and `mkVar` registration.
     let div' ← shareCommon (mkIntDiv a (mkIntLit k))
     internalize div' (← getGeneration e)
     let y ← mkVar div'
@@ -246,6 +248,8 @@ private def propagateNonlinearMod (x : Var) : GoalM Bool := do
   let c' ← if let some a ← getIntValue? a then
     pure { p := .add 1 x (.num (-(a%k))), h := .mod k none c : EqCnstr }
   else
+    -- Note: cannot easily use `preprocessAndInternalize` here; the term is tightly coupled with
+    -- the cutsat polynomial solver and `mkVar` registration.
     let mod' ← shareCommon (mkIntMod a (mkIntLit k))
     internalize mod' (← getGeneration e)
     let y ← mkVar mod'
@@ -566,6 +570,8 @@ private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
     We cannot assume terms have been normalized.
     Recall that terms may not be normalized because of dependencies.
     -/
+    -- Note: cannot easily use `preprocessAndInternalize` here; the term is tightly coupled with
+    -- the cutsat polynomial solver and `mkVar` registration.
     let gen ← getGeneration a
     internalize b' gen
     let ediv ← shareCommon (mkIntDiv a b'); internalize ediv gen

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -73,6 +73,8 @@ def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Po
 
 def _root_.Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Grind.CommRing.Poly) (generation := 0) : LinearM Expr := do
   let e ← p.denoteAsIntModuleExpr
+  -- Note: cannot use `preprocessAndInternalize` here; the expression form is tightly coupled
+  -- with the linear arithmetic solver's proof reconstruction.
   let e ← preprocessLight e
   internalize e generation (some getIntModuleVirtualParent)
   return e

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

@@ -19,17 +19,27 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) (generation : Na
     propagateInjEqs left (.proj ``And 0 proof) generation
     propagateInjEqs right (.proj ``And 1 proof) generation
   | Eq _ lhs rhs    =>
-    let lhs ← preprocessLight lhs
-    let rhs ← preprocessLight rhs
-    internalize lhs generation
-    internalize rhs generation
-    pushEq lhs rhs proof
+    let rl ← preprocessAndInternalize lhs generation
+    let rr ← preprocessAndInternalize rhs generation
+    let proof ← do
+      let proof ← match rl.proof? with
+        | some hp => mkEqTrans (← mkEqSymm hp) proof
+        | none => pure proof
+      match rr.proof? with
+        | some hp => mkEqTrans proof hp
+        | none => pure proof
+    pushEq rl.expr rr.expr proof
   | HEq _ lhs _ rhs =>
-    let lhs ← preprocessLight lhs
-    let rhs ← preprocessLight rhs
-    internalize lhs generation
-    internalize rhs generation
-    pushHEq lhs rhs proof
+    let rl ← preprocessAndInternalize lhs generation
+    let rr ← preprocessAndInternalize rhs generation
+    let proof ← do
+      let proof ← match rl.proof? with
+        | some hp => mkHEqTrans (← mkHEqSymm (← mkHEqOfEq hp)) proof
+        | none => pure proof
+      match rr.proof? with
+        | some hp => mkHEqTrans proof (← mkHEqOfEq hp)
+        | none => pure proof
+    pushHEq rl.expr rr.expr proof
   | _ =>
    reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()

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

@@ -518,8 +518,7 @@ private def synthesizeInsts (mvars : Array Expr) (bis : Array BinderInfo) : Opti
 private def preprocessGeneralizedPatternRHS (lhs : Expr) (rhs : Expr) (origin : Origin) (expectedType : Expr) : OptionT (StateT Choice M) Expr := do
   assert! (← alreadyInternalized lhs)
   -- We use `dsimp` here to ensure terms such as `Nat.succ x` are normalized as `x+1`.
-  let rhs ← preprocessLight (← dsimpCore rhs)
-  internalize rhs (← getGeneration lhs)
+  let rhs := (← preprocessAndInternalize (← dsimpCore rhs) (← getGeneration lhs)).expr
   processNewFacts
   if (← isEqv lhs rhs) then
     return rhs

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

@@ -39,6 +39,9 @@ def propagateProjEq (parent : Expr) : GoalM Unit := do
       shareCommon (mkApp (mkAppN projFn params) ctor)
     else
       shareCommon (mkApp parent.appFn! ctor)
+    -- Note: cannot use `preprocessAndInternalize` here because `parentNew` must stay structurally
+    -- similar to `parent` for congruence closure to connect them. Preprocessing could reduce
+    -- `proj_i (ctor ...)` to the field value, breaking this mechanism.
     internalize parentNew (← getGeneration parent)
     pure parentNew
   trace_goal[grind.debug.proj] "{parentNew}"

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

@@ -317,9 +317,11 @@ where
       let h' ← mkCongrFun h arg
       go rhs' h' (i+1)
     else
-      let rhs ← preprocessLight rhs
-      internalize rhs (← getGeneration e) e
-      pushEq e rhs h
+      let r ← preprocessAndInternalize rhs (← getGeneration e) e
+      let h ← match r.proof? with
+        | some hp => mkEqTrans h hp
+        | none => pure h
+      pushEq e r.expr h
 
 /-- Propagates `ite` upwards -/
 builtin_grind_propagator propagateIte ↑ite := fun e => do

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

@@ -34,10 +34,13 @@ in `(← get).inj.fns`, asserts `f⁻¹ (f a) = a`
 public def mkInjEq (e : Expr) : GoalM Unit := do
   let .app f a := e | return ()
   let some (inv, heq) ← getInvFor? f a | return ()
-  let invApp := mkApp inv e
-  internalize invApp (← getGeneration e)
-  trace[grind.inj.assert] "{invApp}, {a}"
-  pushEq invApp a <| mkApp heq a
+  let r ← preprocessAndInternalize (mkApp inv e) (← getGeneration e)
+  let proof := mkApp heq a
+  let proof ← match r.proof? with
+    | some hp => mkEqTrans (← mkEqSymm hp) proof
+    | none => pure proof
+  trace[grind.inj.assert] "{r.expr}, {a}"
+  pushEq r.expr a proof
 
 def initInjFn (us : List Level) (α β : Expr) (f : Expr) (h : Expr) : GoalM Unit := do
   modify fun s => { s with inj.fns := s.inj.fns.insert { expr := f } { us, α, β, h } }
@@ -53,9 +56,8 @@ builtin_grind_propagator propagateInj ↓Function.Injective := fun e => do
     let f ← if isSameExpr f f' then
       pure f
     else
-      let f' ← preprocessLight f'
-      internalize f' (← getGeneration e)
-      pure f'
+      let r ← preprocessAndInternalize f' (← getGeneration e)
+      pure r.expr
     initInjFn i.constLevels! α β f (mkOfEqTrueCore e (← mkEqTrueProof e))
 
 end Lean.Meta.Grind

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

@@ -14,6 +14,12 @@ If `e` has not been internalized yet, instantiate metavariables, unfold reducibl
 and internalize the result.
 
 This is an auxiliary function used at `proveEq?` and `proveHEq?`.
+
+We deliberately use `preprocessLight` here rather than the full `preprocessAndInternalize`.
+Full preprocessing runs simp, which can normalize terms into forms that break congruence closure.
+For example, `i < (a :: l).length` becomes `i + 1 ≤ (a :: l).length`, making it impossible to
+prove equality with `0 < (a :: l).length` (which becomes `1 ≤ (a :: l).length`) by congruence
+when `i` and `0` are in the same equivalence class.
 -/
 private def ensureInternalized (e : Expr) : GoalM Expr := do
   if (← alreadyInternalized e) then

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

@@ -100,4 +100,13 @@ def preprocessLight (e : Expr) : GoalM Expr := do
   let e ← instantiateMVars e
   shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← Sym.unfoldReducible e))))))
 
+/--
+Preprocesses `e` using the full grind normalization pipeline and internalizes the result.
+This is the preferred entry point for adding newly constructed terms to the E-graph.
+-/
+def preprocessAndInternalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Simp.Result := do
+  let r ← preprocess e
+  internalize r.expr generation parent?
+  return r
+
 end Lean.Meta.Grind