Adic completion is slow

Stream: mathlib4

[Christian Merten]

In PR #14358 the map (AdicCompletion I R) ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M is constructed and shown to be surjective if M is R-finite. During review, @Riccardo Brasca voiced concerns that the file is quite slow, which I agree with. Apart from some slow simp calls that I now squeezed (at the cost of up to 6 lines of simp only [...]), a few rws are quite slow, but I have no idea how to make this faster.

If anyone has ideas how to speed things up, I'd be very happy to hear suggestions. If it helps, this is the output from trace.profiler true: https://share.firefox.dev/4cMVnSA

[Riccardo Brasca]

The file is not horribly slow, but maybe it's better to understand now if there is something wrong.

[Matthew Ballard]

I think one of my local copies of mathlib is unoccupied atm

[Matthew Ballard]

My guess:

instance : AddCommGroup (AdicCompletion I M) :=
  inferInstanceAs <| AddCommGroup (submodule I M)

instance : Module R (AdicCompletion I M) :=
  inferInstanceAs <| Module R (submodule I M)

[Christian Merten]

I see that those two instances appear quite often in the Meta.isDefEq checks for M = R. Could you explain a bit more why these are problematic and what I could try to make it better?

[Matthew Ballard]

Too many instances on Submodule's

[Christian Merten]

Do you think that explicitly spelling out the AddCommGroup and Module instances might make it faster?

[Matthew Ballard]

It could. I had to step away from the computer

[Christian Merten]

I'll try it out, thanks!

[Christian Merten]

The build time is down from ~30 seconds to ~5 seconds! Thanks a lot @Matthew Ballard

[Christian Merten]

So #14534 improves the situation in the AsTensorProduct file, as this benchmark shows: http://speed.lean-fro.org/mathlib4/compare/5f4b267e-9678-4a5a-962b-48ce7e897ba0/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=b134ed19aefe23e70c97e512b219dabce25824d7.

The increased instructions in the Basic and Algebra files are probably acceptable?

(The reduced instruction count in the Functoriality file are due to some added noncomputables)

[Matthew Ballard]

I left some comments

[Matthew Ballard]

The overall slowdown on master seems very small compared the eventual gains

[Christian Merten]

I just did another benchmark comparing two versions of setting up the instances:

• completely manual, i.e. writing out the full instance definition (commit: https://github.com/leanprover-community/mathlib4/pull/14358/commits/55cf90705c3509ab5da127b7ecd4db0e147af667)
• using docs#Function.Injective.commRing and friends (commit: https://github.com/leanprover-community/mathlib4/pull/14358/commits/00f96b96084f0a3e14793105fdda6a08a378c266)

While both are an improvement to the current status, the first version significantly outperforms the second one as this comparison shows:
http://speed.lean-fro.org/mathlib4/compare/04e26275-26be-4d08-8dd1-ffeb4e23bd0e/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=55cf90705c3509ab5da127b7ecd4db0e147af667

[Kevin Buzzard]

docs#Function.Injective.commRing and friends used to be the cause of huge slowdowns because they would cause typeclass inference to take everything apart (TC inference had to solve lots of "this commring instance equals that one" goals, and it would solve them by destructing everything creating 10+ other problems). Is this still happening?

[Christian Merten]

Kevin Buzzard said:

docs#Function.Injective.commRing and friends used to be the cause of huge slowdowns because they would cause typeclass inference to take everything apart (TC inference had to solve lots of "this commring instance equals that one" goals, and it would solve them by destructing everything creating 10+ other problems). Is this still happening?

I don't have a trace of the docs#Function.Injective.commRing version, but the original version with inferInstanceAs <| CommRing (subring I) caused precisely what you describe.

[Matthew Ballard]

It is doing a lot of compiling now!

[Matthew Ballard]

Oh I guess it was before also. But not it is doubled.

[Christian Merten]

Not in the AsTensorProduct file though, right? (everything is noncomputable there).

[Christian Merten]

Matthew Ballard said:

It is doing a lot of compiling now!

Where do you see this? In the benchmark?

[Christian Merten]

Ah, found it. Its both in the Basic and in the Algebra file. Should I just put a noncomputable section at the top?

[Matthew Ballard]

noncomputable section means "try to compile and give up if you can't"

[Christian Merten]

Ah, so mark everything with noncomputable instead?

[Matthew Ballard]

suppress_compilation

[Matthew Ballard]

docs#commandSuppress_compilation

[Matthew Ballard]

The increase is compilation and the increase in typeclass inference are the two main drivers of the regression

[Matthew Ballard]

irreducible isn't really doing you many favors in these files. Not sure about downstream

[Matthew Ballard]

With suppress_compilation at the top and the irreducible attributes removed, I get an improvement overall.

Though I am not a big fan of the repeated Subtype.ext <| proof pattern

[Christian Merten]

Matthew Ballard said:

With suppress_compilation at the top and the irreducible attributes removed, I get an improvement overall.

Though I am not a big fan of the repeated Subtype.ext <| proof pattern

I'd be happy to get rid of the Subtype.ext <| proof pattern, but the alternatives don't seem to provide the same performance gains.

[Christian Merten]

Matthew Ballard said:

With suppress_compilation at the top and the irreducible attributes removed, I get an improvement overall.

Though I am not a big fan of the repeated Subtype.ext <| proof pattern

Should I only remove the two problematic irreducibles (for mul and smul')? Or do you think it's better to get rid of all of them?

[Matthew Ballard]

I really don't want Lean peeking in these too much because the definition are pretty intense. But it doesn't seem to be a problem (yet).

I would hold off on using @[irreducible] until there is a demonstrated need.

When #11521 lands, using Function.Injective.commRing etc should be much better

[Kevin Buzzard]

What needs to happen to get that PR landed?

[Johan Commelin]

I guess we need to lock Eric and Kyle in a room for 1 day...

[Matthew Ballard]

It would be nice to see if #11521 does help. Assuming yes, then we can use the injective/surjective constructors now and improve later.