Unused variables linter and contrapose!

Stream: mathlib4

[Michael Stoll]

Consider the following.

import Mathlib.Data.Nat.Defs
import Mathlib.Tactic.Contrapose

example {m n : ℕ} (h : 1 ≤ n) (h' : m * n < m) : False := by
  contrapose! h'
  exact Nat.le_mul_of_pos_right m h

The "unused variables" linter complains about h' in the contrapose! h' line, presumably because the new h' generated by the tactic (which just states ¬False) is not used in the proof. However, it is necessary to tell contrapose! which hypothesis it should use. It would be nice if the linter could be silenced without having to use set_option linter.unusedVariables false in. I guess one way would be to allow contrapose to accept two arguments, where the second one is used to name the new hypothesis (and defaults to the first one). Then one could write contrapose! h' _, and it should be OK.

[Ruben Van de Velde]

You mean

  contrapose! h' with _h

?

[Michael Stoll]

Should have looked at the docs first ...

[Michael Stoll]

(This came up when updating Mathlib in a fairly old project (on lean 4.6); the linter was apparently not active at the time...)

[Ruben Van de Velde]

Doesn't seem to work with just _; might be possible to add for someone who's motivated

[Michael Rothgang]

The same issue occurred in the carleson project, with recent Lean: https://github.com/fpvandoorn/carleson/pull/127 by @Floris van Doorn van Doorn disables the unusedVariables linter in one file, for this reason.

[Sebastian Ullrich]

The linter will likely be limited in lean#5338 in a way that will not complain about such tactic uses anymore (by default)