Lean 4 adds variable to args for no reason

Stream: mathlib4

[Yury G. Kudryashov]

In !4#4773, if you remove section FTC1 and end FTC1, then Lean adds lb/lb'/FTCFilter _ _ _ to the arguments of sub_le_integral_of_has_deriv_right_of_le. I don't know why and I don't know how to minimize this example.

[Yury G. Kudryashov]

I added a section as a workaround (also, we should split this file into FTC1 and FTC2)

[Mario Carneiro]

It's probably a cases or induction or rw at * or similar that modified one of the variables in the context, making it "used" and hence pulled in to the definition

[Kevin Buzzard]

This seems to me to be a genuine regression :-(

[Eric Wieser]

In induction I assume you mean; obviously this a regression in the statement of FTC!

[Patrick Massot]

There is a simple rule about variable in Lean 4: you should never state a theorem in a context where there are variable you don't want to be included. variable simply doesn't work in Lean 4 the way it worked in Lean 3. It would have been clearer to simply use a different keyword.

[Ruben Van de Velde]

Is this something the ambiguous translation thing could have caught, if it wasn't full of false positives?

[Yury G. Kudryashov]

I caught it first time I tried to apply this theorem.

[Yury G. Kudryashov]

But ambiguous translation should've caught it too.

[Eric Wieser]

I think Kevin's claim is that the new behavior, confusing or otherwise, is just not as useful as the old

[Kevin Buzzard]

Seeing a gazillion irrelevant variables in the infoview is not helpful :-( I know Mario has argued that variables defined 200 lines earlier lead to code which he can't read as easily, but what we have now is not really ideal.

[Eric Wieser]

I think there's a lot of value to being able to say at the top of the file "S is a semiring, R is a ring, K is a field"

[Eric Wieser]

If you use a sectioning approach instead, then all your lemmas move around when they're generalized (replacing K with R or R with S) and our diffs become bigger

[Eric Wieser]

Right now the behavior is "it works just fine (other than an ugly goal view) unless you're planning to use induction, and then you have to write generalizing to keep your foot attached"

[Damiano Testa]

I would also like to point out that "it works just fine" may not be entirely true when Lean guesses incorrectly which typeclasses to use, from the available pool. This lead to my misporting of RatFunc that resulted in Yuri's issues with Laurent.

[Eric Wieser]

Well that never worked well in Lean 3 either (unless you juggle with include/omit, which was a pain there too)

[Eric Wieser]

I didn't suggest above saying at the top of the file "R is a semiring, ring, or field, depending on how I use include"!

[Damiano Testa]

Sure, that file had other issues, but I still preferred when the available assumptions were, by default, the ones that made the statement typecheck, plus some correction for edge cases where you may want to revise this.

[Reid Barton]

Maybe what we want is something like "variable tells autoImplicit what the types are"

[Scott Morrison]

fwiw, I've never liked the "global variables at the top of the file" approach, and find it completely unreadable, and think larger diffs when refactoring is a small price to pay.

[Yury G. Kudryashov]

What's wrong with "in this file, E, F, and G are normed spaces over a nontrivially normed field K"?

[Scott Morrison]

That's fine, I guess. I don't much like the "M is a module over a ring R and V is a module over a field K" approach, where the only way for me to work out the hypotheses of a lemma are to be like a physicist and know from the names of things what they are. :-)

[Scott Morrison]

Hover over declaration names has made this much easier, of course.

[Scott Morrison]

That is, I prefer sections for changing hypothesis strengths rather than having to carry around a lookup table from variable names to typeclasses