Zulip Chat Archive

Stream: general

Topic: sub_eq_add_neg


view this post on Zulip Reid Barton (May 01 2020 at 13:18):

I see the dreaded sub_eq_add_neg was removed from simp! However, maybe some compensatory lemmas involving sub should then be added?

example (n : ) : n - n = 0 := begin
  simp, --  simplify tactic failed to simplify
end

view this post on Zulip Reid Barton (May 01 2020 at 13:23):

I guess I didn't test that this one used to work, but I know a - (a - b) = b did.

view this post on Zulip Gabriel Ebner (May 01 2020 at 13:23):

Yes, they should be added! I only did the bare minimum to get mathlib compiling again. There's probably also lots of lemmas from core that should be marked simp.

view this post on Zulip Reid Barton (May 01 2020 at 13:24):

Did you not encounter much breakage in mathlib then?

view this post on Zulip Gabriel Ebner (May 01 2020 at 13:26):

This was the 3.6 upgrade. 162 files changed, 805 insertions(+), 760 deletions(-). Lots of people helped, but there was a lot of breakage (also from other changes).

view this post on Zulip Reid Barton (May 01 2020 at 13:27):

Ah, fair enough.

view this post on Zulip Reid Barton (May 01 2020 at 13:27):

The new default for binder types of classes is fun. I get a mysterious error about something not being a function, but then I delete whatever comes after the location of the error and the error goes away.

view this post on Zulip Reid Barton (May 01 2020 at 13:29):

(I know I could instead add the funny [] to my structures, but so far it seems better to just go with the flow.)

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 17:36):

sub_self is a simp, why your example fails?

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 17:36):

What do you import?

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 17:37):

It is marked as simp in algebra.group.basic in mathlib.

view this post on Zulip Reid Barton (May 01 2020 at 18:15):

All these attributes should move to the definition site. Also sub_sub_cancel at least should be added as a simp lemma.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 18:32):

Feel free to open a PR ;)


Last updated: May 14 2021 at 21:11 UTC