sub_eq_add_neg

Stream: general

[Reid Barton]

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]

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

[Gabriel Ebner]

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]

Did you not encounter much breakage in mathlib then?

[Gabriel Ebner]

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

[Reid Barton]

Ah, fair enough.

[Reid Barton]

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]

(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]

sub_self is a simp, why your example fails?

[Yury G. Kudryashov]

What do you import?

[Yury G. Kudryashov]

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

[Reid Barton]

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]

Feel free to open a PR ;)