## Stream: general

#### 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


#### 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.

#### 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.

#### Reid Barton (May 01 2020 at 13:24):

Did you not encounter much breakage in mathlib then?

#### 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).

Ah, fair enough.

#### 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.

#### 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.)

#### Yury G. Kudryashov (May 01 2020 at 17:36):

sub_self is a simp, why your example fails?

#### Yury G. Kudryashov (May 01 2020 at 17:36):

What do you import?

#### Yury G. Kudryashov (May 01 2020 at 17:37):

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

#### 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.

#### Yury G. Kudryashov (May 01 2020 at 18:32):

Feel free to open a PR ;)

Last updated: May 14 2021 at 21:11 UTC