noncomm_ring simp lemmas don't apply

Stream: new members

[Darij Grinberg]

Someone here is going along with an example I'm showing on my machine, which works on my machine, but for some reason doesn't on theirs. It's the noncomm_ring tactic saying that noncomm_ring simp lemmas don't apply. This happens for them even if they're trying to prove that a + b = b + a for integers a and b. Is there a known bug?

[Kevin Buzzard]

If it works on one machine and not another, then my first conjecture would be that those machines are using different versions of mathlib, and whoever is having problems should try updating. What is the error? This would be a helpful thing to report.

[Darij Grinberg]

I'll ask her tomorrow. For now I recall the message suggested using abel isntead.

[Darij Grinberg]

hmm, maybe it was failing to find the second operation

[Darij Grinberg]

image.png

[Darij Grinberg]

This is the error she's getting

[Darij Grinberg]

4.21.0

[Darij Grinberg]

but she also gets it for simpler things like proving a + b = b + a for a, b \in \Z

[Darij Grinberg]

this is not a Nat/Int issue

[Aaron Liu]

can reproduce

import Mathlib

-- `noncomm_ring` simp lemmas don't apply; try `abel` instead
example (a b : ℤ) : a + b = b + a := by noncomm_ring

[Aaron Liu]

I think the intent here is that you use abel instead

[Darij Grinberg]

prolly, but I'm scared by the nondeterminism of it all

[Darij Grinberg]

for me it works and i'm on 4.21.0 too

[Aaron Liu]

maybe it's a different commit of mathlib

[Darij Grinberg]

I see. So #version tells you a round number even if you're on a nightly :)

[Aaron Liu]

#version gives you the Lean version, but maybe it's on a different version of mathlib

[Darij Grinberg]

oh!

[Kenny Lau]

is there a #version mathlib?

[Kevin Buzzard]

mathlib doesn't have releases so you may as well just do git log.

[Kevin Buzzard]

I guess one thing to add here is that the naturals are not a non-commutative ring ;-)

[Darij Grinberg]

Yeah, I guess semiring would fit better... but I guess it's not explaining why it's failing for \Z

[Kevin Buzzard]

This also fails with the same error:

import Mathlib

example (R : Type) [Ring R] (a b : R) : a + b = b + a := by
  noncomm_ring

At this point I am thinking that this is unexpected behaviour and you might want to open an issue. Or perhaps the designers are well aware of this issue and are arguing that because you are not using multiplication at all you're using the wrong tactic anyway and should be using the abelian group tactic.

[Aaron Liu]

yes that's how I interpreted it

[Darij Grinberg]

And this seems to be true. Quoting my collaborator: "That makes sense. I didn't update Mathlib, but after rewriting the equation as 1a+1b = 1b+1a, noncomm_ring works now."

[Darij Grinberg]

I must say I was rather surprised that a tactic(!) is defined in mathlib rather than in Lean proper. But I guess this is what you get when tactics are so easy to define :)

[Aaron Liu]

rings are defined in mathlib (well I guess now that we have grind they're also defined in core)

[Robin Arnez]

I guess it'd be even more surprising to you then that in fact the majority of tactics don't come from core (253 from core, 266 directly from mathlib, 39 from a dependency of mathlib)