From 54dce214d1eabdc8564b83909e67a2f94a7e008d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 12 Aug 2025 08:27:39 -0700
Subject: [PATCH] fix: nondeterminism in `grind ring` (#9867)

This PR fixes a nondeterministic behavior in `grind ring`.

Closes #9825
---
 .../Tactic/Grind/Arith/CommRing/EqCnstr.lean  |  4 +-
 .../Grind/Arith/CommRing/Internalize.lean     |  5 +-
 .../Tactic/Grind/Arith/CommRing/Types.lean    |  2 +
 tests/lean/run/grind_9825.lean                | 58 +++++++++++++++++++
 4 files changed, 66 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/grind_9825.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
index 395366bc25..bbdc5a3767 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
@@ -462,9 +462,9 @@ private def propagateEqs : RingM Unit := do
     if (← checkMaxSteps) then return ()
     let some ra ← toRingExpr? a | unreachable!
     map ← process map a ra
-  for (a, ra) in (← getRing).denote do
+  for (a, ra) in (← getRing).denoteEntries do
     if (← checkMaxSteps) then return ()
-    map ← process map a.expr ra
+    map ← process map a ra
 where
   process (map : PropagateEqMap) (a : Expr) (ra : RingExpr) : RingM PropagateEqMap := do
     let d : PolyDerivation := .input (← ra.toPolyM)
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
index f848f559f9..f99c5ed7d0 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
@@ -123,7 +123,10 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
     setTermRingId e
     markAsCommRingTerm e
-    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyRing fun s => { s with
+      denote := s.denote.insert { expr := e } re
+      denoteEntries := s.denoteEntries.push (e, re)
+    }
   else if let some semiringId ← getSemiringId? type then SemiringM.run semiringId do
     let some re ← sreify? e | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
index 038499f46b..462d54ecbe 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
@@ -187,6 +187,8 @@ structure Ring where
   varMap         : PHashMap ExprPtr Var := {}
   /-- Mapping from Lean expressions to their representations as `RingExpr` -/
   denote         : PHashMap ExprPtr RingExpr := {}
+  /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
+  denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
   nextId         : Nat := 0
   /-- Number of "steps": simplification and superposition. -/
diff --git a/tests/lean/run/grind_9825.lean b/tests/lean/run/grind_9825.lean
new file mode 100644
index 0000000000..68b8566212
--- /dev/null
+++ b/tests/lean/run/grind_9825.lean
@@ -0,0 +1,58 @@
+import Lean.Elab.Command
+
+theorem extracted_1_1 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+theorem extracted_1_2 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+theorem extracted_1_3 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+theorem extracted_1_4 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+theorem extracted_1_5 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+theorem extracted_1_6 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
+  ifpnf ≠ 0 →
+    pBf + ppB = pB * (1 / ifpnf) + ppB →
+      ifpnf / (ppB * ifpnf + pB) = 1 / (ppB + pBf)
+  :=
+  by grind -abstractProof only [cases Or]
+
+open Lean
+run_cmd
+  let env ← getEnv
+  let some (.thmInfo ci_1) := env.find? ``extracted_1_1 | unreachable!
+  let some (.thmInfo ci_2) := env.find? ``extracted_1_2 | unreachable!
+  let some (.thmInfo ci_3) := env.find? ``extracted_1_3 | unreachable!
+  let some (.thmInfo ci_4) := env.find? ``extracted_1_4 | unreachable!
+  let some (.thmInfo ci_5) := env.find? ``extracted_1_5 | unreachable!
+  let some (.thmInfo ci_6) := env.find? ``extracted_1_6 | unreachable!
+  assert! ci_1.value.hash == ci_2.value.hash
+  assert! ci_1.value.hash == ci_3.value.hash
+  assert! ci_1.value.hash == ci_4.value.hash
+  assert! ci_1.value.hash == ci_5.value.hash
+  assert! ci_1.value.hash == ci_6.value.hash