Enormous speedup from `dsimp` caching in `simp`

Stream: lean4

[Jovan Gerbscheid]

In lean4#7428, I added a dsimp cache to the simp state, so that in a single simp call different calls to dsimp share their cache.

For example, when simplifying a * b for some a b : A, currently dsimp is ran on each A with a fresh cache, thus duplicating the work (recall a * b is HMul.hMul A A A _ a b). By keeping the cache, A only needs to be visited once.

The resulting Mathlib speedup is enormous:

Metric                 Change
=============================
instructions            -8.1%
task-clock              -7.4%
simp                   -45.6%
instantiate metavars   -11.7%
share common exprs      -8.2%

[Kevin Buzzard]

build: -13458.961⬝10⁹(-8.06%)!

[Eric Wieser]

Jovan Gerbscheid said:

recall a * b is HMul.hMul A A A _ a b

Or more often (e.g. for Field A),

@HMul.hMul.{u_1, u_1, u_1} A A A
  (@instHMul.{u_1} A
    (@Distrib.toMul.{u_1} A
      (@NonUnitalNonAssocSemiring.toDistrib.{u_1} A
        (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} A
          (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} A
            (@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} A
              (@CommRing.toNonUnitalCommRing.{u_1} A
                (@EuclideanDomain.toCommRing.{u_1} A (@Field.toEuclideanDomain.{u_1} A instField)))))))))
  a b

which has 15 As!

[Eric Wieser]

The performance gains seem to be very biased towards Category theory and AlgebraicGeometry, which makes since given that these have many dsimp-able expressions in place of types

[Jovan Gerbscheid]

I wonder if this also removes the need for the sequence dsimp; simp, which is sometimes faster than simp.

[Matthew Ballard]

This is great! The suggested transformWithCache seems pretty useful in itself.

[Jovan Gerbscheid]

Is there something that this PR is still waiting for?

[Kim Morrison]

@Jovan Gerbscheid we really don't want to touch simp at the moment, but I appreciate this speedup is extraordinary. It's on the radar, we aren't ignoring it.

[Kim Morrison]

@Jovan Gerbscheid, and others interested.

After talking to Leo, we've decided we want to wait on this one, the considerable speed-up notwithstanding.

simp still needs a thorough overhaul, and it makes sense to do this all at once. (There's the outstanding issue of dsimp getting bogged down in proofs --- and the related question of how this PR interacts with that problem --- plus the bigger issue of simp switching to dsimp in implicit arguments often breaking reducible-level typechecking. There's also still problems with what simp? reports in some situations, etc. etc.)

Next quarter Leo is doing some substantial work on extensions to grind, including work on Grobner bases and AC rewriting/matching. We think that after that we'll be well placed to return to simp (and possibly be able to integrate some of those features into simp itself), and so we want to bundle changes like this into that overhaul, which we expect to do in Q3 this year.

I appreciate that this is a while to wait, but hopefully you can appreciate both that changes like this are touching absolutely critical components and we want to consider them carefully (not just for the impact on Mathlib), and that for the sake of efficiency we want to avoid too much context switching in the automation development work, and hence want to bundle this with other planned changes.

[Jovan Gerbscheid]

Although I would still really like to see the dsimp caching fixed in lean, if this isn't happening any time soon, at least we can go ahead and merge #21330.

I originally wanted to wait for the improvements in simp to see whether #21330 is still needed after that, but in the status quo, it is definitely an improvement.

[Yury G. Kudryashov]

Are there any public details about the planned Grobner bases support? E.g., what's the target generality?

[Kim Morrison]

re: coefficients? That I'm not sure, I will ask.

[Yury G. Kudryashov]

I wonder how much work will we need to duplicate to make it useful for dealing with CommRings or ZMod.