which parameters to make implicit

Stream: new members

[Patrick Thomas]

Is there a general rule or lint check for which parameters to make implicit? Is it just if the parameter appears in a later parameter?

[Kevin Buzzard]

Yes that's the general rule, but there are other subtleties, for example things might depend on whether you're establishing an implication or an iff, or whether it's a definition or a lemma. In my experience it's pretty easy to work out what you should be doing once you start using your definition, if you feel like lean should be working some stuff out which you keep having to feed it then maybe you should have used {}, and conversely if you keep having to use @ then maybe you shouldn't have.

[Patrick Thomas]

If you use the general rule, will that be enough to ensure that you never need to use @?

[Violeta Hernández]

There's further subtleties in some special cases, when you have an argument appear in a later parameter, but in practice, when you prove the later parameter, the previous one can't be easily inferred

[Violeta Hernández]

Mostly happens with sets and functions, since something like x ∈ s could be literally any proposition on x (which doesn't allow you to infer s unless you already know exactly what you want to prove)

[Patrick Thomas]

Hmm. I think I maybe see. I guess, is there a decidable way to tell which parameters are safe to define as implicit, in the sense of never needing to use @?

[Violeta Hernández]

I'd say the general heuristic is the one you mention, but if you find yourself having to use @ more than once or twice, you should make whichever arguments are being problematic explicit

[Violeta Hernández]

Really, it's just a matter of what works

[Patrick Thomas]

Ok, thank you.
PS: I have seen mentions of a lint checker. Is there one? If so, where should I look for information on it?

[Violeta Hernández]

I think you can lint a file by adding #lint at the end

[Patrick Thomas]

I see, it is a command. That led me to https://leanprover-community.github.io/mathlib_docs/commands.html#linting%20commands. Thank you!

[Alex J. Best]

The linter currently doesn't check which variables are implicit/explicit FYI, if it did I'm sure there would be a lot of linter failures!

[Patrick Thomas]

Is it theoretically possible to create a program that takes a definition and reports which parameters can 'safely' be set implicit?

[Damiano Testa]

If I understood correctly, it might be enough to restate the lemma, proving it with the original lemma itself, but using as many underscores as possible. This may give some idea of which arguments can be inferred by Lean.

[Patrick Thomas]

That makes sense. I was just curious though if there was a decidable way to determine it just from the definition.

[Eric Wieser]

I think @Arthur Paulino made an attempt at a linter to enforce a rule here?

[Arthur Paulino]

Kinda. There was an issue about a linter to flag explicit variables that were used on both sides of equalities and iffs. Turned out it flagged way too many lemmas and there were other reasons not to enforce it. But the linter made it into master as an optional linter

[Kyle Miller]

Something to look forward to in Lean 4 is the ability to set individual implicit variables. For example, we should be able to write finset.univ (α := fin n) rather than needing to write (finset.univ : finset (fin n)). I expect we'll become a lot more aggressive with our use of implicit variables in lemmas.