Zulip Chat Archive

Stream: mathlib4

Topic: typeclass inference and number fields

Kevin Buzzard (Feb 16 2024 at 13:17):

import Mathlib

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

open NumberField

-- fails without bump
set_option synthInstance.maxHeartbeats 80000
#synth MonoidHomClass (β†₯(π“ž K) β†’+* K) (β†₯(π“ž K)) K

Clearly RingHoms are an instance of MonoidHomClass, but Lean doesn't try RingHomClass.toMonoidHomClass until it's given up on several other things. The list it tries (in reverse order) is

      [instances] #[@MulRingSeminormClass.toMonoidHomClass, MulEquivClass.instMonoidHomClass, @MonoidWithZeroHomClass.toMonoidHomClass, @RingHomClass.toMonoidHomClass, @MulSemiringActionHomClass.toMonoidHomClass, @MulCharClass.toMonoidHomClass, @ContinuousMonoidHomClass.toMonoidHomClass]

I was hoping that Yury's #10544 would put paid to this nonsense, but even though we don't have the OrderHoms in this list any more, Lean's algorithm of "try most recently defined instances first" means that it tries looking for ContinuousMonoidHomClass (β†₯(π“ž K) β†’+* K) (β†₯(π“ž K)) K first, and the completely ludicrous #synth TopologicalSpace (π“ž K) (there is no topology anywhere in the question, so this is doomed to failure) takes over 0.2 seconds to fail.

It's hard to point the finger at anything here; Lean just seems to ask a huge number of stupid questions and takes too long to realise that they're stupid. The profiler looks like this:

  [Meta.synthInstance] [2.160795s] βœ… MonoidHomClass (β†₯(π“ž K) β†’+* K) (β†₯(π“ž K)) K β–Ό
    [] [0.011076s] ❌ apply @Subalgebra.normedRing to NormedRing β†₯(π“ž K) β–Ά
    [] [0.017978s] ❌ apply @Subalgebra.normedCommRing to NormedCommRing β†₯(π“ž K) β–Ά
    [] [0.010052s] ❌ apply @Subalgebra.seminormedRing to SeminormedRing β†₯(π“ž K)
    [] [0.023295s] ❌ apply @IntermediateField.toField to Field β†₯(π“ž K) β–Ά
    [] [0.035223s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.019341s] βœ… apply @Subalgebra.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.117823s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.091417s] ❌ apply @DivisionRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.054837s] ❌ apply @LinearOrderedRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.257074s] βœ… apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.138810s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.022135s] ❌ apply Field.henselian to HenselianLocalRing β†₯(π“ž K) β–Ά
    [] [0.022303s] ❌ apply ValuationRing.of_field to ValuationRing β†₯(π“ž K) β–Ά
    [] [0.022662s] ❌ apply ValuationRing.of_field to ValuationRing β†₯(π“ž K) β–Ά
    [] [0.022018s] ❌ apply ValuationRing.of_field to ValuationRing β†₯(π“ž K) β–Ά
    [] [0.058106s] ❌ apply Field.instLocalRingToSemiringToDivisionSemiringToSemifield to LocalRing β†₯(π“ž K) β–Ά
    [] [0.038654s] ❌ apply @EuclideanDomain.to_principal_ideal_domain to IsPrincipalIdealRing β†₯(π“ž K) β–Ά
    [] [0.020477s] ❌ apply DivisionRing.isPrincipalIdealRing to IsPrincipalIdealRing β†₯(π“ž K) β–Ά
    [] [0.010096s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010205s] ❌ apply @LinearOrderedRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.068382s] βœ… apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010016s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain β†₯(π“ž K)
    [] [0.016449s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010516s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.066137s] βœ… apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.016047s] βœ… apply @Subalgebra.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.015671s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.011469s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.011076s] ❌ apply @DivisionRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.016001s] ❌ apply @LinearOrderedRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.012722s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.024936s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010741s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010219s] ❌ apply @DivisionRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010018s] ❌ apply @LinearOrderedRing.isDomain to IsDomain β†₯(π“ž K)
    [] [0.071225s] βœ… apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.035450s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [isDefEq] [0.011253s] βœ… ?m.12709 =?= IsDedekindDomain.toIsDomain β–Ά
    [] [0.011747s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.057460s] βœ… apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain β†₯(π“ž K) β–Ά

I don't know what to do about this issue, but it makes number fields hard to use.

Matthew Ballard (Feb 16 2024 at 13:28):

Does #10617 help?

Kevin Buzzard (Feb 16 2024 at 13:33):

It does! It still times out, but we only need to double once to 40000 (on master we need 50000, on #10617 we only need 30000, so this is definitely a step in the right direction)

Kevin Buzzard (Feb 16 2024 at 13:35):

Furthermore, I see OrderMonoidHomClass.toMonoidHomClass is back in #10617 (the thing Yury removed in the merged-yesterday #10544) so there's a chance that merging master into that branch will actually remove the heartbeat bump completely.

SΓ©bastien GouΓ«zel (Feb 16 2024 at 13:38):

Note that Yury is not done with #10544: he was also planning to separate the algebraic and topological properties of monoids, it just hasn't been done yet, but it should also give you a good gain.

Kevin Buzzard (Feb 16 2024 at 13:38):

On #10617, the profiler says this

  [Meta.synthInstance] [1.127925s] βœ… MonoidHomClass (β†₯(π“ž K) β†’+* K) (β†₯(π“ž K)) K β–Ό
    [] [0.012172s] ❌ apply @Subalgebra.normedCommRing to NormedCommRing β†₯(π“ž K) β–Ά
    [] [0.024413s] ❌ apply @IntermediateField.toField to Field β†₯(π“ž K) β–Ά
    [] [0.016359s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.078029s] ❌ apply @Field.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.079443s] ❌ apply @DivisionRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.052683s] ❌ apply @LinearOrderedRing.isDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.095724s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain β†₯(π“ž K) β–Ά
    [] [0.010863s] ❌ apply Field.henselian to HenselianLocalRing β†₯(π“ž K) β–Ά
    [] [0.010334s] ❌ apply ValuationRing.of_field to ValuationRing β†₯(π“ž K) β–Ά
    [] [0.010595s] ❌ apply ValuationRing.of_field to ValuationRing β†₯(π“ž K) β–Ά
    [] [0.025099s] ❌ apply Field.instLocalRingToSemiringToDivisionSemiringToSemifield to LocalRing β†₯(π“ž K) β–Ά
    [] [0.018363s] ❌ apply @EuclideanDomain.to_principal_ideal_domain to IsPrincipalIdealRing β†₯(π“ž K) β–Ά
    [] [0.019646s] ❌ apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.013119s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά
    [] [0.011887s] βœ… apply @IsDedekindDomain.toIsDomain to IsDomain β†₯(π“ž K) β–Ά

