recyclable variables

Stream: mathlib4

[Damiano Testa]

Throughout mathlib, there are quite a few instances of

variable {m n : Nat}

lemma X {m n : Nat} ...

where the available m n in scope are simply overruled.

Should this be discouraged?

[Damiano Testa]

I am running an experiment (#14675) where a linter warns about the possibility of recycling a variable in scope. This happens thousands of times in mathlib (EDIT: 2650 times spread over 630 files).

I realize that sometimes, this is done on purpose to change the order of the variables in the signature of the statement, but, upon looking at a few samples, this looks like the vast minority of the cases.

[Kyle Miller]

I personally think it's the sort of thing that someone can decide to go through and choose to clean up, but I wouldn't want people to be forced to always avoid shadowing variables.

It would be neat having a code action that inserts all the used variables back as arguments. That would help with moving declarations between modules.

[Damiano Testa]

Fair enough. In fact, I probably have a preference for erring on the explicit side for variables!

[Eric Wieser]

Sometimes shadowing is necessary if you want to change the argument order

[Damiano Testa]

I agree, but I spot-checked a few of the declarations that were flagged and the overwhelming majority did not change the argument order.

[Thomas Murrills]

Kyle Miller said:

It would be neat having a code action that inserts all the used variables back as arguments.

And the reverse! :) (I.e., removing all arguments that shadow variables)

[Yury G. Kudryashov]

Please don't remove explicit variables from theorems.

[Yury G. Kudryashov]

As for the implicit variables, using variable LGTM.

[Kim Morrison]

Ageing with the above, I would not want any policy or linter that pushes us to use more variable.

If anything I would like us to get rid of "global" variables, e.g. when people set up variables for both a monoid and a ring at the top of a file, and then you need to carefully watch the name of the type in order to know which setting you're in. I would prefer if we could completely avoid this idiom and use sections instead. Unclear how one could lint, however.

[Kim Morrison]

(this issue is way better today than it used to be, already)

[Damiano Testa]

Kim, if you can be a little more specific with what kind of variable confusion you would like to avoid, I can try to think about how to improve the situation.

[Damiano Testa]

In fact, even though the linter in this thread flags unnecessary uses of variables, my instinct is also to move away from Lean inserting variables in a seemingly magical way. So I am happy to try something else!

[Yury G. Kudryashov]

I guess, something like variable {M N : Type*} [Monoid M] [CommMonoid N] at the top of the file.

[Kim Morrison]

Exactly that!

[Kevin Buzzard]

Yeah this makes code really hard to read on eg GitHub.

[Jireh Loreaux]

Long sections (several hundred lines) also make it challenging, so our push to keep file size down and disentangle the import hierarchy helps a lot.

[Damiano Testa]

With the idea of making a "lintable rule", how about the linter complains if one available typeclass is an instance of another available typeclass?

This should make uses of "incremental" typeclass assumption in variables neatly separated.

[Damiano Testa]

So, an alternative way of saying this, in scope there can only be an antichain of instances. If you want to violate this, then you should silence the linter.

[Daniel Weber]

Perhaps exclude Prop typeclasses? I believe it's fine for those

[Kim Morrison]

This night also really help all the beginners who write variable [Mul X] [Field X] and don't get any automatic feedback that this is broken. In fact this special case (i.e. the same type argument!) could be a linter even if the full one is problematic for some reason.

[Damiano Testa]

The Mul Field linter I was planning to add to the "beginners" linter that also warns about Nat.sub, Nat.div and friends.

[Daniel Weber]

I might've misunderstood, do you mean to lint against things like [CommRing X] [Field Y]?

[Damiano Testa]

No, against CommRing X and Field X -- note the repetition of X.

[Kevin Buzzard]

The issue with variable {M N : Type*} [Monoid M] [CommMonoid N] 100 lines into a 2000-line-long file (this is something mentioned above which you might be referrring to) is that it says "at this point we establish the for-this-file-only convention that all monoids called M are not commutative, and all monoids called N are commutative, and we expect the user to spot this and understand that this is what's going on throughout the file". A better style is sections called things like commutative with [CommMonoid M] valid throughout that section only.

[Damiano Testa]

So, essentially, for each typeclass assumption you make sure that #synth <that typeclass> in the context of all the remaining ones fails, otherwise the linter tells you that there is a typeclass dependence in your variables.

[Yaël Dillies]

