RFC: Make simp only warn on unused list elements

[andrewmw94]

Proposal

I'd like to make it so simp only [A B] warns if B is not used.

How does this feature improve the user experience?
When updating code, we sometimes 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.

Which Lean users and projects benefit most from this feature/change?
This feature was requested by the Cedar team, but in the Zulip discussion other Lean users said they would appreciate it.

Will this change streamline code maintenance or simplify its structure?
I'm not familiar enough with the Lean code base to offer an opinion.

Community Feedback

Proposed in this Zulip thread.

Summary
People seemed receptive to the idea, with the caveat that it will be difficult to deal with something like split <;> simp [A, B] where B may only be needed in one branch.

Currently, Lean will flag an unused import even though the import can't be removed because it is listed but not used (i.e., it imports B in the example). So adding this linter would make removing unused imports easier.

People also agree we need some way to disable the linter (so opt-in or opt-out). This means the linter will have to go in core so leanOptions can globally enable / disable the linter.

Impact

I believe the impact would be minor. It's an added convenience, but one that several people have said they would appreciate.

[eric-wieser]

This means the linter will have to go in core so leanOptions can globally enable / disable the linter.

Or address #3403 first

[Kha]

RFC accepted; likely this should apply to explicit arguments of simp as well