From bdcb7914b5e3f2b89498d9cdd8f923dd20633150 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 26 Dec 2024 04:50:39 +0100
Subject: [PATCH] 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          | 17 +++++++++++++++--
 src/Lean/Meta/Tactic/Grind/Preprocessor.lean |  2 ++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean
index c30a425e2750..82f49e501e66 100644
--- a/src/Lean/Meta/Tactic/Grind/Inv.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean b/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
index 6aa628459464..26e03dd19a8c 100644
--- a/src/Lean/Meta/Tactic/Grind/Preprocessor.lean
+++ b/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