linter for `rfl` lemmas?

Stream: general

[Scott Morrison]

Would anyone be interested in writing a linter that checks that any @[simp] lemma which can be proved by rfl is proved by rfl?

(It is annoying when this isn't the case as simp then mysteriously refuses to go into dsimp mode.)

[Scott Morrison]

I think this shouldn't be too hard, and belongs in Std.Tactic.Lint.Simp

[Mario Carneiro]

note that this could be pretty expensive, as trying to prove random things by rfl that aren't known to be defeq could end up doing lots of work

[Scott Morrison]

Maybe the linter would actually be more useful with a cheap rfl.

[Eric Wieser]

Is trying to prove it by dsimp sufficient? No, nevermind, that only works if its already proven by rfl

[Yaël Dillies]

We have the option of not running that linter all the time. In fact, there's a bunch of "expensive" linters (mostly @Alex J. Best's) that we don't want to run all the time, but also don't want to never run. What about we set up a weekly cron job?

[Johan Commelin]

I think that makes sense. We could get into the habit of bumping mathlib to a new Lean rc, and after that doing a "linting-bump".