unused argument linter

Stream: mathlib4

[Sébastien Gouëzel]

What is the status of the unused argument linter in mathlib? I just reviewed a PR in which there was a plain unused argument (I mean, an obvious one, like (hJ_card : #J ≤ a ^ n) in the lemma statement, that did not show up at all in the proof), and no linter complaint.

[Kenny Lau]

are you sure it isn't accidentally used by grind or something?

[Floris van Doorn]

They should be enabled (They = both the style and the environment linter). I think that Kenny is right, and maybe rw at *, simp [*] or grind used it to simplify something (or simplified something in the hypothesis), even though it didn't really get used.

[Aaron Liu]

or maybe it got generalized in an induction call, for example

[Sébastien Gouëzel]

You're probably right that it must be used implicitly somewhere. I can't see where, though (no grind, no induction, no *). You can have a look at https://github.com/DavidLedvinka/mathlib4/blob/6633b19fc80192dc25c645c92ba624596de16b60/Mathlib/Topology/EMetricSpace/PairReduction.lean#L356

[Aaron Liu]

definitely probably the wlog

[Aaron Liu]

try obtain rfl | hJ := J.eq_empty_or_nonempty instead

[Sébastien Gouëzel]

Nope. Using

  rcases Finset.eq_empty_or_nonempty J with rfl | hJ

the linter doesn't complain.

[Floris van Doorn]

The rfl in the pattern rfl | hJ substitutes away #J everywhere, including in hypothesis hJ_card, so it is "used".

[Floris van Doorn]

It was the wlog; replacing the first two lines with the following activates the linter

  obtain hJ | hJ := J.eq_empty_or_nonempty
  · simp [hJ]

[Floris van Doorn]

It would be nice to improve the linter and catch these cases.
Maybe it's possible to recognize that the hypothesis hJ_card before executing obtain rfl | hJ and the hypothesis hJ_card after the tactic are "the same" hypothesis, and since the latter is never used, the former is also never used.
This sounds hard, but if we can do this, we might be able to do the same for rw at hJ_card, induction ... generalizing hJ_card etc.