feat: improve counterexamples using ToInt.toInt in grind cutsat (#9065)

This PR improves the counterexamples produced by the `cutsat` procedure
in `grind` when using the `ToInt` gadget.

src/Init/Grind/ToInt.lean

@@ -360,4 +360,15 @@ def Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.
 
 end ToInt
 
+/-
+Remark: `↑a` is notation for `ToInt.toInt a`.
+We want to hide `Lean.Grind.ToInt.toInt` applications in the counterexamples produced by
+the `cutsat` procedure in `grind`.
+-/
+@[app_unexpander ToInt.toInt]
+meta def toIntUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $a:term) => `(↑$a)
+  | _ => throw ()
+
 end Lean.Grind

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.ToInt
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.ModelUtil
 
@@ -25,10 +26,13 @@ private def getCutsatAssignment? (goal : Goal) (node : ENode) : Option Rat := Id
   else
     return none
 
-private def natCast? (e : Expr) : Option Expr :=
-  let_expr NatCast.natCast _ inst a := e | none
-  let_expr instNatCastInt := inst | none
-  some a
+private def natCastToInt? (e : Expr) : Option Expr :=
+  match_expr e with
+  | NatCast.natCast _ inst a =>
+    let_expr instNatCastInt := inst | none
+    some a
+  | Grind.ToInt.toInt _ _ _ a => some a
+  | _ => none
 
 def getAssignment? (goal : Goal) (e : Expr) : MetaM (Option Rat) := do
   let node ← goal.getENode (← goal.getRoot e)
@@ -58,11 +62,11 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
     if (← isIntNatENode node) then
       if let some v ← getAssignment? goal node.self then
         model := assignEqc goal node.self v model
-  -- Assign cast terms
+  -- Assign natCast and toInt terms
   for e in goal.exprs do
     let node ← goal.getENode e
     let i := node.self
-    let some n := natCast? i | pure ()
+    let some n := natCastToInt? i | pure ()
     if model[n]?.isNone then
       let some v := model[i]? | pure ()
       model := assignEqc goal n v model

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

@@ -55,7 +55,7 @@ Returns `true` if `e` should be treated as an interpreted value by the arithmeti
 def isInterpretedTerm (e : Expr) : Bool :=
   isNatNum e || isIntNum e || e.isAppOf ``HAdd.hAdd || e.isAppOf ``HMul.hMul || e.isAppOf ``HSub.hSub
   || 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 ``NatCast.natCast || e.isIte || e.isDIte || e.isAppOf ``OfNat.ofNat || e.isAppOf ``Grind.ToInt.toInt
   || e matches .lit (.natVal _)
 
 /--

tests/lean/run/grind_cutsat_toint_1.lean

@@ -78,3 +78,19 @@ example (a : Fin 4) : 1 < a → a ≠ 2 → a ≠ 3 → False := by
 
 example (a : Fin 2) : a ≠ 0 → a ≠ 1 → False := by
   grind
+
+/--
+trace: [grind.cutsat.model] a := 2
+[grind.cutsat.model] b := 0
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.cutsat.model true in
+example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by
+  grind
+
+-- We use `↑a` when pretty printing `ToInt.toInt a`
+/-- trace: [grind.debug.ring.basis] ↑a + ↑b + -3 * ((↑a + ↑b) / 3) + -1 * ((↑a + ↑b) % 3) = 0 -/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.debug.ring.basis true in
+example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by
+  grind