Ergonomic improvements around simp

Stream: general

[Andrew Wells]

I have a feature I'd like to see added and I'm interested in contributing it to learn the contribution process.

The feature:
I'd like to make it so simp only [A B] warns if B is not used (for now only in proofs that aren't split to avoid difficulties where B is used in some branches but not in all).

Benefits:
When updating our code, we see broken proofs that report an error at some line after simp only [A B] even though the root cause of the issue is that B is no longer being applied. Warning when this happens will make fixing proofs easier.

Drawbacks:
The main concern I see is that this will spam warnings in existing code bases. If this will be a problem, I could implement this feature under a new name (maybe simp wonly), or we could make it opt-in (or opt-out), or?

Do people think this would be generally useful? Are there other concerns I've missed? Does someone have pointers on where to get started for the actual code change?

Thanks in advance!

[Shreyas Srinivas]

The way is use simp is to normally simp? or simp? [extra defs/lemmas...] and click on the suggested tooltip

[Shreyas Srinivas]

Usually the resulting simp only only contains the lemmas that are needed.

[Shreyas Srinivas]

simp's ability to find simp lemmas automatically is, to my mind, a huge benefit that I would never forgo, so I don't see myself starting with a simp only [def list] and building it up.

[Kevin Buzzard]

Isn't the issue that this is a previously-squeezed simp which is no longer working after a mathlib bump?

[Eric Wieser]

I thought it already had the behavior being requested here?

[Shreyas Srinivas]

I think in principle you have a simp only [<arbitrary lemma/def list>] which isn't automatically minimised.

[Kim Morrison]

An implementation difficulty would be that you would need to support things like split <;> simp [A, B], where perhaps B is only used in one of the two branches. People would find it pretty annoying if that were linted.

[Kim Morrison]

As for implementation, see Lean.Meta.Simp.Stats where the actual theorems used in a simp call are recorded.

[Kim Morrison]

Personally I think such a linter would be good. When cleaning up old code I do often find simp only statements containing (now) unnecessary lemmas, and it is extra step while cleaning to deal with these.

[Ruben Van de Velde]

This can also cause issues with minimizing imports: we will flag the import as unused even if removing it will fail because we mention a lemma in a simp call that doesn't use it

[Kim Morrison]

Andrew Wells said:

Drawbacks:
The main concern I see is that this will spam warnings in existing code bases. If this will be a problem, I could implement this feature under a new name (maybe simp wonly), or we could make it opt-in (or opt-out), or?

Ideally this would be implemented a linter, and so set_option linter.unused_simp_theorems false could disable it (and indeed downstream projects could globally disable it). If we can get to the point of no false positive, I think this would be reasonable to turn on globally.

[Eric Wieser]

It's only possible to globally disable it if this linter goes in core, right? leanOptions in the lakefile doesn't work for anything else.

[Andrew Wells]

I opened an issue (https://github.com/leanprover/lean4/issues/4483) and summarized the conversation. Let me know if I missed anything.

@Ruben Van de Velde To make sure I understand correctly: You're saying Lean will currently flag an import as unused even if removing it will fail, and this is another argument for adding the linter I proposed. That's what I put in the summary, so let me know if I need to change it.