superfluous constraints

Stream: lean4

[MangoIV]

Hi, is there a way of letting lean4 figure out, which constraints are not needed? I would like to have something similar to simp? where it tells me which constraints I can delete without going all the way from deleting the constraints and then reintroducing them as the compiler tells me what it cannot deduce.

[James Gallicchio]

I'm not sure I entirely understand the question -- are you trying to minimize typeclass arguments to a def?

[Henrik Böving]

I think so. I also believe this should be doable with an "unused variable" style approach in the resulting Expr of the definition but it doesn't exist right now

[Sebastian Ullrich]

It's a reasonable and perhaps even straightforward extension of the unused variables linter that just hasn't been envisioned originally

[Mario Carneiro]

That does exist, that's the mathlib linter

[Mario Carneiro]

(actually std linter now)

[Eric Rodriguez]

There's also @Alex J. Best's generalisation linter, which I'm not sure if he has plans to port to Lean4.

[Eric Rodriguez]

It led to some very cool results in Lean3, though

[Mario Carneiro]

import Std.Tactic.Lint

def foo (α : Type) [BEq α] := α = α

#lint only unusedArguments

-- Found 1 error in 1 declarations (plus 0 automatically generated ones) in the current file with 1 linters

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
#check foo /- argument 2 inst✝ : BEq α -/

[Sebastian Ullrich]

Is there any reason for this to be a global linter?

[Mario Carneiro]

yes, it works on Exprs instead of syntax

[Mario Carneiro]

so it's impossible to implement as a lean linter unless you get a builtin and not super expensive version of whatsnew in

[Sebastian Ullrich]

Oh, what you mean is that it is also supposed to work on generated definitions

[Mario Carneiro]

The most logical implementation would be to have an append-only list of declarations in the current file in declaration order in the Environment, we already need this for other reasons

[Mario Carneiro]

Even if it only works on the current definition, it's still annoying to code as a lean linter because you have to parse (and to some extent re-elaborate) the syntax to find out what the current declaration is

[Mario Carneiro]

and I'm really concerned about the performance cost of lean linters if we get any more of them, because they are not optional as currently designed

[Henrik Böving]

Could we maybe design this like rust does? Where you can run some sort of linter with the build tool like clippy? I would imagine lake should be hackable enough to allow us to inject stuff into the elaboration of files right?

[Mac Malone]

Henrik Böving said:

I would imagine lake should be hackable enough to allow us to inject stuff into the elaboration of files right?

Unfortunately, no. That is one thing Lake cannot do, because lean does provide any way (I know of) to do so.

[Alex J. Best]

Eric Rodriguez said:

There's also Alex J. Best's generalisation linter, which I'm not sure if he has plans to port to Lean4.

I plan to port and improve it at some point yes!