Zulip Chat Archive

Stream: new members

Topic: squeezing simps


view this post on Zulip Julian Berman (Dec 05 2020 at 22:10):

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?

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 22:12):

bare simp is fine if it closes the goal.

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 22:13):

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.

view this post on Zulip Julian Berman (Dec 05 2020 at 22:15):

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

view this post on Zulip Julian Berman (Dec 05 2020 at 22:19):

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

view this post on Zulip Kevin Buzzard (Dec 05 2020 at 22:20):

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

view this post on Zulip Shing Tak Lam (Dec 06 2020 at 10:12):

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.


Last updated: May 08 2021 at 19:11 UTC