weird speedup in Mathlib.RingTheory.NoetherNormalization

Stream: mathlib4

[Kevin Buzzard]

PR #29207 has a diff which is quite hard to understand, but it's not entirely clear to me that there's a lot going on at the end of the day. However the benchmark bot got very excited about it; in particular, files which are close to the weird JacobiZariski file (nobody understands why it's slow) got magically sped up (one by over 20% and one by over 30%).

I asked @Yaël Dillies if they could guess an explanation, and one suggestion was that it might be to do with universe metavariables in declarations. I don't really know what these are though; Yael suggested that there was a difference between theorem name (R M) ... and variable (R M) in theorem name ... but I could not see any explicit changes of this form in the PR diff. They also suggested that universe metavariables in mathlib declarations were to be avoided in general and asked whether we could lint for them. This is all beyond my understanding.

If I weren't so busy on FLT I would love to devote some time into trying to figure out why this corner of mathlib is so weird and slow; there are messages in this story for our community and we've not managed to figure them out yet. My joke PR #21165 making a JacobiZariski universe-monomorphic sped it up by 60% so at least part of the reason for slowness around here is to do with universes, but I've always been under the vague impression that there are multiple things going on. Is this another one? Can anyone see what's happening and why #29207 was such a win? Initially I was skeptical about the timing changes reported by the speedcenter but Sebastian Ullrich seemed to be confident that something good had actually happened here. It's just that nobody knows why.

[Yaël Dillies]

I too would like to know! Happy to answer questions about the diff

[Jovan Gerbscheid]

I took a close look at the performance difference, and I found a surprising reason for the speedup:

The value of the instance AddMonoidAlgebra.commSemiring has changed into a form that is nicer for unification to deal with. It is now defined as

instance commSemiring : CommSemiring (MonoidAlgebra R M) where

which elaborates to the value

{ toSemiring := semiring, mul_comm := ⋯ }

But before @Yaël Dillies 's PR, it was

instance commSemiring : CommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.semiring with }

which elaborates to this mess:

  let __src := nonUnitalCommSemiring;
  let __src_1 := semiring;
  { toNonUnitalSemiring := __src.toNonUnitalSemiring, toOne := __src_1.toOne, one_mul := ⋯, mul_one := ⋯,
    toNatCast := __src_1.toNatCast, natCast_zero := ⋯, natCast_succ := ⋯, npow := Semiring.npow, npow_zero := ⋯,
    npow_succ := ⋯, mul_comm := ⋯ }

During unification, Lean was checking that AddMonoidAlgebra.commSemiring and AddMonoidAlgebra.semiring give the same semiring. With the new definition, this is immediate. With the old definition, it had to do a lot of unfolding to figure out that the different operations like one, npow, natCast were all definitionally equal.

[Matthew Ballard]

Does docs#Mathlib.Elab.FastInstance.fastInstance convert the latter to the former?

[Jovan Gerbscheid]

The only thing that fastInstance% does is unfold things. So no, it doesn't turn the latter into the former. The former is in some sense "more folded up".

[Matthew Ballard]

No, it tries to infer instances at each step. Or it should. Then it checks we didn't leave the defeq class.

[Jovan Gerbscheid]

Ah, you are right, it does turn the latter into the former!

[Jovan Gerbscheid]

That's great, because I think that means that we could turn the fast_instance% code into a linter that checks if an instance could be defined in a better way, right?

[Matthew Ballard]

Yes

[Jovan Gerbscheid]

Does someone know how a linter is supposed to know which new declarations are added by the given command? I don't want to make this an environment linter, because the linter should run in the same environment as where the instance was elaborated. (Otherwise it might suggest defining A in terms of B when B is defined after A)

[Eric Wieser]

If our goal is to run the linter to check for every place where fast_instance% is legal, maybe we should just override where to always use it

[Jovan Gerbscheid]

The bad code in this case did not use where, but := { ... with }

[Matthew Ballard]

Or it should

There are some things that would be nice to catch, like when an instance uses a projection and that uses a crooked instance.

@Eric Wieser didn't you try the override at some point? I am skeptical we about wanting to always rerun the defeq checks everytime we hit where. A code suggestion would be great.

[Jovan Gerbscheid]

I was more thinking of running such a linter once, to see where the bad instances currently are in Mahtlib. And then see how much performance we can gain from this.

[Eric Wieser]

How would we create the code suggestion if not by running fast_instance% speculatively which runs the same checks?

[Eric Wieser]

Ah indeed, a linter that is not always enabled would work

[Damiano Testa]

As for figuring out which declarations are introduced by a command, the function docs#Mathlib.Linter.getNamesFrom was written precisely with this in mind and to be run from a linter.

[Damiano Testa]

I do not know whether it still works well with Elab.async, since this was when elaboration was still not done in parallel.

[Jovan Gerbscheid]

This discovery lead me to try making #30734. In that PR I try to remove all patterns of the form mul := (· * ·) in an instance definition, which are unneccessary. This removes over 200 lines of code and speeds up mathlib by 0.63%. And this includes a 12.05% speedup in JacobiZariski!