Stream: new members
Topic: squeezing simps
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?
Kevin Buzzard (Dec 05 2020 at 22:12):
bare simp is fine if it closes the goal.
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.
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
Julian Berman (Dec 05 2020 at 22:19):
Yeah not finding that language now, must be my mistake, thanks.
Kevin Buzzard (Dec 05 2020 at 22:20):
I don't think lemmas usually disappear. The problem is that new ones appear!
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 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