Deprecation and time out

Stream: mathlib4

[Antoine Chambert-Loir]

The recent PR #14168 (June 26, 2024) deprecated a number of AlgHom.map_* lemmas on the basis that they are redundant, and asks to replace them with the standard map_* lemma. Unfortunately, this leads to time out problems, in mathlib (as explained in the documentation of the PR), and in the project with @María Inés de Frutos Fernández .

[Antoine Chambert-Loir]

Here is a mwe:

import Mathlib.RingTheory.TensorProduct.Basic

open TensorProduct

variable {R A : Type*} [CommRing R] [CommRing A]

lemma foo [Algebra A R] (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S}
    {T₀ : Subalgebra A R} (x y : ↥T₀ ⊗[A] ↥S₀) :
    (Algebra.TensorProduct.map T₀.val S₀.val) x + (Algebra.TensorProduct.map T₀.val S₀.val) y =
    (Algebra.TensorProduct.map T₀.val S₀.val) (x + y) := by
  rw [AlgHom.map_add] -- But `rw [map_add]` times out.

[María Inés de Frutos Fernández]

The proof exact Eq.symm (map_add (Algebra.TensorProduct.map T₀.val S₀.val) x y) also works in my laptop, but it is slow.
(In the online editor it also times out).

[Riccardo Brasca]

I also noticed the same thing.

[Ruben Van de Velde]

Ugh. Does it still work with rw if you explicitly pass the hom?

[María Inés de Frutos Fernández]

No, it times out as well.

[Kevin Buzzard]

  [synthInstance] [1.237288] ✅️ NonUnitalNonAssocSemiring ({ x // x ∈ T₀ } ⊗[A] { x // x ∈ S₀ }) ▶

is at least part of the problem.

[Kevin Buzzard]

Random hacks like attribute [-instance] Subalgebra.smulCommClass_right in fix the timeout (this is just looking at things in the instance trace which are making things go the long way around)

[Johan Commelin]

We should try to mwe this further. @Antoine Chambert-Loir I have recorded your MWE as the following issue: 

map_add times out, and AlgHom.map_* is deprecated #17507

[Antoine Chambert-Loir]

Thanks a lot. But I don't know what I can do for it.
(Actually, it would be useful, and even reasonable, that “advanced” users of Lean start learning seriously this kind of stuff, but for the moment I feel lost there.)

[Kevin Buzzard]

My experience with trying to minimise these things is that the actual problem might be that mathlib is big, so when you try to minimise, things then get much quicker.

[Antoine Chambert-Loir]

What I mean is that I have no clue about the internal process ran by the compiler. I only have an abstract understanding (if at all) of all the terms that are uttered here and there — unification, typeclass inference, etc. And the game of setting some option (but which one, how can one remember?) to try to find out remains a mysterious one.

[Johan Commelin]

@Antoine Chambert-Loir I didn't mean to oblige you into more work. Actually, there's ongoing work to help automate further minimization of such problems. So we should wait a bit, but maybe this isn't a skill that people should invest in for the future.

[Kevin Buzzard]

I commented on the GitHub issue by the way. I think it's pretty clear what the problem is, but the only solution I can think of is a massive refactor of mathlib changing the way the order hierarchy interacts with the algebra hierarchy.

I'll repeat my thoughts here: the issue is that whenever faced with a goal of the form "↥X acts on Y" where X is a subthing (eg a subalgebra) of R, but coerced to a type, then lean can apply a fact from typeclass inference saying "it suffices to prove that R acts on Y". This fact turns true statements into false ones in these problematic cases (R is too big to act on Y) and then typeclass inference attempts to use the order hierarchy to find the action and takes a long time to fail because it's so big.

[Kevin Buzzard]

The trace makes dismal reading because any attempt to solve this unsolvable goal using order theory is necessarily completely fruitless because there is no order in the question. The easiest fix would just be to not import any order stuff but this is not feasible in practice

[Kevin Buzzard]

Possibly related comment here.

[Michael Stoll]

There is the approach I tried in #12778, but @Yaël Dillies vetoed it on the grounds that it is not the right way of doing things. Alas, nothing seems to have come of the plans to do it the right way:tm: ...

[Daniel Weber]

Kevin Buzzard said:

[...]

I'll repeat my thoughts here: the issue is that whenever faced with a goal of the form "↥X acts on Y" where X is a subthing (eg a subalgebra) of R, but coerced to a type, then lean can apply a fact from typeclass inference saying "it suffices to prove that R acts on Y". [...]

Would it perhaps be possible to give that instance low priority (or the other instance high priority), or would that cause more harm than good?

[Kevin Buzzard]

This is pretty much what Michael did in #12778 and the results looked really good!

[Kevin Buzzard]

annoyingly, I can't remember how to change the priority of an instance to low. The troublesome instances here are docs#Subalgebra.smulCommClass_right, docs#IsScalarTower.subalgebra' and docs#Subalgebra.isScalarTower_mid

I bet that decreasing the prio of these instances will make the example above work fine.

[Antoine Chambert-Loir]

Could we remove these instances in a given file ?

[Michael Stoll]

Maybe something like attribute [local instance 50] ...?

[Michael Stoll]

import Mathlib.RingTheory.TensorProduct.Basic

open TensorProduct

attribute [local instance 50] Subalgebra.smulCommClass_right
  IsScalarTower.subalgebra' Subalgebra.isScalarTower_mid

variable {R A : Type*} [CommRing R] [CommRing A]

count_heartbeats in -- 32416
lemma foo [Algebra A R] (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S}
    {T₀ : Subalgebra A R} (x y : ↥T₀ ⊗[A] ↥S₀) :
    (Algebra.TensorProduct.map T₀.val S₀.val) x + (Algebra.TensorProduct.map T₀.val S₀.val) y =
    (Algebra.TensorProduct.map T₀.val S₀.val) (x + y) := by
  rw [map_add]

[Michael Stoll]

The tipping point is prio 999 vs 1000.

[Kevin Buzzard]

I always imagine that prio should be involved (like when you're declaring the instance) and then my search fails me.

[Kevin Buzzard]

@Yaël Dillies do you have an objection to globally lowering the prio of these instances?

[Yaël Dillies]

I see the results of the benchmark, but tweaking priorities only makes working TC searches faster. Failing ones will still search the full tree

[Kevin Buzzard]

Right, but this is making less of them fail!

[Yaël Dillies]

I think we can tweak the priorities, but the better thing would be to fully cut off the hierarchies

[Yaël Dillies]

And I've been working recently on making less lemmas rely on bundled algebra+order classes. I believe that's a requirement to a greater overhaul.

[Yaël Dillies]

Anyway, you can tweak the priorities in the meantime

[Yuyang Zhao]

Kevin Buzzard said:

Possibly related comment here.

It's even worse there, I'll make a mwe.

[Michael Stoll]

I've tried to update #12778. It passes CI, but benching it gives an error.

[Yuyang Zhao]

The speedcenter is still broken.

[Michael Stoll]

After merging master again, the speed center works agaon on #12778, and it shows a gain of 9.7% in typeclass inference. There are some files that get slower, but this should be fixable with a bit more tinkering...

[Yaël Dillies]

It's funny how the files that got slower are mostly mine :thinking: Maybe because I mostly do algebraic order stuff?

[Michael Stoll]

I think there has been some refactoring, so probably there are some files or declarations that now need the open scoped AlgebraOrderInstances, but didn't before, and there are most likely some new files, too. If I have time, I'll look at that (but you @Yaël Dillies or anybody else is also welcome to do so).

[Yuyang Zhao]

I've recently come back to the FunLike hierarchy slowness. (Before adjusting the priorities) #17675 has a 10x speedup for some other examples, but not for the examples in this topic. I realized we have docs#RingHomClass.toLinearMapClassNNRat and docs#RingHomClass.toLinearMapClassRat, but the scalar type parameter of docs#LinearMapClass is outParam. This may have caused some failed attempts and slow unification.

I'm not sure it's the critical issue of performance, but this looks wrong...

[Yuyang Zhao]

If we want these two instances, should we refactor LinearMapClass? cc @Yaël Dillies who added them.

[Yury G. Kudryashov]

Why do we want these instances, esp. with RingHomClass assumptions?

[Yury G. Kudryashov]

docs#map_rat_smul and docs#map_nnrat_smul have much weaker assumptions

[Yaël Dillies]

Hmm, I don't remember why I needed those instances off the top of my head. I would have to dig through APAP

[Yaël Dillies]

Yury G. Kudryashov said:

docs#map_rat_smul and docs#map_nnrat_smul have much weaker assumptions

Yes, but they don't return a linear map, which makes them somewhat useless in linear map-full applications

[Yaël Dillies]

Something that will definitely work for now is to make them non-instances

[Yury G. Kudryashov]

You can use docs#AddMonoidHom.toRatLinearMap

[Yury G. Kudryashov]

(which can be generalized to AddMonoidHomClass)