Zulip Chat Archive

Stream: mathlib4

Topic: Timeout in Submodule (π“ž K) (π“ž K)

Xavier Roblot (Dec 08 2023 at 19:30):

Lean cannot synthesize Module (π“ž K) (π“ž K) without an increase of heartbeats. 

import Mathlib.NumberTheory.NumberField.Basic

open NumberField

variable (K : Type*) [Field K] [NumberField K]

variable (I : Ideal (π“ž K)) -- OK

variable (M : Submodule (π“ž K) (π“ž K)) -- Timeout

Is it something to worry about?

Andrew Yang (Dec 08 2023 at 20:34):

My experience in FLT regular is that π“ž K is usually very slow to work with, and I use [IsIntegralClosure B A K] whenever possible. And we also had

attribute [local instance 2000] inst_ringOfIntegersAlgebra Algebra.toSMul Algebra.toModule

which would for example make Submodule (π“ž K) (π“ž K) instant.

Andrew Yang (Dec 08 2023 at 20:37):

Looking at the trace of the output without these hacks, I guess things would also improve if the ordered-algebraic classes or topological-algebraic classes were scoped. But this might be controversial.

YaΓ«l Dillies (Dec 08 2023 at 20:40):

What kind of classes is it looking for? If it's CovariantClass/ContravariantClass, I might have a speedup to offer.

Andrew Yang (Dec 08 2023 at 20:43):

I'm referring to these
image.png
Though I'm not sure these are the culprit yet.

YaΓ«l Dillies (Dec 08 2023 at 20:47):

Oh yeah no. Those are fast and sturdy and very very useful everywhere.

Andrew Yang (Dec 08 2023 at 20:58):

In

import Mathlib.NumberTheory.NumberField.Basic

open NumberField

variable (K : Type*) [Field K] [NumberField K]

set_option profiler true
set_option trace.Meta.synthInstance.tryResolve true
set_option trace.Meta.isDefEq true
set_option synthInstance.maxHeartbeats 1000000
set_option maxHeartbeats 10000000000

variable (M : Submodule (π“ž K) (π“ž K)) -- Timeout

There is a [12.650751s] βœ… IsDomain β†₯(π“ž K) β‰Ÿ IsDomain β†₯(π“ž K), which looks like lean is having a trouble unifying
Subalgebra.toCommRing with SubringClass.toRing.
Maybe @Anne Baanen knows what's going on?

Anne Baanen (Dec 08 2023 at 22:28):

Oh that's a big issue indeed, worth looking into. Don't know from the top of my head what's going wrong here, the defeq cache is a lot more robust nowadays so I assume it's not the same equality being tested exponentially often, right?

Adam Topaz (Dec 08 2023 at 22:37):

Should we make docs#NumberField.ringOfIntegers irreducible?

Matthew Ballard (Dec 12 2023 at 21:39):

You can get away with just set_option synthInstance.maxHeartbeats 50000 if using lean4#2478

Xavier Roblot (Dec 13 2023 at 10:27):

Adam Topaz said:

Should we make docs#NumberField.ringOfIntegers irreducible?

If that just means replacing def by irreducible_def in the definition of ringOfIntegers, then it does not help much... It still get a timeout when I try #synth Module (π“ž K) (π“ž K)

Kevin Buzzard (Jan 11 2024 at 13:35):

