chore: check whether pointer equality implies structural equality in …

…`grind` (#6451)

This PR checks whether in the internal state of the `grind` tactic
pointer equality implies structural equality.

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

@@ -49,14 +49,27 @@ private def checkParents (e : Expr) : GoalM Unit := do
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty
 
+private def checkPtrEqImpliesStructEq : GoalM Unit := do
+  let nodes ← getENodes
+  for h₁ : i in [: nodes.size] do
+    let n₁ := nodes[i]
+    for h₂ : j in [i+1 : nodes.size] do
+      let n₂ := nodes[i]
+      -- We don't have multiple nodes for the same expression
+      assert! !isSameExpr n₁.self n₂.self
+      -- and the two expressions must not be structurally equal
+      assert! !Expr.equal n₁.self n₂.self
+
 /--
-Check basic invariants if `grind.debug` is enabled.
+Checks basic invariants if `grind.debug` is enabled.
 -/
-def checkInvariants : GoalM Unit := do
+def checkInvariants (expensive := false) : GoalM Unit := do
   if grind.debug.get (← getOptions) then
     for (_, node) in (← get).enodes do
       checkParents node.self
       if isSameExpr node.self node.root then
         checkEqc node
+    if expensive then
+      checkPtrEqImpliesStructEq
 
 end Lean.Meta.Grind

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

@@ -139,6 +139,8 @@ def preprocess (mvarId : MVarId) : PreM State := do
   loop (← mkGoal mvarId)
   if (← isTracingEnabledFor `grind.pre) then
     trace[grind.pre] (← ppGoals)
+  for goal in (← get).goals do
+    discard <| GoalM.run' goal <| checkInvariants (expensive := true)
   get
 
 def preprocessAndProbe (mvarId : MVarId) (p : GoalM Unit) : PreM Unit := do