From 8b1d2fc2d5545418e43d8aeba632ca085d601b9a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 29 Jun 2025 04:22:24 -0700
Subject: [PATCH] feat: `OfSemiring.toQ` unexpander (#9076)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds an unexpander for `OfSemiring.toQ`. This an auxiliary
function used by the `ring` module in `grind`, but we want to reduce the
clutter in the diagnostic information produced by `grind`. Example:
```
example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α)
    : x^2*y = 1 → x*y^2 = y → x + y = 2 → False := by
  grind
```
produces
```
  [ring] Ring `Ring.OfSemiring.Q α` ▼
    [basis] Basis ▼
      [_] ↑x + ↑y + -2 = 0
      [_] ↑y + -1 = 0
```
---
 src/Init/Grind/Ring/Envelope.lean  | 12 +++++++++++-
 tests/lean/run/grind_semiring.lean | 11 +++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean
index 3d08cbce6f..540b086902 100644
--- a/src/Init/Grind/Ring/Envelope.lean
+++ b/src/Init/Grind/Ring/Envelope.lean
@@ -503,6 +503,16 @@ def ofCommSemiring : CommRing (OfSemiring.Q α) :=
 
 attribute [instance] ofCommSemiring
 
-end OfCommSemiring
+/-
+Remark: `↑a` is notation for `OfSemring.toQ a`.
+We want to hide `OfSemring.toQ` applications in the diagnostic information produced by
+the `ring` procedure in `grind`.
+-/
+@[app_unexpander OfSemiring.toQ]
+meta def toQUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $a:term) => `(↑$a)
+  | _ => throw ()
 
+end OfCommSemiring
 end Lean.Grind.CommRing
diff --git a/tests/lean/run/grind_semiring.lean b/tests/lean/run/grind_semiring.lean
index 4ff1f58015..5b6df96092 100644
--- a/tests/lean/run/grind_semiring.lean
+++ b/tests/lean/run/grind_semiring.lean
@@ -28,3 +28,14 @@ example [CommSemiring α] [AddRightCancel α] (x y : α) : x^2*y = 1 → x*y^2 =
 
 example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α) : x^2*y = 1 → x*y^2 = y → x + y = 1 → False := by
   grind
+
+/--
+trace: [grind.ring.assert.basis] ↑x + ↑y + -2 = 0
+[grind.ring.assert.basis] ↑y ^ 3 + -4 * ↑y ^ 2 + 4 * ↑y + -1 = 0
+[grind.ring.assert.basis] 2 * ↑y ^ 2 + -3 * ↑y + 1 = 0
+[grind.ring.assert.basis] ↑y + -1 = 0
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.ring.assert.basis true in
+example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α) : x^2*y = 1 → x*y^2 = y → x + y = 2 → False := by
+  grind