Andrew just reminded me of this issue in their FLT-regular talk at Lean Together 2024. I think the relevant part of the instance trace is this:

        [tryResolve] [9.838419s] βœ… IsDomain β†₯(π“ž K) β‰Ÿ IsDomain β†₯(π“ž K) β–Ό
          [isDefEq] [4.865673s] βœ… IsDomain β†₯(π“ž K) =?= IsDomain β†₯?m.9046 β–Ό
            [] [4.865389s] βœ… CommSemiring.toSemiring =?= Ring.toSemiring β–Ό
              [] [4.865353s] βœ… Ring.toSemiring =?= Ring.toSemiring β–Ό
                [delta] [4.865339s] βœ… Ring.toSemiring =?= Ring.toSemiring β–Ό
                  [] [4.865321s] βœ… CommRing.toRing =?= SubringClass.toRing (π“ž K) β–Ό
                    [] [4.865221s] βœ… CommRing.toRing =?= Function.Injective.ring Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0)
                          (_ : ↑1 = ↑1) (_ : βˆ€ (x x_1 : β†₯(π“ž K)), ↑(x + x_1) = ↑(x + x_1))
                          (_ : βˆ€ (x x_1 : β†₯(π“ž K)), ↑(x * x_1) = ↑(x * x_1)) (_ : βˆ€ (x : β†₯(π“ž K)), ↑(-x) = ↑(-x))
                          (_ : βˆ€ (x x_1 : β†₯(π“ž K)), ↑(x - x_1) = ↑(x - x_1))
                          (_ : βˆ€ (x : β†₯(π“ž K)) (x_1 : β„•), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                          (_ : βˆ€ (x : β†₯(π“ž K)) (x_1 : β„€), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                          (_ : βˆ€ (x : β†₯(π“ž K)) (x_1 : β„•), ↑(x ^ x_1) = ↑(x ^ x_1)) (_ : βˆ€ (x : β„•), ↑↑x = ↑↑x)
                          (_ : βˆ€ (x : β„€), ↑↑x = ↑↑x) β–Ά
          [isDefEq] [4.941348s] βœ… ?m.8348 =?= SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing (π“ž K) β–Ά

The thing taking all of the time is checking IsDomain β†₯(π“ž K) β‰Ÿ IsDomain β†₯(π“ž K), something which looks obvious but the problem is that one of the ring structures is coming from CommSemiring.toSemiring and the other from Ring.toSemiring, and typeclass inference has a habit of sometimes exploding with these kinds of question. The 4.5 seconds is just breaking down into many many tiny goals which then keep exploding again, e.g.

                                  [delta] [0.566770s] βœ… AddGroupWithOne.zsmul =?= AddGroupWithOne.zsmul β–Ό
                                    [] [0.566496s] βœ… Function.Injective.addGroupWithOne Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0)
                                          (_ : ↑1 = ↑1)
                                          (_ : βˆ€ (x x_1 : β†₯(Subalgebra.toSubring (π“ž K))), ↑(x + x_1) = ↑(x + x_1))
                                          (_ : βˆ€ (x : β†₯(Subalgebra.toSubring (π“ž K))), ↑(-x) = ↑(-x))
                                          (_ : βˆ€ (x x_1 : β†₯(Subalgebra.toSubring (π“ž K))), ↑(x - x_1) = ↑(x - x_1))
                                          (_ : βˆ€ (x : β†₯(Subalgebra.toSubring (π“ž K))) (x_1 : β„•), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                                          (_ : βˆ€ (x : β†₯(Subalgebra.toSubring (π“ž K))) (x_1 : β„€), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                                          (_ : βˆ€ (x : β„•), ↑↑x = ↑↑x)
                                          (_ :
                                            βˆ€ (x : β„€),
                                              ↑↑x =
                                                ↑↑x) =?= Function.Injective.addGroupWithOne Subtype.val
                                          (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0) (_ : ↑1 = ↑1)
                                          (_ : βˆ€ (x x_1 : β†₯(π“ž K)), ↑(x + x_1) = ↑(x + x_1))
                                          (_ : βˆ€ (x : β†₯(π“ž K)), ↑(-x) = ↑(-x))
                                          (_ : βˆ€ (x x_1 : β†₯(π“ž K)), ↑(x - x_1) = ↑(x - x_1))
                                          (_ : βˆ€ (x : β†₯(π“ž K)) (x_1 : β„•), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                                          (_ : βˆ€ (x : β†₯(π“ž K)) (x_1 : β„€), ↑(x_1 β€’ x) = ↑(x_1 β€’ x))
                                          (_ : βˆ€ (x : β„•), ↑↑x = ↑↑x) (_ : βˆ€ (x : β„€), ↑↑x = ↑↑x) β–Ά

@Matthew Ballard do you understand how to fix these kinds of problems nowadays?

Kevin Buzzard (Jan 11 2024 at 13:38):

This seems to be a minimal hack which "fixes" the issue:

import Mathlib.Algebra.Module.Submodule.Basic
import Mathlib.NumberTheory.NumberField.Basic

variable (K : Type*) [Field K] [NumberField K]

open NumberField

attribute [local instance 1001] Algebra.toModule -- makes it quick; 1000 not good enough

set_option synthInstance.maxHeartbeats 0 in
set_option maxHeartbeats 0 in
set_option trace.profiler true in
variable (M : Submodule (π“ž K) (π“ž K))

Andrew Yang (Jan 11 2024 at 13:53):

Matthew Ballard said:

You can get away with just set_option synthInstance.maxHeartbeats 50000 if using lean4#2478

This is the structure flattening I was talking about. This alone does not solve the problem though.

Kevin Buzzard (Jan 11 2024 at 14:34):

Not the main issue, but I was surprised to run into this in the trace:

      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)
      [Meta.synthInstance] ❌ Field β„€
        [Meta.synthInstance] result <not-available> (cached)

Matthew Ballard (Jan 11 2024 at 14:37):

See also #mathlib4 > example (p : P) : Q := p takes 0.25s to fail!

Matthew Ballard (Jan 11 2024 at 14:38):

Matthew Ballard said:

Getting flashbacks


Kevin Buzzard (Jan 11 2024 at 14:44):

Here's the fix which demotes the bad instance rather than promotes the good one:

import Mathlib.Algebra.Module.Submodule.Basic
import Mathlib.NumberTheory.NumberField.Basic

variable (K : Type*) [Field K] [NumberField K]

open NumberField

attribute [local instance 909] Subalgebra.module' -- 910 no good

variable (M : Submodule (π“ž K) (π“ž K))

Matthew Ballard (Jan 11 2024 at 14:48):

Is that searching over all A?

Matthew Ballard (Jan 11 2024 at 15:52):

It is committing to R = β„€ in

instance module' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : Module R' S :=
  S.toSubmodule.module'

and then trying everything to get SMul K β„€

Anne Baanen (Jan 11 2024 at 16:00):

As a quick fix it sounds like a decent idea to lower the priority of docs#Subalgebra.module', since the "default" instance is docs#Subalgebra.module

Anne Baanen (Jan 11 2024 at 16:03):

I find it weird though that there is this free parameter that becomes β„€: in module' every parameter is specified by the expected type.

Matthew Ballard (Jan 11 2024 at 16:04):

In the process of now of priority := low

Anne Baanen (Jan 11 2024 at 16:06):

Anne Baanen said:

I find it weird though that there is this free parameter that becomes β„€: in module' every parameter is specified by the expected type.

Nevermind, we get R = β„€ because π“ž K : Subalgebra β„€ K.

Matthew Ballard (Jan 11 2024 at 16:06):

Should this even be an instance?

Anne Baanen (Jan 11 2024 at 16:08):

I believe there are a few uses where we have a tower of ring extensions and want to make a subalgebra to put something in between the top. So I think yes, it should be an instance.

Matthew Ballard (Jan 11 2024 at 16:09):

I've seen other places where this pattern is a performance hit

Anne Baanen (Jan 11 2024 at 16:09):

I'll try de-instancing it on my machine and seeing how much breaks.

Matthew Ballard (Jan 11 2024 at 16:09):

Yeah, I took the easy way out :)

Matthew Ballard (Jan 11 2024 at 16:19):

Well, success for the example. I'll bench next.

Anne Baanen (Jan 11 2024 at 16:35):

At least the following files rely on the instance:

Matthew Ballard (Jan 11 2024 at 16:36):

#9655 is on the benchmark queue so maybe that will be enough

Matthew Ballard (Jan 11 2024 at 17:15):

No change with performance overall - up for review

Antoine Chambert-Loir (Jan 19 2024 at 12:56):

@Anne Baanen , what happens if those 3 files are added a local instance?

Anne Baanen (Jan 22 2024 at 18:36):

Actually it turns out I disabled the wrong instance: Submodule.module' instead of Subalgebra.module'. According to branch#uninstance-Subalgebra-module-tower on my machine, it is totally fine to remove this instance altogether!

Matthew Ballard (Jan 22 2024 at 18:37):

I think this is prudent since the integers will end up satisfying the constraints often

Kevin Buzzard (Apr 22 2024 at 23:51):

I occasionally come back to this question. Here is a summary of the issue (or at least, one of the issues):

import Mathlib.Tactic

variable (K : Type) [Field K] [NumberField K]

open NumberField

-- #synth SMul (π“ž K) (π“ž K) -- times out

set_option synthInstance.maxHeartbeats 70000 in -- fails at 60000
set_option trace.Meta.synthInstance true in
set_option trace.profiler true in
#synth SMul (π“ž K) (π“ž K) -- fails without instance maxHeartbeats bump

This kind of failure makes working with integers of number fields very difficult. There are other variants, e.g. if LL is also a number field and a KK-algebra, then SMul (π“ž K) (π“ž L) also takes forever, even though Algebra (π“ž K) (π“ž L) is fast.

What I've discovered whilst sitting jetlagged in a hotel in Singapore at 5am is that the problem is the following: Because π“ž K is actually a term of type Subalgebra \Z K, the goal is really SMul β†₯(π“ž K) β†₯(π“ž K). Typeclass inference can find 15 or so instances which apply, but among them are the deadly instances Submonoid.smul, Subsemiring.smul , and the poorly-named Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra which should really be called Subalgebra.smul. The type of Submonoid.smul is basically [SMul M' Ξ±] (S : Submonoid M') : SMul (β†₯S) Ξ± and you can now guess what the others are. These do look good syntactically for a goal of SMul β†₯(π“ž K) β†₯(π“ž K), but they are deadly because they leave a goal of the form SMul K (π“ž K) and this takes 2.5 seconds to fail on my machine.

So now I realise that this is the same problem as #synth SMul β„‚ ℝ that we saw in another thread, although this is even worse because it takes even longer to give up.

In this situation it is extremely difficult to steer typeclass inference away from ever running into the goal SMul K (π“ž K), so the question is whether it is possible to make it fail quickly. 

import Mathlib.Tactic

variable (K : Type) [Field K] [NumberField K]

open NumberField

set_option synthInstance.maxHeartbeats 70000 in
set_option trace.Meta.synthInstance true in
set_option trace.profiler true in
#synth SMul K (π“ž K) -- fails after thousands of lines of nonsense

Riccardo Brasca (Apr 23 2024 at 03:53):

Thanks for looking at this. If you want a concrete example to work on, in #11792 there is a discussion about a rather slow file.

Riccardo Brasca (Apr 23 2024 at 03:54):

BTW, is there a simple way of profiling a file? I mean, set_option profiler true gives information about any single declaration, I would like to have the total.

Michael Stoll (Apr 23 2024 at 09:20):

If you do lake build <Module> in the terminal (on a file containing set_option profiler true near the beginning), it also prints a summary at the end.

Michael Stoll (Apr 23 2024 at 09:24):

Kevin Buzzard said:

In this situation it is extremely difficult to steer typeclass inference away from ever running into the goal SMul K (π“ž K), so the question is whether it is possible to make it fail quickly.

You could try to remove the instance attribute locally from the instance leading to the problematic SMul K (π“ž K) search (or reduce its priority). You could possibly also try to increase the priority of the instance you want to trigger. Or you could make (local) shortcut instances for SMul (π“ž K) (π“ž K)and SMul (π“ž K) (π“ž L).

I've been working on one of the very slow Mathlib files to see if I can speed it up, and I'll report on this soon somewhere here. Stay tuned!

YaΓ«l Dillies (Apr 23 2024 at 10:11):

I believe there's a better solution: Replace

def ringOfIntegers : Subalgebra β„€ K := integralClosure β„€ K

by

def ringOfIntegers : Type _ := integralClosure β„€ K

YaΓ«l Dillies (Apr 23 2024 at 10:12):

Then your TC goals will be Submodule (π“ž K) (π“ž K) rather than Submodule β†₯(π“ž K) β†₯(π“ž K) and will match many less instances.

YaΓ«l Dillies (Apr 23 2024 at 10:13):

Of course, this comes at the cost of π“ž K not being a Subalgebra anymore, but the coercion to Type _ of one.

Riccardo Brasca (Apr 23 2024 at 10:22):

I was also thinking about this... I will try to see how annoying it is.

Anne Baanen (Apr 23 2024 at 12:07):

Another approach that we could try is to give the β†₯ coercion a different name for each setlike, instead of docs#SetLike.instCoeSortType.

YaΓ«l Dillies (Apr 23 2024 at 12:12):

Wouldn't Lean still try to unfold them?

Anne Baanen (Apr 23 2024 at 12:12):

I mean like we already do for coes:

def coeSort (s : MySubobject X) : Type* :=
  { x : X // x ∈ s }

instance : CoeSort (MySubobject X) Type* :=
  ⟨coeSort⟩

Anne Baanen (Apr 23 2024 at 12:13):

(Presumably using a @[coeSort] attribute to do delaboration.)

Anne Baanen (Apr 23 2024 at 12:13):

Then the discrimination tree can index on MySubobject.coeSort and we don't have the billion candidate instances.

YaΓ«l Dillies (Apr 23 2024 at 12:16):

Oh sorry, I misunderstood. Yes, that sounds reasonable.

Anne Baanen (Apr 23 2024 at 12:31):

One drawback of my idea is that all the instances on Subtype have to be copied over manually: LE, Coe, Mul, ...

Anne Baanen (Apr 23 2024 at 12:46):

Yeah, I don't see this working out. For example docs#MulMemClass.subtype must use the generic CoeSort instance, and docs#Subsemigroup.topEquiv_toMulHom must use the specific. We're definitely going to get type errors this way.

Anne Baanen (Apr 23 2024 at 12:48):

I think I'll try out YaΓ«l's plan instead. Defining RingOfIntegers as a Type instead of a Subalgebra is probably the least destructive alternative.

Kevin Buzzard (Apr 23 2024 at 14:02):

Michael Stoll said:

You could try to remove the instance attribute locally from the instance leading to the problematic SMul K (π“ž K) search (or reduce its priority).

There are multiple problematic instances (three).

You could possibly also try to increase the priority of the instance you want to trigger.

This all seems so brittle.

Or you could make (local) shortcut instances for SMul (π“ž K) (π“ž K)and SMul (π“ž K) (π“ž L).

Yes, probably this is what I'd do if I actually ran into this in practice. Basically the problem is that there are many misleading instances of the from SMul \u A \uB.

Anne Baanen (Apr 23 2024 at 16:33):

Anne Baanen said:

I think I'll try out YaΓ«l's plan instead. Defining RingOfIntegers as a Type instead of a Subalgebra is probably the least destructive alternative.

Seems to work fine! I didn't get totally to the end of fixing, feel free to take over branch#RingOfInteger_Type.

Riccardo Brasca (Apr 23 2024 at 16:34):

Great! I will have a look tomorrow morning (morning in Singapore)

Anne Baanen (Apr 23 2024 at 16:34):

Note that quite a bit of the difficulty comes from deciding to replace the coercion (π“ž K) β†’ K with algebraMap (π“ž K) K. Since both are in use at different places this seemed like a good opportuinity to standardize.

YaΓ«l Dillies (Apr 23 2024 at 16:55):

Fixed some of the style

YaΓ«l Dillies (Apr 23 2024 at 16:56):

I won't work on it more soon

Matthew Ballard (Apr 24 2024 at 00:28):

It builds now and the example above is much, much, much better.

Riccardo Brasca (Apr 24 2024 at 00:37):

Wow, thanks!!

Matthew Ballard (Apr 24 2024 at 00:37):

Most of the work was done already :)

Riccardo Brasca (Apr 24 2024 at 00:41):

I've created #12386 just to test

Matthew Ballard (Apr 24 2024 at 00:45):

It doesn't lint yet

Riccardo Brasca (Apr 24 2024 at 00:46):

Yep, I fixed the errors

Riccardo Brasca (Apr 24 2024 at 01:57):

The bench results are very good!

Riccardo Brasca (Apr 24 2024 at 02:45):

I've marked #12386 "awaiting review". I hope I have added everybody as coauthor, but I am not sure I did it in the right way, so don't hesitate to make any modification.

Riccardo Brasca (Apr 24 2024 at 02:48):

(@Anne Baanen I don't how to make you the main author, if you want to open another PR this is if course perfectly fine)

Jireh Loreaux (Apr 24 2024 at 02:55):

Hmmm... I'm wondering how often we should do this. Maybe it's a design pattern we should use elsewhere too.

Jireh Loreaux (Apr 24 2024 at 02:56):

I'm thinking of, for example, docs#elementalStarAlgebra

Riccardo Brasca (Apr 24 2024 at 03:02):

I don't know, but in practice everybody working with ring of integers noticed it is sometimes a pain.

YaΓ«l Dillies (Apr 24 2024 at 07:19):

Woohoo, that's seemingly the first time I got a good idea wrt performance :)

YaΓ«l Dillies (Apr 24 2024 at 07:20):

I would like to do the same to docs#circle not because of performance issues but because we never use it as a submonoid (and, like, it's mathematically a subgroup)

Anne Baanen (Apr 24 2024 at 09:01):

Riccardo Brasca said:

(Anne Baanen I don't how to make you the main author, if you want to open another PR this is if course perfectly fine)

Don't worry about attribution too much: being listed as a co-author is useful for finding the changes later, otherwise it's YaΓ«l's idea with Matt's and Riccardo's fixes so there is no one author.

Matthew Ballard (Apr 24 2024 at 11:32):

Jireh Loreaux said:

Hmmm... I'm wondering how often we should do this. Maybe it's a design pattern we should use elsewhere too.

I think part of the reason this is so bad is that Lean is led repeatedly to find some instance of a class on β„€ to make progress. But then β„€ matches almost everything.

Kevin Buzzard (Apr 24 2024 at 20:16):

Yes, Algebra K (O K) can lead quickly to Algebra K Z

YaΓ«l Dillies (Jul 25 2024 at 08:02):

I have written up the lessons learned in a wiki page: https://github.com/leanprover-community/mathlib4/wiki/Tradeoffs-of-concrete-types-defined-as-subobjects. I would happily turn it into a blog post if you think it would be valuable.

Kim Morrison (Jul 25 2024 at 10:28):

Yes please, a blog post would be great. We'd like to move away from having the wiki at all.

YaΓ«l Dillies (Jul 25 2024 at 11:45):

blog#86

YaΓ«l Dillies (Jul 25 2024 at 11:46):

Please in particular check the last paragraph. My understanding of the implications of Proj : Scheme is shaky

Andrew Yang (Jul 25 2024 at 17:05):

I think the underlying space of Proj A is not the same as the underlying space of Proj as a manifold anyways so I'm not sure if the example is right.

YaΓ«l Dillies (Jul 25 2024 at 18:39):

Hmm, okay, do people know of a better example?

Eric Wieser (Jul 27 2024 at 08:18):

I don't fully believe the head symbol claim; lean4 uses discrtrees nor head symbols for almost all indexing

YaΓ«l Dillies (Jul 27 2024 at 08:19):

How do you explain the performance boost in #12386 then?

Kevin Buzzard (Jul 27 2024 at 09:18):

IIRC this was caused by Module (π“ž K) (π“ž K) triggering a search for Module K (π“ž K) which took a long time to fail

Kevin Buzzard (Jul 27 2024 at 09:18):

The obvious solution Module.id or whatever it's called was being tried last because it is the first instance of module defined in mathlib and hence at the very back of the queue

Anne Baanen (Jul 29 2024 at 08:35):

Don't have the trace in front of me, but I believe it's effectively indexed on head symbols here anyway because in the instance declarations, the only arguments to the classes are free variables or other instances.

Yakov Pechersky (Aug 01 2024 at 20:55):

I'm hitting a related timeout currently working with residue fields. Is there a good way of resolving?

import Mathlib

open Valued

variable (K : Type*) [Field K] {Ξ“β‚€ : outParam Type*}
    [LinearOrderedCommGroupWithZero Ξ“β‚€] [vK : Valued K Ξ“β‚€]

example (n : β„•) : Module π’ͺ[K] (𝓂[K] ^ n : Ideal π’ͺ[K]) := Submodule.module _
example (n : β„•) : Module π’ͺ[K] (𝓂[K] ^ n : Ideal π’ͺ[K]) := by infer_instance -- timeout

Yakov Pechersky (Aug 01 2024 at 20:59):

Might have to do with Valued.ResidueField being a def (even reducible) and not an abbrev?

Matthew Ballard (Aug 01 2024 at 23:07):

The keys for the goal are #[Module, Subtype, _uniq.26983, β—Ύ, Subtype, Subtype, _uniq.26983, β—Ύ, β—Ύ, *, *] but we have a lot of instances like docs#LieSubmodule.module' with weak keys like #[Module, *, Subtype, *, β—Ύ, *, *].

Of course, we have no Lie algebra structure in play but it because the keys match Lean then tries to synthesize the instance parameters and unify against a LieSubmodule. The signature is 

{R : Type u} β†’
  {L : Type v} β†’
    {M : Type w} β†’
      [inst : CommRing R] β†’
        [inst_1 : LieRing L] β†’
          [inst_2 : AddCommGroup M] β†’
            [inst_3 : _root_.Module R M] β†’
              [inst_4 : LieRingModule L M] β†’
                (N : LieSubmodule R L M) β†’
                  {S : Type u_1} β†’
                    [inst_5 : Semiring S] β†’
                      [inst_6 : SMul S R] β†’
                        [inst_7 : _root_.Module S M] β†’ [inst_8 : IsScalarTower S R M] β†’ _root_.Module S β†₯↑N

so this takes some time.

There are quite few of these instances of Module on subtypes with weak keys so it adds. Especially because both the arguments to Module are coerced from subtypes.

Kevin Buzzard (Aug 02 2024 at 07:48):

Two quick workarounds: (1) set_option synthInstance.maxHeartbeats 40000 and it works (2) don't import Lie algebras and other things making typeclass inference go off the rails, 

import Mathlib.Topology.Algebra.Valued.ValuedField

open Valued

variable (K : Type*) [Field K] {Ξ“β‚€ : outParam Type*}
    [LinearOrderedCommGroupWithZero Ξ“β‚€] [vK : Valued K Ξ“β‚€]
#synth Semiring π’ͺ[K]
example (n : β„•) : Module π’ͺ[K] (𝓂[K] ^ n : Ideal π’ͺ[K]) := Submodule.module _
-- set_option synthInstance.maxHeartbeats 40000
-- set_option trace.Meta.synthInstance true
-- set_option trace.profiler true
count_heartbeats in -- 15457
example (n : β„•) : Module π’ͺ[K] (𝓂[K] ^ n : Ideal π’ͺ[K]) := by infer_instance
variable (n : β„•) in
#synth Module π’ͺ[K] (𝓂[K] ^ n : Ideal π’ͺ[K]) -- modern way to do the last line

takes under 1/2 as long.

In my opinion the right long-term fix for this is to redefine π’ͺ[K] as a Type not a Subring. I might be saying the same thing as Matt but my understanding of the problem is that because the goal is actually Module β†₯π’ͺ[K] β†₯(𝓂[K] ^ n), Lean is constantly being sidetracked with ideas of the form "ooh we need to prove ClassName β†₯X Y and (X : Subring X') so we could perhaps make progress by finding a term of type ClassName X' Y." This idea is almost always a disaster in the sense that it might take some time to fail because Mathlib is now big, and there are lots of classes.

Rereading Matt's response I think it says the same thing as mine but in a more sophisticated way.

See here for how I designed finite adele rings not as subalgebras but as types, to avoid this kind of problem.

Matthew Ballard (Aug 02 2024 at 14:51):

I haven't finished getting a working version of mathlib (or even a test-passing toolchain) but I suspect that swapping the argument order of Membership.mem as advised by Mario is going to help a good deal here and elsewhere

Matthew Ballard (Aug 03 2024 at 10:33):

With those changes @Yakov Pechersky 's example goes down to under 13000 heartbeats for instance synthesis and 19000 over all.

YaΓ«l Dillies (Aug 03 2024 at 10:35):

Matthew, may I nudge you into contributing some paragraph in blog#86 :pray:

Matthew Ballard (Aug 03 2024 at 10:47):

Mario Carneiro said:

One thing I just noticed is that docs#SetLike.instCoeSortType directly uses a lambda and membership:

instance (priority := 100) : CoeSort A (Type _) :=
  ⟨fun p => { x : B // x ∈ p }⟩

Since this is a coercion, it is unfolded and therefore loads of mathlib terms contain these explicit lambdas. (This also needs a dedicated delaborator, written just below it.) Has anyone tried replacing this with a call to a setToType function? The specific reason I have to believe that this will improve performance across the library is that I can see failed instance searches caused by the fact that the indexing is not able to handle the lambdas: if I have definitions foo, bar : Subgroup G then CommGroup ↑foo also attempts to apply an instance for CommGroup ↑bar. Normally this would not happen because the discrimination tree can tell them apart, but after the aforementioned elaboration the result is CommGroup {x // x ∈ foo} vs CommGroup {x // x ∈ bar} and lean gives up indexing at the lambda.

Does linking to Mario's original message count?

Notification Bot (Aug 03 2024 at 10:47):

A message was moved here from #mathlib4 > Ways to speed up Mathlib by Matthew Ballard.

YaΓ«l Dillies (Aug 03 2024 at 10:50):

Will make do

Matthew Ballard (Aug 03 2024 at 11:07):

My understanding: we have the following values for the keys 

inductive Key where
  | const : Name β†’ Nat β†’ Key
  | fvar  : FVarId β†’ Nat β†’ Key
  | lit   : Literal β†’ Key
  | star  : Key
  | other : Key
  | arrow : Key
  | proj  : Name β†’ Nat β†’ Nat β†’ Key

Currently docs#Lean.Meta.DiscrTree.mkPath sends e.getAppFn to .other for the cases

(Expr.mdata (KVMap.mk _) _)
(Expr.letE _ _ _ _ _)
(Expr.lam _ _ _ _)
(Expr.app _ _)
(Expr.sort _)
(Expr.bvar _)

In particular, anything hiding inside of a .lam is just crunched down to .other. As Mario explained above, with the current ordered of Membership.mem we have a lambda at the head of any coercion of a subtype to sort.

Reversing the order, the head becomes Membership.mem, which being a constant, gets placed into the keys itself and indexing can go deeper to generate more refined keys.

YaΓ«l Dillies (Aug 03 2024 at 11:10):

That non-keying of lambda I had understood, but I had not thought of looking up SetLike.instCoeSortType

Matthew Ballard (Aug 03 2024 at 11:14):

It is a fairly subtle change when just looking at the expression pretty printed. After all, you only see two things get swapped. But if you are better than me at reading off the Expr it is perhaps more obvious.

Matthew Ballard (Aug 03 2024 at 11:24):

In "fixing" mathlib, the worst offender is just the standard docs#Set.CoeSortType. Interestingly if you look at the porting note for it, you see that docs#Set.Elem is introduced to solve a similar indexing problem but for norm_cast. But since it is a essentially an abbrev the indexing for keys just unfolds and marches on.

Matthew Ballard (Aug 04 2024 at 20:59):

Actually, I spent some time on cleaning up my understanding here and I am more confused.

At some point there is a reduction step for the expression where we eta reduce. And it seems like the deBruijn variables themselves are quite important in the eta reduction.

We have a lambda whose body is the application of .bvar 0 after the change. Before it’s more complicated application. But the bound variable doesn’t come from the lambda itself but from the initial .forallE earlier.

Matthew Ballard (Aug 04 2024 at 21:01):

This is the example I still testing on 

βˆ€ {G : Type*} [Group G] {H : Subgroup G}, SMul (β†₯H.op) G

Before

#[SMul, Subtype, MulOpposite, *, β—Ύ, *]

and after

#[SMul, Subtype, MulOpposite, *, Membership.mem, MulOpposite, *, Subgroup, MulOpposite, *, *, *, Subgroup.op, *, *, *, *]

Last updated: May 02 2025 at 03:31 UTC