fix: denotation functions for interfacing CommRing and linarith (#8693)

This PR fixes the denotation functions used to interface the ring and
linarith modules in grind.

Author: leodemoura

src/Init/Grind/CommRing/Poly.lean

@@ -1142,13 +1142,31 @@ end Stepwise
 
 /-! IntModule interface -/
 
+def Mon.denoteAsIntModule [CommRing α] (ctx : Context α) (m : Mon) : α :=
+  match m with
+  | .unit => One.one
+  | .mult pw m => go m (pw.denote ctx)
+where
+  go (m : Mon) (acc : α) : α :=
+    match m with
+    | .unit => acc
+    | .mult pw m => go m (acc * pw.denote ctx)
+
 def Poly.denoteAsIntModule [CommRing α] (ctx : Context α) (p : Poly) : α :=
   match p with
   | .num k => Int.cast k * One.one
-  | .add k m p => Int.cast k * m.denote ctx + denote ctx p
+  | .add k m p => Int.cast k * m.denoteAsIntModule ctx + denoteAsIntModule ctx p
+
+theorem Mon.denoteAsIntModule_go_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon) (acc : α)
+    : denoteAsIntModule.go ctx m acc = acc * m.denote ctx := by
+  induction m generalizing acc <;> simp [*, denoteAsIntModule.go, denote, mul_one, One.one, *, mul_assoc]
+
+theorem Mon.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon)
+    : m.denoteAsIntModule ctx = m.denote ctx := by
+  cases m <;> simp [denoteAsIntModule, denote, denoteAsIntModule_go_eq_denote]; rfl
 
 theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (p : Poly) : p.denoteAsIntModule ctx = p.denote ctx := by
-  induction p <;> simp [*, denoteAsIntModule, denote, mul_one, One.one]
+  induction p <;> simp [*, denoteAsIntModule, denote, mul_one, One.one, Mon.denoteAsIntModule_eq_denote]
 
 open Stepwise
 

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

@@ -67,26 +67,9 @@ def NotIneqCnstr.denoteExpr (c : NotIneqCnstr) : M Expr := do
 private def denoteNum (k : Int) : LinearM Expr := do
   return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← getOne)
 
-def _root_.Lean.Grind.CommRing.Power.denoteAsIntModuleExpr (pw : Grind.CommRing.Power) : LinearM Expr := do
-  let x := (← getRing).vars[pw.x]!
-  if pw.k == 1 then
-    return x
-  else
-    return mkApp2 (← getRing).powFn x (toExpr pw.k)
-
-def _root_.Lean.Grind.CommRing.Mon.denoteAsIntModuleExpr (m : Grind.CommRing.Mon) : LinearM Expr := do
-  match m with
-  | .unit => getOne
-  | .mult pw m => go m (← pw.denoteAsIntModuleExpr)
-where
-  go (m : Grind.CommRing.Mon) (acc : Expr) : LinearM Expr := do
-    match m with
-    | .unit => return acc
-    | .mult pw m => go m (mkApp2 (← getRing).mulFn acc (← pw.denoteAsIntModuleExpr))
-
 def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do
   match p with
   | .num k => denoteNum k
-  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getRing).mulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
+  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).hmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
 end Lean.Meta.Grind.Arith.Linear

tests/lean/run/grind_linarith_1.lean

@@ -52,6 +52,14 @@ example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
     : a ≤ b → b ≤ c → a ≤ c := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
+example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
+    : a < b → b < c + d → a - d < c := by
+  grind
+
+example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
     : a < b → b < c + d → a - d < c := by
   grind
+
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α)
+    : a < b → b < c → c < a → False := by
+  grind