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.)

[Damiano Testa]

Arriving late here.

On the one hand, the flexible linter was written before the "do not squeeze terminal simps" policy started, so it does not have any awareness of this.

On the other hand, the linter already does so much with investigating the metavariable context that adding a check that terminal simps are not squeezed should be really easy.

Even more, if you make your code compliant with the multiGoal linter, then a regex check for terminal simps may already take care of almost all of them and be even simpler to implement.

[Mrigank Pawagi]

Interesting insights. Thanks!

[Igor Khavkine]

Sorry to bump an older thread, but it seems relevant. I would like to know what is the current style guideline about "squeezing terminal simps"? The public facing documentation says that calls to simp or simp? made during development should be replaced by simp only [...] tactics. Should that documentation be updated?

This came recently in the discussion at #25564.

[Edward van de Meent]

Igor Khavkine said:

The public facing documentation says that calls to simp or simp? made during development should be replaced by simp only [...] tactics.

The documentation says that about "using simp in the middle of a proof", i.e. non-terminal simps.

[Edward van de Meent]

i believe the current consensus is that terminal simps must not be squeezed?

[Edward van de Meent]

indeed, the style guide says not to (unless really necessary)

[Edward van de Meent]

@Yaël Dillies said (at the github discussion):

Ah! Can you raise on Zulip that https://leanprover-community.github.io/contribute/style.html#squeezing-simp-calls is misplaced?

I don't think that this is misplaced? it's in style, as it is a style guideline... Where would you place it?

[Yaël Dillies]

where we encourage the squeezing of simp calls

[Edward van de Meent]

maybe we should move the encouraging of squeezing simp calls, then

[Yaël Dillies]

Sure, that is another option. It's just that right now they are in different places. No wonder so many newcomers squeeze their terminal simps :-)

[Michael Rothgang]

Add to this that mathlib also has many squeezed terminal simps, from before this policy was added.

[Michael Rothgang]

Re: where to place this? I would think it's good to

• augment the page about simp, with at least a note that terminal simps should not be squeezed (and a brief reference to the style guide)
• mention non-terminal simps in the style guide: currently, they are only mentioned on that page (which is definitely not ideal)

[Johan Commelin]

Sounds good. And then similar changes could be made to #glossary

[Johan Commelin]

https://leanprover-community.github.io/glossary.html