feat: add functions for converting ring reified terms back into Expr (#8033)

This PR adds functions for converting `CommRing` reified terms back into
Lean expressions.

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -14,11 +14,16 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Eq
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 
 namespace Lean
 
 builtin_initialize registerTraceClass `grind.ring
 builtin_initialize registerTraceClass `grind.ring.internalize
 builtin_initialize registerTraceClass `grind.ring.assert
+builtin_initialize registerTraceClass `grind.ring.assert.unsat (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true)
 
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+
+namespace Lean.Meta.Grind.Arith.CommRing
+/-!
+Helper functions for converting reified terms back into their denotations.
+-/
+
+private def denoteNum (ring : Ring) (k : Int) : MetaM Expr := do
+  return mkApp ring.intCastFn (toExpr k)
+
+def _root_.Lean.Grind.CommRing.Power.denoteExpr' (ring : Ring) (pw : Power) : MetaM Expr := do
+  let x := ring.vars[pw.x]!
+  if pw.k == 1 then
+    return x
+  else
+    return mkApp2 ring.powFn x (toExpr pw.k)
+
+def _root_.Lean.Grind.CommRing.Mon.denoteExpr' (ring : Ring) (m : Mon) : MetaM Expr := do
+  match m with
+  | .unit => denoteNum ring 1
+  | .mult pw m => go m (← pw.denoteExpr' ring)
+where
+  go (m : Mon) (acc : Expr) : MetaM Expr := do
+    match m with
+    | .unit => return acc
+    | .mult pw m => go m (mkApp2 ring.mulFn acc (← pw.denoteExpr' ring))
+
+def _root_.Lean.Grind.CommRing.Poly.denoteExpr' (ring : Ring) (p : Poly) : MetaM Expr := do
+  match p with
+  | .num k => denoteNum ring k
+  | .add k m p => go p (← denoteTerm k m)
+where
+  denoteTerm (k : Int) (m : Mon) : MetaM Expr := do
+    if k == 1 then
+      m.denoteExpr' ring
+    else
+      return mkApp2 ring.mulFn (← denoteNum ring k) (← m.denoteExpr' ring)
+
+  go (p : Poly) (acc : Expr) : MetaM Expr := do
+    match p with
+    | .num 0 => return acc
+    | .num k => return mkApp2 ring.addFn acc (← denoteNum ring k)
+    | .add k m p => go p (mkApp2 ring.addFn acc (← denoteTerm k m))
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (ring : Ring) (e : RingExpr) : MetaM Expr := do
+  go e
+where
+  go : RingExpr → MetaM Expr
+  | .num k => denoteNum ring k
+  | .var x => return ring.vars[x]!
+  | .add a b => return mkApp2 ring.addFn (← go a) (← go b)
+  | .sub a b => return mkApp2 ring.subFn (← go a) (← go b)
+  | .mul a b => return mkApp2 ring.mulFn (← go a) (← go b)
+  | .pow a k => return mkApp2 ring.powFn (← go a) (toExpr k)
+  | .neg a => return mkApp ring.negFn (← go a)
+
+def _root_.Lean.Grind.CommRing.Power.denoteExpr (ringId : Nat) (pw : Power) : GoalM Expr := do
+  pw.denoteExpr' (← getRing ringId)
+
+def _root_.Lean.Grind.CommRing.Mon.denoteExpr (ringId : Nat) (m : Mon) : GoalM Expr := do
+  m.denoteExpr' (← getRing ringId)
+
+def _root_.Lean.Grind.CommRing.Poly.denoteExpr (ringId : Nat) (p : Poly) : GoalM Expr := do
+  p.denoteExpr' (← getRing ringId)
+
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (ringId : Nat) (e : RingExpr) : GoalM Expr := do
+  e.denoteExpr' (← getRing ringId)
+
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Eq.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
@@ -30,26 +31,42 @@ private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
   if isSameExpr a b then return () -- TODO: check why this is needed
   let some ringId ← inSameRing? a b | return ()
-  trace[grind.ring] "{← mkEq a b}"
+  trace[grind.ring.assert] "{← mkEq a b}"
   let some ra ← toRingExpr? ringId a | return ()
   let some rb ← toRingExpr? ringId b | return ()
-  let p ← toPoly ringId (ra.sub rb)
+  let p ← (ra.sub rb).toPolyM ringId
   if let .num k := p then
-    if k != 0 && (← hasChar ringId) then
+    if k == 0 then
+      trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} = 0"
+    else if (← hasChar ringId) then
+      trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} = 0"
       setEqUnsat ringId k a b ra rb
-      return ()
+    else
+      -- Remark: we currently don't do anything if the characteristic is not known.
+      trace[grind.ring.assert.discard] "{← p.denoteExpr ringId} = 0"
+    return ()
+
+  trace[grind.ring.assert.store] "{← p.denoteExpr ringId} = 0"
   -- TODO: save equality
 
 @[export lean_process_ring_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
   let some ringId ← inSameRing? a b | return ()
-  trace[grind.ring] "{mkNot (← mkEq a b)}"
+  trace[grind.ring.assert] "{mkNot (← mkEq a b)}"
   let some ra ← toRingExpr? ringId a | return ()
   let some rb ← toRingExpr? ringId b | return ()
-  let p ← toPoly ringId (ra.sub rb)
-  if p == .num 0 then
-    setNeUnsat ringId a b ra rb
+  let p ← (ra.sub rb).toPolyM ringId
+  if let .num k := p then
+    if k == 0 then
+      trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} ≠ 0"
+      setNeUnsat ringId a b ra rb
+    else
+      -- Remark: if the characteristic is known, it is trivial.
+      -- Otherwise, we don't do anything.
+      trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} ≠ 0"
     return ()
+
+  trace[grind.ring.assert.store] "{← p.denoteExpr ringId} ≠ 0"
   -- TODO: save disequalitys
 
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -30,12 +30,10 @@ private def mkLemmaPrefix (ringId : Nat) (declName declNameC : Name) : GoalM Exp
     return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx
 
 def setNeUnsat (ringId : Nat) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
-  trace[grind.ring.assert] "unsat diseq {a}, {b}"
   let h ← mkLemmaPrefix ringId ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
   closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b)
 
 def setEqUnsat (ringId : Nat) (k : Int) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
-  trace[grind.ring.assert] "unsat eq {a}, {b}"
   let mut h ← mkLemmaPrefix ringId ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
   let (charInst, c) ← getCharInst ringId
   if c == 0 then

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean

@@ -66,7 +66,7 @@ def getCharInst (ringId : Nat) : GoalM (Expr × Nat) := do
 Converts the given ring expression into a multivariate polynomial.
 If the ring has a nonzero characteristic, it is used during normalization.
 -/
-def toPoly (ringId : Nat) (e : RingExpr) : GoalM Poly := do
+def _root_.Lean.Grind.CommRing.Expr.toPolyM (ringId : Nat) (e : RingExpr) : GoalM Poly := do
   if let some c ← nonzeroChar? ringId then
     return e.toPolyC c
   else