squeezing simps

Stream: new members

[Julian Berman]

Is it considered useful to replace bare simps in mathlib with simp only ones? I'm reading a file for other reasons (it's algebra/group/basic) which has a bunch of bare ones. Or is that not useful considering the lemmas simp are using for this file are unlikely to disappear?

[Kevin Buzzard]

bare simp is fine if it closes the goal.

[Kevin Buzzard]

This is a maintenance issue. simp gets better over time, so simp in the middle of a goal might change behaviour making code hard to maintain. simp only is far less likely to change even if new simp lemmas are added.

[Julian Berman]

Got it OK -- I thought I saw a note in the docs that they weren't desirable entirely because if a proof using bare simp starts to fail you don't know what lemma that disappeared is the one that was relied on (whereas if you have the explicit list you at least maybe guess at what the lemma said or something). Maybe that was referring to something else

[Julian Berman]

Yeah not finding that language now, must be my mistake, thanks.

[Kevin Buzzard]

I don't think lemmas usually disappear. The problem is that new ones appear!

[Shing Tak Lam]

Also worth noting - sometimes simp only can be a lot faster than just simp. In #3963 I (mostly) just replaced simp with simp only, and the time required to check that file halved, for one lemma it went from 40 seconds to 2.