why isn't Nat.add_succ a simp lemma?

Stream: general

[Kevin Buzzard]

I am redesigning the levels of the natural number game in preparation for a formal launch in October. One comment I had about the original version (from Scott) was that I do not do a good job at all of teaching simp. The reason for this is clear -- in 2018 I didn't have a clue what simp did -- I was still in the mindset where I optimistically hoped that it "proved all simple things".

But things move on and in NNG4 I will explain how to use the simplifier to prove things such as a+b+c+d+e=e+d+c+b+a. One thing I noticed during my preparation of this stuff was that whilst docs#Nat.add_zero was completely unsurprisingly tagged simp, docs#Nat.add_succ was not. Is there a reason for this? Is this related to the reason we have norm_cast and push_cast: it may not be a good idea to train the simplifier to push succ in any particular direction, and it would be better to have bespoke tactics which move it? In NNG itself I think that it would save a lot of time if it were simp in the sense that the simplifier would then do more automatically.

[Eric Wieser]

For Nat.add_succ : n + Nat.succ m = Nat.succ (n + m), the questions is whether it's more useful to have + on the outside or succ on the outside, and it's easiest to be neutral and not choose

[Chris Hughes]

I think the natural number game is kind of a niche case. When proving things about your definitions you often want to unfold them, but not after you've already proved your basic lemmas. I don't see any reason why one should be preferred, and I think too many simp lemmas can lead to other simp lemmas not triggering (I think it is useful to not have add_assoc and add_comm as simp lemmas for this reason, but I don't know of a concrete reason why.

[Kevin Buzzard]

For NNG it's unambiguously true that you want to pull succs out, and once you have developed enough machinery you then banish succ completely (for example the function is not taught to undergraduates, it being a special case of addition).

[Chris Hughes]

It's difficult to banish succ because the induction tactic still makes goals involving succ.

[Chris Hughes]

I think that's the only barrier to banishing succ which is something I wholeheartedly support.

[Eric Wieser]

I think this might be an argument for local attribute [simp] Nat.add_succ within NNG

[Eric Wieser]

Or perhaps a nng_simps simp set like we have for mlfd_simps

[Chris Hughes]

I agree that would make the nng easier, but I don't know if that's a good thing pedagogically.

[Kevin Buzzard]

Yes! I don't teach simp too early, because then every early level is induction <;> simp [IH]