refactor: simplify inferface between core and offset module

`processNewEqLit` optimization is not worth the extra complexity.

src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean

@@ -339,9 +339,7 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     if let some (b, k) := isNatOffset? e then
       internalizeTerm e b k
     else if let some k := isNatNum? e then
-      -- core module has support for detecting equality between literals
-      unless isEqParent parent? do
-        internalizeTerm e z k
+      internalizeTerm e z k
 
 @[export lean_process_new_offset_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
@@ -353,17 +351,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     addEdge u v 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_1) a b h
     addEdge v u 0 <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_2) a b h
 
-@[export lean_process_new_offset_eq_lit]
-def processNewEqLitImpl (a b : Expr) : GoalM Unit := do
-  unless isSameExpr a b do
-    trace[grind.offset.eq.to] "{a}, {b}"
-    let some k := isNatNum? b | unreachable!
-    let u ← getNodeId a
-    let z ← mkNode (← getNatZeroExpr)
-    let h ← mkEqProof a b
-    addEdge u z k <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_1) a b h
-    addEdge z u (-k) <| mkApp3 (mkConst ``Grind.Nat.le_of_eq_2) a b h
-
 def traceDists : GoalM Unit := do
   let s ← get'
   for u in [:s.targets.size], es in s.targets.toArray do

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

@@ -133,22 +133,15 @@ private def checkOffsetEq (rhsRoot lhsRoot : ENode) : GoalM PendingTheoryPropaga
   | some lhsOffset =>
     if let some rhsOffset := rhsRoot.offset? then
       return .eq lhsOffset rhsOffset
-    else if isNatNum rhsRoot.self then
-      return .eqLit lhsOffset rhsRoot.self
     else
       -- We have to retrieve the node because other fields have been updated
       let rhsRoot ← getENode rhsRoot.self
       setENode rhsRoot.self { rhsRoot with offset? := lhsOffset }
       return .none
-  | none =>
-    if isNatNum lhsRoot.self then
-      if let some rhsOffset := rhsRoot.offset? then
-        return .eqLit rhsOffset lhsRoot.self
-    return .none
+  | none => return .none
 
 def propagateOffset : PendingTheoryPropagation → GoalM Unit
   | .eq lhs rhs => Arith.Offset.processNewEq lhs rhs
-  | .eqLit lhs lit => Arith.Offset.processNewEqLit lhs lit
   | _ => return ()
 
 /--

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

@@ -957,14 +957,6 @@ Notifies the offset constraint module that `a = b` where
 @[extern "lean_process_new_offset_eq"] -- forward definition
 opaque Arith.Offset.processNewEq (a b : Expr) : GoalM Unit
 
-/--
-Notifies the offset constraint module that `a = k` where
-`a` is term that has been internalized by this module,
-and `k` is a numeral.
--/
-@[extern "lean_process_new_offset_eq_lit"] -- forward definition
-opaque Arith.Offset.processNewEqLit (a k : Expr) : GoalM Unit
-
 /-- Returns `true` if `e` is a numeral and has type `Nat`. -/
 def isNatNum (e : Expr) : Bool := Id.run do
   let_expr OfNat.ofNat _ _ inst := e | false
@@ -980,8 +972,6 @@ def markAsOffsetTerm (e : Expr) : GoalM Unit := do
   let root ← getRootENode e
   if let some e' := root.offset? then
     Arith.Offset.processNewEq e e'
-  else if isNatNum root.self && !isSameExpr e root.self then
-    Arith.Offset.processNewEqLit e root.self
   else
     setENode root.self { root with offset? := some e }
 

tests/lean/run/grind_offset_cnstr.lean

@@ -399,10 +399,5 @@ example (a : Nat) : a < 2 → a = 5 → False := by
 example (a : Nat) : a < 2 → a = b → b = c → c = 5 → False := by
   grind
 
-#guard_msgs (trace) in -- none of the numerals should be internalized by the offset module
-set_option trace.grind.offset.internalize true in
-example (a b c d e : Nat) : a = 1 → b = 2 → c = 3 → d = 4 → e = 5 → a ≠ e := by
-  grind
-
 example (a b : Nat) : a + 1 = b → b = 0 → False := by
   grind