Tool to convert `simp` to `simp only`

Stream: lean4

[Mrigank Pawagi]

Hey all, I am an undergraduate learning Lean in a class this semester. I have been working on a course project, which I will soon be turning in. We discussed in class that since the behaviour of simp can change over updates, it is best practice to only have simp only in order to make code robust and maintainable. However, my code was riddled with 450+ unguarded simp statements, and converting them to simp only by first changing them to simp? and then clicking the suggestion in the infoview seemed to be very tedious.

I therefore made a small tool which does this in quite a hacky way: https://github.com/mrigankpawagi/simpleafier. I was able to transform all of my simps in less than 30 seconds (with the "fast" mode) and had to spend only a minute or two more fixing 2 small errors that came up after the transformation.

I would like to know if there's a cleaner way to do this that other people are aware of, for example, from inside Lean? I would also be happy to hear any feedback or suggestions. (PS my course project is here).

[Michael Rothgang]

Thanks for asking, that's an interesting question!
Let me start with more of a side point: not all simps are bad: if a simp closes a goal (it's a "terminal simp"), leaving it as simp is usually fine. (In fact, mathlib policy asks for such simps to be simp and not simp onlys.)
This leads me to a related tool: mathlib's flexible linter. You can activate it with set_option linter.flexible true in a file (or change your lakefile; if you don't know what this is, going file by file may be good enough). The linter will complain about every "non-terminal simp" (but will leave terminal simps alone) --- so you could use the linter as a means of checking "which simps do I actually need to change".

[Michael Rothgang]

(If you're not on a very recent mathlib, you may need to import Mathlib.Tactic.Linter.Flexible to make the set_option work. On recent mathlib, that is never necessary any more.)

[Mrigank Pawagi]

Thanks for your answer. You're right! My tool does, in fact, leave many simp onlys at the end of proofs (it was a little tricky to manage them automatically).

Good to know that there is a linter to help with this. It is generally better to take care of this while writing the proofs in the first place (before one ends up in a situation like mine with hundreds of bad simps :smiley:)!

[Mrigank Pawagi]

I have added set_option linter.flexible true to my file. It does not complain about terminal simp onlys though :sweat_smile:. For that I might just have to ctrl+F and check

[Michael Rothgang]

Indeed, the linter (currently) only checks one implication.

[Michael Rothgang]

@Damiano Testa How difficult would it be to lint for terminal simps which are squeezed? (That should probably be covered by a new option, and cannot be enabled in mathlib yet either --- but it could help here or in downstream projects.)