Timeout in Submodule (𝓞 K) (𝓞 K)

Stream: mathlib4

[Xavier Roblot]

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]

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]

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]

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

[Andrew Yang]

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

[Yaël Dillies]

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

[Andrew Yang]

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]

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]

Should we make docs#NumberField.ringOfIntegers irreducible?

[Matthew Ballard]

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

[Xavier Roblot]

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)