From 388b6f045bd6d79df9b503d55eef6688ceb8f647 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 8 Apr 2025 14:01:07 -0700
Subject: [PATCH] chore: avoid unnecessary quotations in cutsat traces and
 counterexamples (#7877)

cc @kim-em
---
 src/Lean/Message.lean                          |  7 -------
 .../Meta/Tactic/Grind/Arith/Cutsat/Model.lean  |  2 +-
 .../Meta/Tactic/Grind/Arith/Cutsat/Search.lean |  8 ++++----
 .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean   |  8 ++++----
 .../Meta/Tactic/Grind/Arith/Offset/Model.lean  |  2 +-
 src/Lean/Meta/Tactic/Grind/Arith/Util.lean     | 18 ++++++++++++++++++
 src/Lean/Meta/Tactic/Grind/PP.lean             |  4 ++--
 tests/lean/run/grind_cutsat_div_1.lean         |  4 ++--
 tests/lean/run/grind_cutsat_eq_1.lean          |  4 ++--
 tests/lean/run/grind_cutsat_nat_le.lean        |  2 +-
 tests/lean/run/grind_mbtc_1.lean               | 12 ++++++------
 11 files changed, 41 insertions(+), 30 deletions(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index cda2165b51..b2c1c6b8b9 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -509,13 +509,6 @@ def indentExpr (e : Expr) : MessageData :=
 def aquote (msg : MessageData) : MessageData :=
   "「" ++ msg ++ "」"
 
-/-- Quote `e` using `「` and `」` if `e` is not a free variable, constant, or literal. -/
-def quoteIfNotAtom (e : Expr) : MessageData :=
-  if e.isFVar || e.isConst || e.isLit then
-    e
-  else
-    aquote e
-
 class AddMessageContext (m : Type → Type) where
   /--
   Without context, a `MessageData` object may be missing information
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
index 620217c1af..40d5e3b99f 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
@@ -122,7 +122,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
   r := r.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
   if (← isTracingEnabledFor `grind.cutsat.model) then
     for (x, v) in r do
-      trace[grind.cutsat.model] "{quoteIfNotAtom x} := {v}"
+      trace[grind.cutsat.model] "{quoteIfArithTerm x} := {v}"
   return r
 
 end Lean.Meta.Grind.Arith.Cutsat
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
index 28de53482f..5c4fb5a0bd 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
@@ -59,7 +59,7 @@ private def checkIsNextVar (x : Var) : GoalM Unit := do
     throwError "`grind` internal error, assigning variable out of order"
 
 private def traceAssignment (x : Var) (v : Rat) : GoalM Unit := do
-  trace[grind.cutsat.assign] "{quoteIfNotAtom (← getVar x)} := {v}"
+  trace[grind.cutsat.assign] "{quoteIfArithTerm (← getVar x)} := {v}"
 
 private def setAssignment (x : Var) (v : Rat) : GoalM Unit := do
   checkIsNextVar x
@@ -419,15 +419,15 @@ def processVar (x : Var) : SearchM Unit := do
   | some (lower, _), none =>
     let lower := lower.ceil
     let v := dvdSol.geAvoiding lower diseqVals
-    trace[grind.debug.cutsat.search] "{lower} ≤ {quoteIfNotAtom (← getVar x)} := {v}"
+    trace[grind.debug.cutsat.search] "{lower} ≤ {quoteIfArithTerm (← getVar x)} := {v}"
     setAssignment x v
   | none, some (upper, _) =>
     let upper := upper.floor
     let v := dvdSol.leAvoiding upper diseqVals
-    trace[grind.debug.cutsat.search] "{quoteIfNotAtom (← getVar x)} := {v} ≤ {upper}"
+    trace[grind.debug.cutsat.search] "{quoteIfArithTerm (← getVar x)} := {v} ≤ {upper}"
     setAssignment x v
   | some (lower, c₁), some (upper, c₂) =>
-    trace[grind.debug.cutsat.search] "{lower} ≤ {lower.ceil} ≤ {quoteIfNotAtom (← getVar x)} ≤ {upper.floor} ≤ {upper}"
+    trace[grind.debug.cutsat.search] "{lower} ≤ {lower.ceil} ≤ {quoteIfArithTerm (← getVar x)} ≤ {upper.floor} ≤ {upper}"
     trace[grind.debug.cutsat.getBestLower] "lower: {lower}, c₁: {← c₁.pp}"
     if lower > upper then
       let .true ← resolveRealLowerUpperConflict c₁ c₂
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
index 59873736bd..c59cf03355 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -87,15 +87,15 @@ def resetAssignmentFrom (x : Var) : GoalM Unit := do
 def _root_.Int.Linear.Poly.pp (p : Poly) : GoalM MessageData := do
   match p with
   | .num k => return m!"{k}"
-  | .add 1 x p => go (quoteIfNotAtom (← getVar x)) p
-  | .add k x p => go m!"{k}*{quoteIfNotAtom (← getVar x)}" p
+  | .add 1 x p => go (quoteIfArithTerm (← getVar x)) p
+  | .add k x p => go m!"{k}*{quoteIfArithTerm (← getVar x)}" p
 where
   go (r : MessageData)  (p : Int.Linear.Poly) : GoalM MessageData := do
     match p with
     | .num 0 => return r
     | .num k => return m!"{r} + {k}"
-    | .add 1 x p => go m!"{r} + {quoteIfNotAtom (← getVar x)}" p
-    | .add k x p => go m!"{r} + {k}*{quoteIfNotAtom (← getVar x)}" p
+    | .add 1 x p => go m!"{r} + {quoteIfArithTerm (← getVar x)}" p
+    | .add k x p => go m!"{r} + {k}*{quoteIfArithTerm (← getVar x)}" p
 
 def _root_.Int.Linear.Poly.denoteExpr' (p : Poly) : GoalM Expr := do
   let vars ← getVars
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean
index b156ba24ec..ffefc71bde 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean
@@ -76,7 +76,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
   r := r.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
   if (← isTracingEnabledFor `grind.offset.model) then
     for (x, v) in r do
-      trace[grind.offset.model] "{quoteIfNotAtom x} := {v}"
+      trace[grind.offset.model] "{quoteIfArithTerm x} := {v}"
   return r
 
 end Lean.Meta.Grind.Arith.Offset
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
index 33f7293dc7..9ab1ba163c 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Util.lean
@@ -64,4 +64,22 @@ partial def isRelevantPred (e : Expr) : Bool :=
   | Dvd.dvd α _ _ _ => isSupportedType α
   | _ => false
 
+def isArithTerm (e : Expr) : Bool :=
+  match_expr e with
+  | HAdd.hAdd _ _ _ _ _ _ => true
+  | HSub.hSub _ _ _ _ _ _ => true
+  | HMul.hMul _ _ _ _ _ _ => true
+  | HDiv.hDiv _ _ _ _ _ _ => true
+  | HMod.hMod _ _ _ _ _ _ => true
+  | Neg.neg _ _ _ => true
+  | OfNat.ofNat _ _ _ => true
+  | _ => false
+
+/-- Quote `e` using `「` and `」` if `e` is an arithmetic term that is being treated as a variable. -/
+def quoteIfArithTerm (e : Expr) : MessageData :=
+  if isArithTerm e then
+    aquote e
+  else
+    e
+
 end Lean.Meta.Grind.Arith
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index 60d4607451..395b4dd043 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -126,7 +126,7 @@ private def ppOffset : M Unit := do
   if model.isEmpty then return ()
   let mut ms := #[]
   for (e, val) in model do
-    ms := ms.push <| .trace { cls := `assign } m!"{quoteIfNotAtom e} := {val}" #[]
+    ms := ms.push <| .trace { cls := `assign } m!"{Arith.quoteIfArithTerm e} := {val}" #[]
   pushMsg <| .trace { cls := `offset } "Assignment satisfying offset constraints" ms
 
 private def ppCutsat : M Unit := do
@@ -138,7 +138,7 @@ private def ppCutsat : M Unit := do
   if model.isEmpty then return ()
   let mut ms := #[]
   for (e, val) in model do
-    ms := ms.push <| .trace { cls := `assign } m!"{quoteIfNotAtom e} := {val}" #[]
+    ms := ms.push <| .trace { cls := `assign } m!"{Arith.quoteIfArithTerm e} := {val}" #[]
   pushMsg <| .trace { cls := `cutsat } "Assignment satisfying linear constraints" ms
 
 private def ppThresholds (c : Grind.Config) : M Unit := do
diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean
index bb35017683..2bccc78c1c 100644
--- a/tests/lean/run/grind_cutsat_div_1.lean
+++ b/tests/lean/run/grind_cutsat_div_1.lean
@@ -73,8 +73,8 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): Fals
   sorry
 
 /--
-info: [grind.cutsat.assign] 「f 0」 := 11
-[grind.cutsat.assign] 「f 1」 := 2
+info: [grind.cutsat.assign] f 0 := 11
+[grind.cutsat.assign] f 1 := 2
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.assign true in
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index c06c426f37..43f1f5a6d6 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -6,8 +6,8 @@ open Int.Linear
 -- set_option trace.grind.cutsat.internalize true
 
 /--
-info: [grind.cutsat.eq] -1*「b + f a + 1」 + b + 「f a」 + 1 = 0
-[grind.cutsat.eq] b + 「f a」 + 1 = 0
+info: [grind.cutsat.eq] -1*「b + f a + 1」 + b + f a + 1 = 0
+[grind.cutsat.eq] b + f a + 1 = 0
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.eq true in
diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean
index ccd51b3200..c0553ae357 100644
--- a/tests/lean/run/grind_cutsat_nat_le.lean
+++ b/tests/lean/run/grind_cutsat_nat_le.lean
@@ -30,7 +30,7 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
 
 /--
 info: [grind.debug.cutsat.eq] c = 0
-[grind.cutsat.assert] 「↑c」 = 0
+[grind.cutsat.assert] ↑c = 0
 -/
 #guard_msgs (info) in
 set_option trace.grind.debug.cutsat.eq true in
diff --git a/tests/lean/run/grind_mbtc_1.lean b/tests/lean/run/grind_mbtc_1.lean
index 504bd79feb..7a466b7a00 100644
--- a/tests/lean/run/grind_mbtc_1.lean
+++ b/tests/lean/run/grind_mbtc_1.lean
@@ -10,8 +10,8 @@ example (f : Int → Int) (x : Int)
 -- but `f x` and `f 1` have different assignments.
 /--
 info: [grind.cutsat.model] x := 1
-[grind.cutsat.model] 「f x」 := 2
-[grind.cutsat.model] 「f 1」 := 5
+[grind.cutsat.model] f x := 2
+[grind.cutsat.model] f 1 := 5
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.model true in
@@ -22,8 +22,8 @@ example (f : Int → Int) (x : Int)
 
 /--
 info: [grind.cutsat.model] x := 2
-[grind.cutsat.model] 「f x」 := 2
-[grind.cutsat.model] 「f 1」 := 5
+[grind.cutsat.model] f x := 2
+[grind.cutsat.model] f 1 := 5
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.model true in
@@ -57,8 +57,8 @@ example (f : Int → α) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x
 info: [grind.cutsat.model] x := 7
 [grind.cutsat.model] y := 8
 [grind.cutsat.model] b := 3
-[grind.cutsat.model] 「f 3」 := 8
-[grind.cutsat.model] 「f (b + 1)」 := 7
+[grind.cutsat.model] f 3 := 8
+[grind.cutsat.model] f (b + 1) := 7
 -/
 #guard_msgs (info) in
 set_option trace.grind.cutsat.model true in