max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: OfSemiring.toQ unexpander (#9076)

Browse source 
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
```
This commit is contained in:
Leonardo de Moura 2025-06-29 04:22:24 -07:00 • committed by GitHub
parent 98e868e3d2
commit 8b1d2fc2d5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Grind/Ring/Envelope.lean
View file

@ -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

11
tests/lean/run/grind_semiring.lean
View file

@ -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