Behaviour of ring tactic

Stream: general

[Florent Schaffhauser]

I have an example of algebraic identity in a ring where ring_nf makes no progress but, if I assume that the ring in question is a field, then ring_nf closes the goal.

example {R : Type} [Ring R] (u a v p q : R) : (u + a * v) + (p + a * q) = (u + p) + a * (v + q) := by
{
  ring_nf -- makes no progress
  sorry
}

example {R : Type} [Field R] (u a v p q : R) : (u + a * v) + (p + a * q) = (u + p) + a * (v + q) := by
{
  ring_nf  -- closes the goal
}

Is this expected behaviour?

I must be doing something wrong, because specialising to the integers makes the proof work:

example (u a v p q : ℤ) : (u + a * v) + (p + a * q) = (u + p) + a * (v + q) := by
{
  ring_nf -- closes the goal
}

[Kevin Buzzard]

ring only works for commutative rings

[Kim Morrison]

noncomm_ring sometimes suffices for non-commutative rings, but it is a "best effort" tactic, not a decision procedure.

[Asei Inoue]

I think “ring” tactic should provide a suggestion message …
for example “ring tactic is for commutative ring”

[Asei Inoue]

“you probably want to use abel, noncomm_ring…”

[Kevin Buzzard]

Maybe the tactic docstring is the place for those comments?

[Johan Commelin]

The docstring already mentions the commutativity constraint. But I think it is a nice suggestion that ring could complain with Could not synthesize instance of [CommSemiRing ?R] where ?R is replaced by the type of the LHS/RHS in the goal.

[Johan Commelin]

And it could then additionally suggest trying abel or noncomm_ring.

[Florent Schaffhauser]

Yes, an error message like that that would be good! Although in the present case, it is mostly my fault for thinking that Ring means CommRing, so the error message could also say not all rings are commutative! :sweat_smile:

[Asei Inoue]

@Johan Commelin it sounds good!! thank you very much

[Damiano Testa]

Johan Commelin said:

And it could then additionally suggest trying abel or noncomm_ring.

Is it really the case that ring may fail on something non-abelian and abel would succeed?

[Johan Commelin]

import Mathlib.Tactic.Ring

example (R : Type) [Ring R] (x y : R) : x + y = y + x := by ring_nf -- fails

[Damiano Testa]

Touché. Still...

[Damiano Testa]

I'm inclined to say that ring_nf_nf should be abel!

[Kyle Miller]

The ring1 tactic tells you about the instance failure:

example (R : Type) [Ring R] (x y : R) : x + y = y + x := by ring1
/-
failed to synthesize
  CommSemiring R
-/

The issue with ring is that it's defined as

macro (name := ring) "ring" : tactic =>
  `(tactic| first | ring1 | try_this ring_nf)

and this error message is discarded once it goes to the second case.

The ring_nf is a ring1-powered simp, and it's not able to diagnose a missing CommRing instance (it normalizes all CommRing subexpressions).

[Kyle Miller]

If ring_nf could detect that nothing was done (and fail), then the macro could be

macro (name := ring) "ring" : tactic =>
  `(tactic| first | ring1 | try_this ring_nf | ring1)

which should print that "failed to synthesize" error

[Kevin Buzzard]

Damiano Testa said:

Johan Commelin said:

And it could then additionally suggest trying abel or noncomm_ring.

Is it really the case that ring may fail on something non-abelian and abel would succeed?

Just to be clear, abel is assuming the additive structure is commutative, ring is assuming the multiplicative structure is commutative.

[Michael Stoll]

(and the additive structure is commutative even for docs#NonUnitalNonAssocSemiring s ...)

[Kevin Buzzard]

The only example I know of + being used in mathematics to indicate something non-commutative is for ordinals.