linter.unusedVariables bug?

Stream: lean4

[Alex Kontorovich]

Sebastien Gouezel said:

This looks like a linter bug, right?

Is the behavior below a bug in the unusedVariables linter? (There are lots of mathematical situations in which you would want the hx below not to flag linter)

variable {X : Type}

def Baz (x : X) : Prop := sorry

def Bop (x : X) : Prop := sorry

example (a : X) (ha : Baz a) (h : ∀ (x : X) (hx : Baz x), Bop x) : Bop a :=  h a ha -- unused variable `hx` [linter.unusedVariables]

I can open an issue if indeed this is a bug. (It can be overcome by replacing (hx : with (_ :.) Thanks!

[Alex J. Best]

You can write this as Baz x implies Bop x, or use _hx, I think reasonable people disagree on whether this is a reasonable thing for the linter to ask of you

[Patrick Massot]

Why don't you write

example (a : X) (ha : Baz a) (h : ∀ (x : X), Baz x → Bop x) : Bop a :=  h a ha

[Alex Kontorovich]

Patrick Massot said:

Why don't you write

example (a : X) (ha : Baz a) (h : ∀ (x : X), Baz x → Bop x) : Bop a :=  h a ha

This issue arose in #7506, please look at Mathlib/MeasureTheory/Group/FundamentalDomain line 875. We want something to be true for all measurable sets U. If we replace (_ : MeasurableSet U) with (meas_U : MeasurableSet U), then linter complains.

[Alex Kontorovich]

I think I see; so even in this setting, you would propose that we replace lines 875-876:

(U : Set (Quotient α_mod_G)) (_ : MeasurableSet U),
  μ U = volume (π ⁻¹' U ∩ t)

with:

(U : Set (Quotient α_mod_G)), MeasurableSet U → μ U = volume (π ⁻¹' U ∩ t)

I suppose that's fine?...

[Patrick Massot]

I still agree with you that the linter is weird. But you wouldn't write this "for all U, for all U is measurable, ..." on paper. The way we usually solve this in Lean is by using Set. Then you can use bounded quantifiers.

[Alex Kontorovich]

Thanks. But sorry I don't follow the suggestion to use Set? Can you elaborate please?

[Patrick Massot]

There is no new suggestion here. I'm only saying that the reason you don't encounter this situation more often is that it is usually set up with Set X instead of a predicate on X. Of course Set X is defined to be predicates on X but with different instances and psychological impact.