feat: improve grind linarith counterexamples for NatModule

This PR improves the counterexamples produced by `grind linarith` for
`NatModule`s. `grind` now hides occurrences of the auxiliary function
`Grind.IntModule.OfNatModule.toQ`.

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.ModelUtil
+import Init.Grind.Module.Envelope
 public section
 namespace Lean.Meta.Grind.Arith.Linear
 
@@ -22,6 +23,11 @@ private def hasType (type : Expr) (n : ENode): MetaM Bool :=
     let type' ← inferType n.self
     isDefEq type' type
 
+private def toQ? (e : Expr) : Option Expr :=
+  match_expr e with
+  | Grind.IntModule.OfNatModule.toQ _ _ a => some a
+  | _ => none
+
 /--
 Construct a model that satisfies all constraints in the linarith model for the structure with id `structId`.
 It also assigns values to (integer) terms that have not been internalized by the linarith model.
@@ -36,6 +42,14 @@ def mkModel (goal : Goal) (structId : Nat) : MetaM (Array (Expr × Rat)) := do
     if (← hasType s.type node) then
       if let some v := getAssignment? s node.self then
         model := assignEqc goal node.self v model
+  -- Assign `toQ a` terms
+  for e in goal.exprs do
+    let node ← goal.getENode e
+    let i := node.self
+    let some n := toQ? i | pure ()
+    if model[n]?.isNone then
+      let some v := model[i]? | pure ()
+      model := assignEqc goal n v model
   let r ← finalizeModel goal (hasType s.type) model
   traceModel `grind.linarith.model r
   return r

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

@@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Data.Rat.Basic
-
+import Init.Grind.Module.Envelope
 public section
 
 namespace Lean.Meta.Grind.Arith
@@ -60,7 +59,7 @@ def isInterpretedTerm (e : Expr) : Bool :=
   isNatNum e || isIntNum e || e.isAppOf ``HAdd.hAdd || e.isAppOf ``HMul.hMul || e.isAppOf ``HSub.hSub || e.isAppOf ``HSMul.hSMul
   || e.isAppOf ``Neg.neg || e.isAppOf ``HDiv.hDiv || e.isAppOf ``HMod.hMod || e.isAppOf ``One.one || e.isAppOf ``Zero.zero
   || e.isAppOf ``NatCast.natCast || e.isIte || e.isDIte || e.isAppOf ``OfNat.ofNat || e.isAppOf ``Grind.ToInt.toInt
-  || e matches .lit (.natVal _)
+  || e.isAppOf ``Grind.IntModule.OfNatModule.toQ || e matches .lit (.natVal _)
 
 /--
 Adds the assignments `e' := v` to `a` for each `e'` in the equivalence class os `e`.

tests/lean/run/grind_nat_module.lean

@@ -54,3 +54,15 @@ end
 example [NatModule α] [AddRightCancel α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c d : α)
     : a ≤ b → a ≥ c + d → d ≤ 0 → d ≥ 0 → b = c → a = b := by
   grind
+
+/--
+trace: [grind.linarith.model] a := 0
+[grind.linarith.model] b := 1
+[grind.linarith.model] c := 1
+[grind.linarith.model] d := -2
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.linarith.model true in
+example [NatModule α] [AddRightCancel α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedAdd α] (a b c d : α)
+    : a ≤ b → a ≥ c + d → b = c → a = b := by
+  grind