Zulip Chat Archive

Stream: general

Topic: can we make a core lemma into a simp lemma


Johan Commelin (Aug 07 2018 at 12:31):

nat.sub_self is in core. I think it should be a simp lemma. Can we add such an attribute post-hoc in a mathlib file?

Sean Leather (Aug 07 2018 at 12:32):

attribute [simp] nat.sub_self

Kevin Buzzard (Aug 07 2018 at 12:39):

or local attribute [simp] nat.sub_self if you're scared that making it a simp lemma more globally will cause other problems. I see that the additive group version sub_self isn't a simp lemma either. This might be something to do with subtraction being involved. I think a - b = a + (-b) is a simp lemma and because of this simp might change your a - a to a + (-a) before it notices your attribute.

We were talking about a related thing a day or two ago, where simp just failed to simplify quite a complicated thing because it couldn't manage a + (b + -a) = b.

Johan Commelin (Aug 07 2018 at 12:45):

Right. But I think whenever n : nat and you encounter (n - n) somewhere in your goal, there should be no harm at all if you replace it with 0 : nat...

Johan Commelin (Aug 07 2018 at 12:45):

Maybe I just don't understand simp.

Mario Carneiro (Aug 07 2018 at 12:45):

nat.sub_self should be a simp lemma. We can add it to data.nat.basic. As I've mentioned, sub_self will never trigger as a simp lemma

Johan Commelin (Aug 07 2018 at 12:47):

Right... because "group vs semigroup" ?

Mario Carneiro (Aug 07 2018 at 12:48):

nat.sub is not the same as the one defined for additive groups

Mario Carneiro (Aug 07 2018 at 12:48):

the sub-unfolding simp lemma only applies to the additive group sub

Mario Carneiro (Aug 07 2018 at 12:48):

of course n + -n doesn't even make sense over nat

Kevin Buzzard (Aug 07 2018 at 13:01):

Aah very nice :-) Is there any way of telling simp to try sub_self before trying the dreaded sub_eq_add_neg?


Last updated: Dec 20 2023 at 11:08 UTC