type-class inference slow/timing out

Stream: mathlib4

[Kenny Lau]

import Mathlib

#synth AddCommMonoid (ℤ ⧸ Ideal.span ({37} : Set ℤ))

[Kenny Lau]

I think this is due to diamond instance coming from quotient and from addgroup -> Zmod?

[Eric Wieser]

This works:

import Mathlib

set_option synthInstance.maxHeartbeats 32197

#synth AddCommMonoid (ℤ ⧸ Ideal.span ({37} : Set ℤ))

[Eric Wieser]

attribute [-instance] NormedAddCommGroup.toENormedAddCommMonoid also fixes it (docs#NormedAddCommGroup.toENormedAddCommMonoid)

[Floris van Doorn]

Some suspicious instances I found by looking through the trace, which maybe should be scoped:

• docs#Submodule.Quotient.normedAddCommGroup (and docs#Ideal.Quotient.normedCommRing) - might be ok, but this means we need to prove ideal properties by type-class inference to use this. We currently do that before even checking whether M has a seminorm.
• docs#Subsingleton.instComplementedLattice - I think we should scope all instances that assume unique/subsingleton(/finite?) to conclude some algebraic (or topological) class.
• docs#Bundle.instNormedAddCommGroupOfRiemannianBundle seems really bad: it has a variable as its head symbol, and can therefore unify with any function application. In particular, when trying to find NormedAddCommGroup (ℤ ⧸ Ideal.span {37}) it will use E := fun A => ℤ ⧸ A. This should definitely be scoped.

Removing the 4 instances mentioned above reduced the number of heartbeats by 70x, from 20000 to 300.

• docs#ENormedAddCommMonoid.toAddCommMonoid (and friends) are ok I think, but maybe should have lower priority.
• Also, why are docs#IsSimpleModule, docs#IsSemisimpleModule and docs#IsSemisimpleRing abbrevs? Do you really want to apply instances like docs#BooleanAlgebra.toComplementedLattice to try to find an instance?

[Kenny Lau]

(cc @ZhiKai Pong)

[Floris van Doorn]

I think we should make much more classes non-abbrevs: docs#IsArtinian, docs#WellFoundedLT (is docs#isWellOrder_lt now completely useless, since WellFoundedLT is currently an abbrev?), etc.

[Floris van Doorn]

(cc @Sébastien Gouëzel for the bundle instance)

[Junyan Xu]

So we should try to replace abbrev X := Y by class X extends Y, right? I try to do this in #27427 for semisimple modules and I expect I'll need to add a few instances, since previously e.g. IsSimpleModule->IsSemisimpleModule comes from IsSimpleOrder->ComplementedLattice.

[Junyan Xu]

The loss of defeq is annoying, see errors at https://github.com/leanprover-community/mathlib4/actions/runs/16497574869/job/46647016790?pr=27427

[Junyan Xu]

With class X extends Y we still get an instance from X to Y. Is this bad?

[Floris van Doorn]

Junyan Xu said:

The loss of defeq is annoying, see errors at https://github.com/leanprover-community/mathlib4/actions/runs/16497574869/job/46647016790?pr=27427

you can replace t of type ComplementedLattice ... by { t with } and that should work fine (if the type is known(?)), so that is barely any overhead, IMO.

[Floris van Doorn]

Junyan Xu said:

With class X extends Y we still get an instance from X to Y. Is this bad?

That direction is fine. In a semi-simple module it's fine if you use that Submodule is a completed lattice. We block the other direction, because it's rare that you are looking for a semi-simple module instance, and you want to find a generic complemented lattice instance. It is much more likely that you only want to try other semi-simple module instances. (Whenever you want to apply a generic complemented lattice instance to semi-simple modules, then that has to now be added as a separate instance.)

[Floris van Doorn]

I also diagnosed the type-class problem from #lean4 > grind and ordered ring (cc @Heather Macbeth), and identified a few more problematic instances, although the results here are not as clear as they were in the example above.

I do think we should strive for some better instances hygiene in Mathlib.

import Mathlib

set_option trace.Meta.synthInstance true
set_option trace.profiler true

variable {K : Type*} [Field K] {x y z : K}

/- instances that are not great, since they assume something ordered and conclude
something algebraic. It might be annoying to scope them, though... -/
attribute [-instance]
  IsStrictOrderedRing.toCharZero
  instIsAddTorsionFree
  IsStrictOrderedRing.noZeroDivisors
/- probably fine... -/
attribute [-instance]
  Module.instNoZeroSMulDivisorsOfIsDomain
/- concluding something algebraic from something finite(-dimensional).  -/
attribute [-instance]
  Module.instIsReflexiveOfFiniteOfProjective
  Module.free_of_finite_type_torsion_free'
/- these instances all conclude something algebraic from finite/subsingleton,
and should all be scoped, IMO -/
attribute [-instance]
  Subsingleton.to_noZeroDivisors
  Module.Free.of_subsingleton'
  Subsingleton.instComplementedLattice
  isArtinian_of_finite
  AddMonoid.fg_of_finite
  Finite.to_wellQuasiOrderedLE
  Finite.to_wellFoundedLT
  isNoetherian_of_finite
  isNoetherian_of_subsingleton
  Module.Finite.of_finite
  Subsingleton.to_isAddTorsionFree
  Module.FinitePresentation.of_subsingleton
  Module.Free.of_subsingleton
/- not very suspicious, but it's relatively slow by itself,
probably when unifying instances -/
attribute [-instance]
  IsFractionRing.instFaithfulSMul
/- not great together with `Module.IsNoetherian.finite`. -/
attribute [-instance]
  isNoetherian_of_isNoetherianRing_of_finite

#count_heartbeats in
#synth Lean.Grind.NoNatZeroDivisors K

[Junyan Xu]

Do we need some class IsTrivial extends Subsingleton as an algebraic version of Subsingleton?

[Junyan Xu]

The bench result of #27427 is out, overall it speeds things up but there are also some files that get a lot slower.

[Robin Carlier]

Do we have a documentation entry/library note/docstring that explains and document clearly why such instances are "bad/not great"?

[Aaron Liu]

-- see note [lower instance priority] maybe

[Eric Wieser]

Junyan Xu said:

The bench result of #27427 is out, overall it speeds things up but there are also some files that get a lot slower.

I'm not convinced that any benchmarks are trustworthy at the moment; many changes are in files that are earlier than your diff

[Robin Carlier]

Aaron Liu said:

-- see note [lower instance priority] maybe

The note is related but I feel like it's not the full story here.

I think if we're removing or scoping these instances this should come along such a documentation entry so that newcomers/less aware people don't think it's good to turn them back to instances or to make them global.

[Sébastien Gouëzel]

Floris van Doorn said:

docs#Bundle.instNormedAddCommGroupOfRiemannianBundle seems really bad: it has a variable as its head symbol, and can therefore unify with any function application. In particular, when trying to find NormedAddCommGroup (ℤ ⧸ Ideal.span {37}) it will use E := fun A => ℤ ⧸ A. This should definitely be scoped.

Scoped in #27462

[Kim Morrison]

/- these instances all conclude something algebraic from finite/subsingleton,
and should all be scoped, IMO -/

@Floris van Doorn, do you have ideas about where any of these should be scoped to? Subsingleton? Finite?

[Floris van Doorn]

That's how I would scope them, yes. It might be a bit annoying, but I expect that these instances are not used all that frequently(?)

[Eric Wieser]

I think we need them all to be available to the nontriviality tactic

[Kim Morrison]

#27592 looks at

  Subsingleton.to_noZeroDivisors
  Module.Free.of_subsingleton'
  Subsingleton.instComplementedLattice
  isArtinian_of_finite
  AddMonoid.fg_of_finite
  Finite.to_wellQuasiOrderedLE
  Finite.to_wellFoundedLT

either removing them as an instance, or scoping the instance.

[Kim Morrison]

Sadly this only minimally reduces the heartbeats required for variable (K : Type) [Field K] in #synth Lean.Grind.NoNatZeroDivisors K from 18808 down to 18643.

[Kim Morrison]

Eric Wieser said:

I think we need them all to be available to the nontriviality tactic

How does one open a namespace in TacticM?

[Andrew Yang]

Can we have a scope that contains all things that could be instances but cannot due to loops or bad performances or even diamonds and have something like infer_instance! that opens it locally and suggests a scope to open when it is found?

[Heather Macbeth]

It's surprising to me that Grind.NoNatZeroDivisors fails so slowly when IsAddTorsionFree fails so quickly:

import Mathlib

variable {K : Type*} [Field K]

#time -- 944 ms to fail
#synth Lean.Grind.NoNatZeroDivisors K

#time -- 973 ms to fail
#synth NoZeroSMulDivisors ℕ K

#time -- 73 ms to fail
#synth IsAddTorsionFree K

[Heather Macbeth]

They're equivalent to each other under very mild conditions, right?

import Mathlib

example {K : Type*} [AddCommMonoid K] : Lean.Grind.NoNatZeroDivisors K ↔ IsAddTorsionFree K := by
  constructor
  · rintro ⟨h⟩
    constructor
    intro k hk a b
    exact h k a b hk
  · rintro ⟨h⟩
    constructor
    intro k a b hk habk
    exact h hk habk

[Heather Macbeth]

Would it work simply to have only one instance of Lean.Grind.NoNatZeroDivisors, namely from IsAddTorsionFree?

[Jireh Loreaux]

It's worth also considering that, according to the module documentation here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/NoZeroSMulDivisors/Defs.html#NoZeroSMulDivisors, our goal will be to remove NoZeroSMulDivisors in favor of something mathematically correct for semimodules.

[Heather Macbeth]

Does that mean that IsAddTorsionFree K is the "good way"?

[Jireh Loreaux]

I would argue "yes".

[Heather Macbeth]

So maybe the really problematic instance here is docs#instNoNatZeroDivisorsOfNoZeroSMulDivisorsNat :grinning:

[Yaël Dillies]

Jireh Loreaux said:

It's worth also considering that, according to the module documentation here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/NoZeroSMulDivisors/Defs.html#NoZeroSMulDivisors, our goal will be to remove NoZeroSMulDivisors in favor of something mathematically correct for semimodules.

Ahah, I added this docstring three days ago. I am glad it turns out useful already

[Kim Morrison]

Unfortunately replacing docs#instNoNatZeroDivisorsOfNoZeroSMulDivisorsNat with an instance from IsAddTorsionFree K causes a grind failure in LinearAlgebra/RootSystem/Finite/Lemmas

[Yaël Dillies]

Where can I see that failure?

[Kim Morrison]

Let me push a branch.

[Kim Morrison]

#27627

[Kim Morrison]

I think the problem is that CommRing + CharZero doesn't give IsAddTorsionFree.

[Kim Morrison]

perhaps providing that instance will destroy the gains Heather observed above :-(

[Scott Carnahan]

That is strange. You ought to get IsAddTorsionFree from the combination of CharZero and IsDomain.

[Kim Morrison]

Yaël Dillies said:

Where can I see that failure?

@Yaël Dillies, would you be interested in fixing this?

[Kim Morrison]

I added the instance saying a characteristic zero domain has IsAddTorsionFree in #28031. It has no effect on the timings above.

[Kim Morrison]

and #28033 changes the instances for NoNatZeroDivisors to use this. It drastically speeds up the failing synthesis problem

import Mathlib

variable {K : Type*} [Field K] {x : K}
#synth Lean.Grind.NoNatZeroDivisors K

as well as @Heather Macbeth's originally reported problem

example : x ^ 3 * x ^ 42 = x ^ 45 := by grind

[Yaël Dillies]

Kim Morrison said:

Yaël Dillies said:

Where can I see that failure?

Yaël Dillies, would you be interested in fixing this?

Sorry, I am very behind on everything (although things will get better now that I live in one place). If you want me to do something, please somehow land a notification in my inbox (eg by creating an issue and assigning me to it)