which is a clear improvement (e.g. everything is under 0.1 seconds now) (I suspect that the profiler isn't reporting things < 0.01 second, which is why the list is shorter).

Kevin Buzzard (Feb 16 2024 at 14:50):

BTW @Matthew Ballard re the sorries in #10617 : the problem in ContinuousFunctionalCalculus.lean seems to be a diamond:

example : (Subalgebra.normedRing (elementalStarAlgebra β„‚ a).toSubalgebra) = NormedCommRing.toNormedRing := by
  rfl -- fails

I have a 5 hour train journey ahead of me this evening -- let me know if I can help with this PR.

Matthew Ballard (Feb 16 2024 at 14:51):

Thanks. I have a fix for that. See #lean4 > instance priorities and parents for the underlying issue

Matthew Ballard (Feb 16 2024 at 14:51):

Otherwise, it could definitely use some eyes since it is basically scratch work atm

Jireh Loreaux (Feb 16 2024 at 15:27):

@Matthew Ballard this line from #10617 makes me very happy :heart_eyes:

Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus instructions -31.4%

Kevin Buzzard (Feb 16 2024 at 15:39):

Yeah, Matt brings joy to the community. I remember feeling just the same way (as did Amelia) when his PRs were making group cohomology file instructions go down by 30%.

Matthew Ballard (Feb 16 2024 at 15:44):

Unfortunately that may be because of the sorry’s in that commit :cry:

Ruben Van de Velde (Feb 16 2024 at 15:55):

Fastest proof is no proof :brain:

Matthew Ballard (Feb 16 2024 at 16:24):

Kevin Buzzard said:

BTW Matthew Ballard re the sorries in #10617 : the problem in ContinuousFunctionalCalculus.lean seems to be a diamond:

example : (Subalgebra.normedRing (elementalStarAlgebra β„‚ a).toSubalgebra) = NormedCommRing.toNormedRing := by
  rfl -- fails

I have a 5 hour train journey ahead of me this evening -- let me know if I can help with this PR.

Somewhere the SubringClass instance is the only thing available to build one a NormedRing. Bumping priorities of the added classes built via Subring's does nothing

Matthew Ballard (Feb 16 2024 at 17:42):

Jireh Loreaux said:

Matthew Ballard this line from #10617 makes me very happy :heart_eyes:

Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus instructions -31.4%

It looks like -9% with a working file

Matthew Ballard (Feb 16 2024 at 17:44):

On the example at the start of this topic, after merging master, it is just at the border of 20000 heartbeats. It goes through without the bump but tracing the instance synthesis pushes it over

Kevin Buzzard (Feb 16 2024 at 18:54):

So if Yury makes more changes then we should be back on track :-)

BTW

example : (Subalgebra.normedRing (elementalStarAlgebra β„‚ a).toSubalgebra) = NormedCommRing.toNormedRing := by
  rfl

works on master (on line 78 of Analysis.NormedSpace.Stat.ContinuousFunctionalCalculus)

Patrick Massot (Feb 16 2024 at 19:10):

I don’t understand why you need all this fancy algebra to crash instance synthesis. Look at how a sober example works:

#synth Nonempty (β„•) -- fine
#synth Nonempty (β„• β†’ β„•) -- fine
#synth Nonempty (β„• β†’ β„• β†’ β„•) -- fine
#synth Nonempty (β„• β†’ β„• β†’ β„• β†’ β„•) -- fine
#synth Nonempty (β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„•) -- fine
#synth Nonempty (β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„•) -- fine
#synth Nonempty (β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„• β†’ β„•) -- deterministic time out

Patrick Massot (Feb 16 2024 at 19:12):

Now I’ll stop derailing this thread and open another one.

Matthew Ballard (Feb 16 2024 at 22:34):

Kevin Buzzard said:

BTW

example : (Subalgebra.normedRing (elementalStarAlgebra β„‚ a).toSubalgebra) = NormedCommRing.toNormedRing := by
  rfl

works on master (on line 78 of Analysis.NormedSpace.Stat.ContinuousFunctionalCalculus)

This works on the current version also. Even by with_reducible_and_instances rfl works

Matthew Ballard (Feb 23 2024 at 23:32):

#10617 is ready for review now. About ~2T less instructions.

Riccardo Brasca (Feb 23 2024 at 23:44):

This looks amazing!

Riccardo Brasca (Feb 23 2024 at 23:45):

Should this solve all the various problems with π“ž K once and for all?

Matthew Ballard (Feb 23 2024 at 23:55):

It will help but not completely resolve I think

Last updated: May 02 2025 at 03:31 UTC