fix: remove inShareCommon filter used in grind

This PR removes the `inShareCommon` quick filter used in `grind` preprocessing steps. `shareCommon` is no longer used only for fully preprocessed terms.

closes #9830

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

@@ -202,7 +202,6 @@ partial def canon (e : Expr) : GoalM Expr := do profileitM Exception "grind cano
 where
   visit (e : Expr) : StateRefT (Std.HashMap ExprPtr Expr) GoalM Expr := do
     unless e.isApp || e.isForall do return e
-    if (← inShareCommon e) then return e
     -- Check whether it is cached
     if let some r := (← get).get? { expr := e } then
       return r

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

@@ -44,7 +44,6 @@ partial def markNestedSubsingletons (e : Expr) : GrindM Expr := do profileitM Ex
   visit e |>.run' {}
 where
   visit (e : Expr) : M Expr := do
-    if (← inShareCommon e) then return e
     if isMarkedSubsingletonApp e then
       return e -- `e` is already marked
     -- check whether result is cached

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

@@ -334,16 +334,6 @@ def shareCommon (e : Expr) : GrindM Expr := do
   modify fun s => { s with scState }
   return e
 
-/--
-Returns `true` if `e` has already been hash-consed.
-Recall that we use `shareCommon` as the last step of the preprocessing
-function `preprocess`.
-Later, we create terms using new terms that have already been preprocessed,
-and we skip preprocessing steps by checking whether `inShareCommon` returns `true`
--/
-def inShareCommon (e : Expr) : GrindM Bool := do
-  return (← get).scState.map.contains { expr := e }
-
 /-- Returns `true` if `e` is the internalized `True` expression.  -/
 def isTrueExpr (e : Expr) : GrindM Bool :=
   return isSameExpr e (← getTrueExpr)

tests/lean/run/grind_9830.lean

@@ -0,0 +1,12 @@
+abbrev F : Fin 3 → Nat
+| 0 => 0
+| 1 => 1
+| 2 => 2
+
+abbrev Pairwise (r : α → α → Prop) :=
+  ∀ ⦃i j⦄, i ≠ j → r i j
+
+abbrev onFun (f : β → β → φ) (g : α → β) : α → α → φ := fun x y => f (g x) (g y)
+
+example : Pairwise (onFun (fun a b => a + b < 10) fun x ↦ F x) := by
+  grind