Damiano, that's a good start but it's not enough: [CommMonoid R] [Ring R] is also bad

[Daniel Weber]

Kevin Buzzard said:

The issue with variable {M N : Type*} [Monoid M] [CommMonoid N] 100 lines into a 2000-line-long file (this is something mentioned above which you might be referrring to) is that it says "at this point we establish the for-this-file-only convention that all monoids called M are not commutative, and all monoids called N are commutative, and we expect the user to spot this and understand that this is what's going on throughout the file". A better style is sections called things like commutative with [CommMonoid M] valid throughout that section only.

Perhaps the actual problem is variable being in effect for too many lines? After all, this problem persists even if it's [Foo M] [Bar N], where Foo and Bar are completely unrelated, only it's easier to figure out from the context what's going on.

[Damiano Testa]

Yaël Dillies said:

Damiano, that's a good start but it's not enough: [CommMonoid R] [Ring R] is also bad

I agree, but let me try to get a linter working that flags all uses that are "clearly" bad and then we can discuss other, more subtle abuses. Does that seem right?

[Damiano Testa]

I'm going to write a "permissive" linter that just does what I said above, also to see if there are some "legitimate" uses of a dependency among typeclass assumptions. Given that mathlib is so large, there is usually some edge case (typically by you, Yaël), where the linter is not doing what it should! :smile:

[Daniel Weber]

Perhaps if both are named and each time it's explicitly written which one to use

[Damiano Testa]

#14731 in its very first run!

[Yury G. Kudryashov]

Daniel Weber said:

Kevin Buzzard said:

The issue with variable {M N : Type*} [Monoid M] [CommMonoid N] 100 lines into a 2000-line-long file (this is something mentioned above which you might be referrring to) is that it says "at this point we establish the for-this-file-only convention that all monoids called M are not commutative, and all monoids called N are commutative, and we expect the user to spot this and understand that this is what's going on throughout the file". A better style is sections called things like commutative with [CommMonoid M] valid throughout that section only.

Perhaps the actual problem is variable being in effect for too many lines? After all, this problem persists even if it's [Foo M] [Bar N], where Foo and Bar are completely unrelated, only it's easier to figure out from the context what's going on.

OTOH, variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} at the top of a measure theory file is OK, even if the file is long.

[Patrick Massot]

Damiano Testa said:

So, essentially, for each typeclass assumption you make sure that #synth <that typeclass> in the context of all the remaining ones fails, otherwise the linter tells you that there is a typeclass dependence in your variables.

When would that run? I am a bit worried this would be a rather slow linter.

[Damiano Testa]

For the moment, I'm just trying to get something that reports something useful.

It is currently running on each variable command, but I think that some of the warnings that it is reporting are timeouts. :upside_down:

[Yaël Dillies]

Surely it should be a syntax linter, so that it is only run when you open a file in vscode?

[Damiano Testa]

It is a syntax linter, but syntax linters also run on CI.

[Eric Wieser]

75% of all syntax linter time is spent in the unusedVariables linter

[Yaël Dillies]

Damiano Testa said:

It is a syntax linter, but syntax linters also run on CI.

That sounds like maybe they shouldn't?

[Damiano Testa]

If syntax linters did not run on CI, then whatever they are warning against would get merged, though.
(Or likely I misunderstood what you meant! :smile: )

[Damiano Testa]

The first run, uncovered a bug when dealing with binder-update.

The current round found in Mathlib/Order/Minimal.lean:

variable [PartialOrder α]
...
variable [LE α] [LE β] {s : Set α} {t : Set β}
/- Minimal.lean:357:9
Typeclass '[LE α]' is implied by [[PartialOrder α], [LE β], [LE β]]
note: this linter can be disabled with `set_option linter.dependentTypeclass false`
-/

[Yaël Dillies]

Whoops :flushed:

[Damiano Testa]

Spot-checking a few files, the linter seems to flag actual issues. However, resolving these issues is sometimes tricky. If the file looks like

variable [Mul X]
...
variable [Group X]

lemma Y

when the linter gets to Group Y it tells you that now Mul X is superfluous. However, simply sectioning off Mul X, it is not clear whether lemma Y might work with just Mul X.

Of course, this is exactly one of the traps that the linter is supposed to avoid, but now it requires quite a bit of thinking about what to do!

[Johan Commelin]

Well, I'm really glad that you started digging into this. It unearths a whole new category of technical debt.

[Johan Commelin]

