unused variable warning

Stream: lean4

[Kevin Buzzard]

Doing basic logic with my class and in a lot of my proofs there are unused variables, e.g. I'm just getting them to prove dumb stuff like P -> True and they do intro hP; triv or whatever and then get a warning that they didn't use hP. The second question is P -> Q -> P (an axiom of predicate logic) and intro hP; intro hQ; exact hP gives an unused variable warning, but this is week 1 of the course and I'm not sure that I want to trouble them with this at this point. Can I turn these warnings off for e.g. an entire file?

[Jireh Loreaux]

set_option linter.unusedVariables false

[Jireh Loreaux]

the set_option version is the way to turn off "core" linters whereas the @[nolint ...] is the way to turn off "Mathlib" linters.

[Kevin Buzzard]

Is there an easy way to tell whether a linter is a core one or a mathlib one? I wasn't even sure if this was the right stream for this question because I didn't really even know where to start looking.

[Jireh Loreaux]

(I think) the easy way is that the core ones trigger immediately, but the Mathlib ones you need to trigger manually with #lint.

[Kim Morrison]

That's not quite true. There are two separate linting frameworks, and any project can add linters to either framework. One is defined in Lean, the other in Std.

[Jireh Loreaux]

So what I said is true if you replace Mathlib with Std, right?

[Kim Morrison]

Yes.

[Mario Carneiro]

By the way, I just reimplemented the unused variables linter in lean4#3186 and I was surprised to discover that a major part of the algorithm, and by far the slowest, is spent trawling all metavariable assignments in all intermediate elaborator states looking for fvars exactly because it is needed to support cases like this:

theorem implicitlyUsedVariable : P ∧ Q → Q := by
  intro HPQ
  have HQ : Q := by exact And.right HPQ
  assumption -- HQ should count as used

This surprises me because this is exactly the case which, like @Kevin Buzzard , I had grown to think was not handled by the algorithm! So I guess whatever it is doing is not sufficient...

[Johan Commelin]

There are two kinds of "unused variable" warnings:

• a variable that got a pretty name, but that pretty name is never mentioned again in the user-written proof.
• a variable that is genuinely unused, it doesn't appear in the proof term (i.e., doesn't show up in the pp.all version of the proof)

Both are useful. But my impression is that they currently aren't very distinguished, and both carry the same name.

[Johan Commelin]

For example, the "unused pretty name" linter could (should?) complain in Mario's HQ example above.
But the "genuinely unused" linter certainly shouldn't complain.

[Mario Carneiro]

the funny part is that one of the reasons we have to go to great lengths to justify that HQ is used is because many tactics will just skip it entirely, e.g. if assumption here was to close the goal using And.right HPQ instead of using HQ directly. Would HQ be "genuinely unused" in that case?

[Mario Carneiro]

In such a case, if you look at the proof term you won't find HQ anywhere

[Mario Carneiro]

(this doesn't actually happen in this particular case, but I think it would if we used haveI instead of have)

[Johan Commelin]

I also thought of haveI and I agree it's a tricky one. So I'm glad that you went to great lengths (-;

[Kyle Miller]

Is there an interface where a tactic can say "I used this"? I guess the algorithm is trawling through the infotrees since these are more-or-less already that interface?

For the example of tactics that indirectly use a variable, maybe they could be sure to register that variable in the infotree.

[Mario Carneiro]

That would be helpful. We have to look through the entire metavar context, every metavariable that has been created before or during the operation of the tactic, exactly because we have no clear idea of what the tactic did. I tried just looking at the assignments of the goals in the after state, but the after state is not necessarily "after" enough, it may still be partially unassigned and there is no "final mvar context" we can look at because elaboration can contain unrelated mvar contexts (e.g. evaluating the (config := ...) argument of a simp call)

[Mario Carneiro]

Because this procedure is such a blunt instrument it also clearly has false negatives

[Kyle Miller]

Yeah, a tactic could even elaborate a term, checkpoint the metavar context, and then repeatedly do further processing of that term from that checkpointed context to solve for multiple goals... It was kind of a shock to realize that not only is that there no final metavariable context, but there can't be one (short of doing a very large transformation and uniquifying metavariables between multiple contexts).

[Martin Ceresa]

Hello!
Has been some progress here? I have a concrete example. I am using variables to show termination but not during computation.
In concrete

def fun ... (a : \alpha) ... := match HDest : a with
                                                      ....
termination_by sizeOf  a.Field  -- type \alpha is a record.
decreasing_by all_goals { .... ; rw [ HDest ] ; ... }

I don't want to turn off the linter, but to explicitily say I am using this here.
Maybe there is a better way to do this, splitting the record so no need to say how they decrease, but type \alpha is a concept I do not think I should break here.

[Joachim Breitner]

No progress yet. https://github.com/leanprover/lean4/issues/2920 is the issue for that particular problem

[Martin Ceresa]

Cool, using one of the suggested solutions works like a charm.
I did not know that naming it '_h' does not triggers the linter.
Just for the record, modifying the previos code fragment as follows:

def fun ... (a : \alpha) .... := match _HDest : a with ...

Works :muscle: