why ring doesn't work on ring

Stream: new members

[Xiyu Zhai]

Hi, I'm frustrated when trying to make the following thing work:

import Mathlib

open Ring

-- good
example (R : Type) [Ring R] (a b c : R) : x + 1 = 1 + x := by ring

-- good
example (a b c: ℤ) : a * (b + c) = a * b + a * c := by ring

-- good
example (R : Type) [Ring R] (a b c : R) : a * (b + c) = a * b + a * c := by
  apply mul_add

-- failed
-- vscode error message:
-- unsolved goals
-- R : Type
-- inst✝ : Ring R
-- a b c : R
-- ⊢ a * (b + c) = a * b + a * cLean 4
example (R : Type) [Ring R] (a b c : R) : a * (b + c) = a * b + a * c := by
  ring

All but the last one work. It says unsolved goal for the last one.

Did I miss an import or something?

[David Renshaw]

the noncomm_ring tactic works here

[David Renshaw]

and ring works if you have [CommRing R] instead of [Ring R].

[Xiyu Zhai]

thanks. But may I ask why? Is it a current limitation of the ring tactics? Or rather, ring tactics is for comm rings. But Ring is for general ring.

[David Renshaw]

some previous discussion: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Behaviour.20of.20ring.20tactic/near/436205094

[Xiyu Zhai]

That's extremely helpful!!!

[Jireh Loreaux]

If we updated the try_this tactic to:

/-- Produces the text `Try this: <tac>` with the given tactic, and then executes it. -/
elab tk:"try_this" tac:tactic info:(str)? : tactic => do
  Elab.Tactic.evalTactic tac
  Meta.Tactic.TryThis.addSuggestion tk tac (origSpan? := ← getRef)
  match info with
  | some info => logInfoAt (← getRef) m!"{info}"
  | none => pure ()

Then when it's used in a macro like ring that macro can provide a custom message to go with the suggestion. Here would could include common pitfalls. Something like:
"ring failed to close the goal. If you're working in a noncommutative ring, abelian group or module, try noncomm_ring, abel or module, respectively."

[Jireh Loreaux]

Also, what is the better way to write that match. I know it must be something easy.

[Eric Wieser]

if let .some info := info then

[Eric Wieser]

But I think the message should be handled as part of addSuggestion, which already lets you specify pre / post text

[Jireh Loreaux]

I thought it only let you specify pre text? I was thinking of the header that can be changed, which is different from the preinfo or postinfo.

[Jireh Loreaux]

#19763

[Jireh Loreaux]

In case we're going to meet: https://siue.zoom.us/j/91006322517?pwd=cI31tlyKTehpABaRRstBi8c48RmAf6.1