Can you generate a list of filenames + line numbers that indicate where we should look for trouble?

[Kevin Buzzard]

In fact is it even clear what happens if you state a lemma which only mentions * at this point? Do you pick up a random one or is it deterministic? It's likely that the statement will not use any group properties but the proof will so presumably the statement must get the group one or else the proof wouldn't work

[Damiano Testa]

Johan Commelin said:

Can you generate a list of filenames + line numbers that indicate where we should look for trouble?

Does the output of CI work? The list of files is

- Mathlib.Order.Minimal
- Mathlib.RingTheory.OreLocalization.Basic
- Mathlib.Data.Finset.Update
- Mathlib.CategoryTheory.Monoidal.Category
- Mathlib.CategoryTheory.FinCategory.AsType
- Mathlib.Data.Fintype.Sort
- Mathlib.Computability.TuringMachine
- Mathlib.Data.MLList.BestFirst
- Mathlib.Order.Birkhoff
- Mathlib.Combinatorics.SimpleGraph.Finite
- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
- Mathlib.GroupTheory.Perm.Sign
- Mathlib.CategoryTheory.Limits.Preserves.Limits
- Mathlib.Combinatorics.Additive.AP.Three.Defs
- Mathlib.RingTheory.OreLocalization.Ring
- Mathlib.Algebra.Module.Submodule.Map
- Mathlib.Topology.Order
- Mathlib.LinearAlgebra.Pi
- Mathlib.Algebra.Field.Subfield
- Mathlib.GroupTheory.QuotientGroup
- Mathlib.Topology.Bases
- Mathlib.Algebra.Algebra.Opposite
- Mathlib.Combinatorics.SimpleGraph.DegreeSum
- Mathlib.GroupTheory.CommutingProbability
- Mathlib.Algebra.MonoidAlgebra.Degree
- Mathlib.CategoryTheory.GlueData
- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
- Mathlib.Combinatorics.Optimization.ValuedCSP
- Mathlib.Algebra.DirectSum.Module
- Mathlib.LinearAlgebra.StdBasis
- Mathlib.GroupTheory.SpecificGroups.Alternating
- Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
- Mathlib.CategoryTheory.GradedObject.Single
- Mathlib.RingTheory.HahnSeries.Multiplication
- Mathlib.Analysis.Convex.Basic
- Mathlib.RingTheory.Localization.Module
- Mathlib.Analysis.Calculus.Deriv.Mul
- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
- Mathlib.Analysis.Analytic.Polynomial
- Mathlib.FieldTheory.NormalClosure
- Mathlib.Analysis.NormedSpace.TrivSqZeroExt
- Mathlib.FieldTheory.Finite.GaloisField
- Mathlib.Algebra.Lie.Weights.Cartan
- Mathlib.LinearAlgebra.Matrix.LDL
- Mathlib.Algebra.Module.Zlattice.Basic
- Mathlib.MeasureTheory.Measure.Haar.Quotient
- Mathlib.RingTheory.Ideal.Norm
- Mathlib.RingTheory.DedekindDomain.Different
- Mathlib.Probability.Process.Stopping
- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
- Mathlib.NumberTheory.NumberField.Embeddings
- Mathlib.Analysis.Distribution.SchwartzSpace
- Mathlib.Probability.Kernel.Condexp

(some of these could be false positives, but I have not yet observed one).

[Damiano Testa]

Kevin Buzzard said:

In fact is it even clear what happens if you state a lemma which only mentions * at this point? Do you pick up a random one or is it deterministic? It's likely that the statement will not use any group properties but the proof will so presumably the statement must get the group one or else the proof wouldn't work

I have not investigated this, but the variable behaviour is very "dangerous": after I mis-ported a file due to not realizing what variable actually did, I have been very very worried of variable.

[Damiano Testa]

Here is a "fix" of one file: #14746.

It is a real challenge to know whether or not separating the typeclasses made some lemmas assume too much.

[Johan Commelin]

Damiano Testa said:

Johan Commelin said:

Can you generate a list of filenames + line numbers that indicate where we should look for trouble?

Does the output of CI work?

Thanks for the list of filenames. The CI output is quite intimidating with its thousands of lines.

[Damiano Testa]

The output is long, but if you look at it file-by-file it is not so bad!

[Damiano Testa]

Let me do a "read" of one file!

[Scott Carnahan]

I had a recent PR merged that changed RingTheory.HahnSeries.Multiplication. CI complained about line 85, but I cannot see a problem.

