Zulip Chat Archive

Stream: general

Topic: limitations of `noncomm_ring`


view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:52):

oh yes, that's definitely a bug

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:52):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:52):

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

view this post on Zulip Jalex Stark (Jul 02 2020 at 02:53):

ohh

view this post on Zulip Jalex Stark (Jul 02 2020 at 02:53):

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

view this post on Zulip Jalex Stark (Jul 02 2020 at 02:53):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:56):

The error message is "simp failed to simplify".

view this post on Zulip Jalex Stark (Jul 02 2020 at 03:06):

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

view this post on Zulip Heather Macbeth (Jul 02 2020 at 03:23):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:48):

patched in #3268


Last updated: May 08 2021 at 04:14 UTC