Stream: general

Topic: limitations of noncomm_ring

Heather Macbeth (Jul 02 2020 at 01:43):

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 (Jul 02 2020 at 02:52):

oh yes, that's definitely a bug

Scott Morrison (Jul 02 2020 at 02:52):

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

Scott Morrison (Jul 02 2020 at 02:52):

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

ohh

Jalex Stark (Jul 02 2020 at 02:53):

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

Jalex Stark (Jul 02 2020 at 02:53):

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

Scott Morrison (Jul 02 2020 at 02:56):

The error message is "simp failed to simplify".

Jalex Stark (Jul 02 2020 at 03:06):

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

Heather Macbeth (Jul 02 2020 at 03:23):

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

Scott Morrison (Jul 02 2020 at 04:48):

patched in #3268

Last updated: May 08 2021 at 04:14 UTC