[Damiano Testa]

⚠ [4711/4819] Building Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/lean/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean -R ./././. -o ././.lake/build/lib/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.olean -i ././.lake/build/lib/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.ilean -c ././.lake/build/ir/Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.c --json
warning: ././././Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean:183:22: Typeclass '[IsScalarTower ℝ 𝕜
      G]' is implied by [[NormedAddCommGroup E],
 [NormedSpace ℝ E],
 [NormedAddCommGroup F],
 [NormedSpace ℝ F],
 [NormedAddCommGroup G],
 [NormedSpace ℝ G],
 [NormedAddCommGroup W],
 [NormedSpace ℝ W],
 [MeasurableSpace E],
 [BorelSpace E],
 [FiniteDimensional ℝ E],
 [IsAddHaarMeasure μ],
 [NormedField 𝕜],
 [NormedAlgebra ℝ 𝕜],
 [NormedSpace 𝕜 G],
 [NormedField 𝕜],
 [NormedAlgebra ℝ 𝕜],
 [NormedSpace 𝕜 G]]
note: this linter can be disabled with `set_option linter.dependentTypeclass false`

This is just saying that `IsScalarTower ℝ 𝕜 G] is implied by (a subset of)

 [[NormedAddCommGroup E],
 [NormedSpace ℝ E],
 [NormedAddCommGroup F],
 [NormedSpace ℝ F],
 [NormedAddCommGroup G],
 [NormedSpace ℝ G],
 [NormedAddCommGroup W],
 [NormedSpace ℝ W],
 [MeasurableSpace E],
 [BorelSpace E],
 [FiniteDimensional ℝ E],
 [IsAddHaarMeasure μ],
 [NormedField 𝕜],
 [NormedAlgebra ℝ 𝕜],
 [NormedSpace 𝕜 G],
 [NormedField 𝕜],
 [NormedAlgebra ℝ 𝕜],
 [NormedSpace 𝕜 G]]

[Damiano Testa]

I think that a reasonable way forward is to

• make Lean print the actual instances that are used by inferInstance, so that it removes the other typeclasses that do not play a role in the inference;
• automatically flag lemmas that compile with those "bigger" typeclasses removed, so that you can move to an earlier place in the file the corresponding lemma.

[Damiano Testa]

As for the length of the CI output, each built file produces a line (already ~4k lines!) and each time the linter fires, there is one extra line for you can disable this linter by....

[Damiano Testa]

Scott Carnahan said:

I had a recent PR merged that changed RingTheory.HahnSeries.Multiplication. CI complained about line 85, but I cannot see a problem.

Scott, was this meant for this thread? The linter that is being discussed here is just a prototype.

[Scott Carnahan]

Yes, I meant I looked at the output of CI that you linked, and looked at the current file, but could not see the variable problem that CI mentioned. Perhaps I was reading it wrong.

[Damiano Testa]

If you want to paste the output here, I can try to clarify it.

[Damiano Testa]

Oh, I found it by looking at the file.

[Damiano Testa]

This is what happens:

variable {Γ R V : Type*} [PartialOrder Γ] [Zero V] [SMul R V]

/-- The casting function to the type synonym. -/
def of {Γ : Type*} (R : Type*) {V : Type*} [PartialOrder Γ] [Zero V] [SMul R V] :
    HahnSeries Γ V ≃ HahnModule Γ R V := Equiv.refl _

/-- Recursion principle to reduce a result about the synonym to the original type. -/
@[elab_as_elim]
def rec {motive : HahnModule Γ R V → Sort*} (h : ∀ x : HahnSeries Γ V, motive (of R x)) :
    ∀ x, motive x :=
  fun x => h <| (of R).symm x

@[ext]
theorem ext (x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
  (of R).symm.injective <| HahnSeries.coeff_inj.1 h

variable {V : Type*} [AddCommMonoid V] [SMul R V]

the linter flags [Zero V] on the first line, when it parses [AddCommMonoid V] on the last line of the excerpt above.

[Damiano Testa]

This case is subtle, since I actually think that this is ok, because the V from before is shadowed, but I am not completely sure.

Even if it is ok, I would probably still think that "good" code should section this better. I consider this a "success" of the linter.

[Damiano Testa]

(Btw, this "action at a distance" can be confusing and I am still trying to figure out what would be a good way of reporting it.)

[Damiano Testa]

Kevin Buzzard said:

In fact is it even clear what happens if you state a lemma which only mentions * at this point? Do you pick up a random one or is it deterministic? It's likely that the statement will not use any group properties but the proof will so presumably the statement must get the group one or else the proof wouldn't work

While trying to figure out whether there is a pattern to this, I found this very cryptic failure:

import Mathlib.Algebra.Group.Defs

variable {Z}
variable [Semigroup Z]
variable [Group Z]

example {z : Z} : z * z * z = z * (z * z) :=
  mul_assoc ..
/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  inst✝¹
inferred
  Monoid.toSemigroup
-/

Instead of Lean just picking either one of the typeclasses that work, you get an error. The end result is probably that the user will remove Group, but this is likely after a while of being confused by the error message.

[Scott Carnahan]

I think I understand now. It looks like you are working with a version of the file from before the PR was merged. However, I am quite impressed that the linter was able to pick up that pair.

[Damiano Testa]

I just pushed another attempt at better reporting issues. The linter is now more or less aware of which typeclass assumptions are used in the implication, as well as whether the flag of an issue happens "far away". Here is an example:

import Mathlib.Tactic.Linter.DependentTypeclass
import Mathlib.Algebra.Ring.Defs

variable {Z}

/-  warning here:
Typeclass '[Semigroup Z]' follows from '{Z} [MonoidWithZero Z] ↦ inferInstance'
note: this linter can be disabled with `set_option linter.dependentTypeclass false`
-/
variable [Semigroup Z]  -- underlined in yellow

/- info here:
The assumptions '{Z} [MonoidWithZero Z]' imply the earlier assumption '[Semigroup Z]'
-/
variable [MonoidWithZero Z]  -- underlined in blue

[Damiano Testa]

If instead a single block of variables already has some dependency, then the linter just underlines the "implied" typeclasses and, for each one, it tells you which other ones are used for the implication.

[Damiano Testa]

This is still slightly hacky, since I get precise Expr information about which typeclass assumptions are needed, but I am finding it trick to convert it back to Syntax information that is what the linter has direct access to. But it seems to work.

[Damiano Testa]

What I consider to be the main missing usability feature for this, is flagging which lemmas that appear after a dependency in typeclasses is introduced can be actually proved before the dependency is introduced.

E.g. in

variable {X} [Mul X]
...
variable [Group X]
lemma Y <only involving mul>

flagging Y as needing to move earlier.

[Damiano Testa]

This will likely have to wait a couple of days, though!

[Damiano Testa]

If anyone feels like helping out, please take a look at the output of the linter at #14731.

[Damiano Testa]

The yellow squiggles tell you which typeclass assumption are implied by the blu squiggles. Typically, you first see the yellow squiggles and they become redundant when the blue squiggles become part in scope.

[Damiano Testa]

For instance in Mathlib/RingTheory/Valuation/ValExtension.lean,

• on line 51 there are [LinearOrderedCommMonoidWithZero ΓR] [LinearOrderedCommMonoidWithZero ΓA] with yellow squiggles and
• on line 97-98 there are [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] with blue squiggles.

So, once you reach line 97-98, it is likely that the older variables are no longer desirable and can only cause trouble,

[Michael Rothgang]

This looks like a dangling sentence. Would you like to finish it? (I'm certainly curious how this post ends :-))

[Damiano Testa]

Ah,
... so some work needs to be done.

[Damiano Testa]

However, simply sectioning out the older ones and copying over the new ones may force Lean to use the stronger assumption, when the weaker was actually used.

[Damiano Testa]

This requires care and probably more metaprogram help to make sure that by sectioning off the weaker assumptions you are not actually increasing the hypotheses of later declarations.

[Damiano Testa]

In an ideal world, once the blue squiggle appears, the yellow-squiggled variable should disappear from scope.

[Damiano Testa]

There is some care to be taken in case some later declarations can be moved earlier with the weaker assumptions.

[Damiano Testa]

It is possible that "mathlib builds" is already a good test that instances have not been strengthened.

[Damiano Testa]

Otherwise, these will be picked up by the typeclass generalization tool... :see_no_evil:

[Matthew Ballard]

I left comment on the PR but it would be good to get more exposure to understand the desired user experience.

I am somewhat worried about hammering infer_instance to check for overlaps on each variable.

The examples above make me think we should only care about local instance overlap for a core style linter and perhaps leave deeper checks for CI.