limitations of `noncomm_ring`

Stream: general

[Heather Macbeth]

The tactic noncomm_ring (source) cannot do the following problem; should it be able to? Note that abel can, and noncomm_ring is built on top of abel.

import tactic.noncomm_ring

-- works
example {R : Type*} [ring R] (a b : R) : a + -b = -b + a := by abel

-- fails
example {R : Type*} [ring R] (a b : R) : a + -b = -b + a := by noncomm_ring

[Scott Morrison]

oh yes, that's definitely a bug

[Scott Morrison]

wrap the simp only [...] call in noncomm_ring with try { ... }

[Scott Morrison]

or use the { fail_if_unchanged := ff } configuration option for simp.

[Jalex Stark]

ohh

[Jalex Stark]

I thought the problem was that the simp only [...] was making negative progress

[Jalex Stark]

but the problem is that it makes 0 progress, so it fails?

[Scott Morrison]

The error message is "simp failed to simplify".

[Jalex Stark]

that'll teach me not to form such a strong opinion without running the code

[Heather Macbeth]

Thanks for the diagnosis, @Scott Morrison ! I filed an issue report, #3267 .

[Scott Morrison]

patched in #3268