fix: nondeterminism in grind ring (#9867)

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

Closes #9825

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)

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}"

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. -/

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