splitting field discussion @ porting meeting

Stream: mathlib4

[Kevin Buzzard]

I'm just re-watchig the porting meeting video so I can try and understand better what's happening. Here are some questions

1) At some point @Alex J. Best suggests making AdjoinRoot irreducible. I'd know how to do this in mathlib3 but I have no idea how to do it in mathlib4. If I just write @[irreducible] def AdjoinRoot [CommRing R] ... then everything is immediately broken, for example the next declaration

instance instCommRing : CommRing (AdjoinRoot f) :=
  Ideal.Quotient.commRing _

fails with

type mismatch
  Quotient.commRing ?m.1045
has type
  CommRing (?m.1043 ⧸ ?m.1045) : Type u
but is expected to have type
  CommRing (AdjoinRoot f) : Type u

In Lean 3 you could make something irreducible later on but in Lean 4 I think you can't do this. How does one make AdjoinRoot irreducible? Is that even possible? Everyone in the meeting seemed to think that this was not a totally crazy idea so I'm probably missing something.

2) Looking at Algebra.Field.Defs I noticed we have

-- see Note [lower instance priority]
instance (priority := 100) DivisionRing.toDivisionSemiring [DivisionRing α] : DivisionSemiring α :=
  { ‹DivisionRing α›, (inferInstance : Semiring α) with }

Whatever is that about? If I just delete , (inferInstance : Semiring α)then the file still compiles. Surely every field of a division semiring is going to be a field of division ring? Why do we even need that instance?

3) Getting back to the discussion at the porting meeting, we have (in the same file, Algebra.Field.Defs),

class Field (K : Type u) extends CommRing K, DivisionRing K

Did we establish that the slowdowns were due to colliding fields which were not obviously rfl and indeed took a long time to prove they were rfl? Does this mean that our definition of Field should not have so many overlapping fields? It could just extend DivisionRing and any structure with a commutative multiplication, like CommSemigroup or whatever. Is there a chance that this would make life better, or is it litkely to only make things stay the same? I tried making the change and most of mathlib compiles but there was some breakage in RingTheory.TensorProduct which I didn't understand ("error: typeclass instance problem is stuck, it is often due to metavariables" -- I don't really understand that message).

4) I made !4#4507 on the basis that this was my understanding of the conclusions of the meeting. I need to sleep now but it would be interesting to see if this helps with the splitting field PR.

[Eric Wieser]

Surely every field of a division semiring is going to be a field of division ring? Why do we even need that instance?

This wasn't true of Lean3; docs#ring has no mul_zero field

[Eric Wieser]

I think we added one accidentally during ad-hoc porting and never bothered to remove it because it didn't really matter

[Riccardo Brasca]

Do you have a link to the video?

[Eric Wieser]

It could just extend DivisionRing and any structure with a commutative multiplication, like CommSemigroup or whatever. Is there a chance that this would make life better, or is it likely to only make things stay the same?

This won't make any difference. As described in a paper you recently refereed, class Foo extends Bar, Baz means "embed a copy of Bar, copy the fields as needed from Baz". The fields that would be copied are identical in your proposed change.

[Alex J. Best]

My understanding is that you need to use the irreducible_def command https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/IrreducibleDef.html#Lean.Elab.Command.command_Irreducible_def____ . This gives you an irreducible definition and a lemma you can rewrite with to actually unfold the definition when you want to prove things about it (but tactics wont be able to see through the def otherwise).

[Riccardo Brasca]

Riccardo Brasca said:

Do you have a link to the video?

Found.

[Eric Wieser]

Changing the order of DivisionRing and CommRing could easily make a difference, but I'd expect it to make things worse

[Kevin Buzzard]

Eric Wieser said:

Is there a chance that this would make life better, or is it likely to only make things stay the same?

This won't make any difference. As described in a paper you recently refereed, class Foo extends Bar, Baz means "embed a copy of Bar, copy the fields as needed from Baz". The fields that would be copied are identical in your proposed change.

Are you talking about my PR? My understanding is that it makes a much nicer term because Field.mk now no longer eats a comm_ring instance which is constructed from a field instance piecewise, it just eats the comm_ring instance I give it.

[Eric Wieser]

Edited, I didn't quote a long enough part of the top message; I was talking about your third item

[Kevin Buzzard]

I searched for the phrase you quoted, but you also fixed a typo in it so my search failed :-)

[Riccardo Brasca]

I saw the video, thanks for digging into this!

I am not sure I understand the conclusion, should we try to provide the "main parent instance" (meaning the one with embedded copy) explicitly, as you did for toCommRing? It seems something long but definitely doable everywhere in the library.

[Kevin Buzzard]

There are two competing additions on AdjoinRoot f if f is irreducible; one coming from the fact that AdjoinRoot f is always a ring and one coming from the fact that it's a field if f is irreducible. The two definitions are defeq but rfl takes one second to prove this because of...I dunno, because it apparently has to unfold a whole bunch of stuff, and each level of unfolding (equality of CommRing structures, equality of AddCommGroup structures, equality of AddCommMonoid structures, equality of Add structures) takes a quarter of a second, for reasons I still don't fully understand and which seem to be incredibly hard to fix.

So the trick is to make sure that, whenever possible, Lean listens to the "I'm a ring" message before the "I'm a field" message, because most of the additions are coming from "I'm a ring".

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Riccardo Brasca said:

Do you have a link to the video?

Found.

Where?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20porting.20meeting.20series/near/362040095 -- the meetings are recorded every week. I found this one particularly instructional -- I attended the meeting but I watched the entire thing again a day later and learnt more

[Filippo A. E. Nuccio]

Thanks!

[Damiano Testa]

Thanks for the link, Kevin!

[Damiano Testa]

I feel somewhat responsible for these issues: AdjoinRoot was one of the first files that I helped porting. Also, RatFunc is having typeclass issues.

I have not had a chance to watch at the recording yet, but seeing that this is generating some discussion among the experts makes me feel at the same time better and a little worse!

[Eric Wieser]

The issues are not ones introduced during porting, so I don't think you need to feel responsible

[Kevin Buzzard]

yeah, the problems with AdjoinRoot being slow were already there in Lean 3 as I think you are well aware!

[Damiano Testa]

I am aware, but in Lean 3, splitting field still worked... :upside_down:

[Damiano Testa]

Anyway, I never really understand how something works, if it never breaks...

[Kevin Buzzard]

The issue probably is that old_structure_cmd is now not being used (this no longer exists) and we are currently enjoying having to learn about what the consequences of this design decision are.

[Kevin Buzzard]

Eric wrote a paper about it but it's top secret.

[Eric Wieser]

/me should really face the arXiv LaTeX build error gauntlet and get it over with

[Notification Bot]

15 messages were moved from this topic to #general > latex woes by Heather Macbeth.

[Kevin Buzzard]

(thanks Heather!)

Back to the point: I'm trying to make some kind of sense of the slowness of AdjoinRoot and SplittingField. In Lean 3 it was slow and it was just one of those things. In Lean 4 we have better tracing so it's easier to try and debug, although I am now totally confused by what I found.

Here's some code (an instance from the middle of a proof in RingTheory/Adjoin/Field) :

import Mathlib.RingTheory.AdjoinRoot

variable {F K : Type _} [Field F] [Field K] [Algebra F K]
    (s : Set K) (a : K)

set_option maxHeartbeats 300000 in -- necessary
set_option synthInstance.maxHeartbeats 300000 in -- also necessary
set_option trace.Meta.synthInstance true in
set_option profiler true in
set_option trace.Meta.isDefEq true in
example  : Algebra { x // x ∈ Algebra.adjoin F s }
    { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F s } {a} } := by
  infer_instance

-- [Meta.synthInstance] [10.692269s] ✅ Algebra { x // x ∈ Algebra.adjoin F s } { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F s } {a} } ▶

-- -> 3382 lines if unfolded

-- -> 8 occurences of [] [0.792442s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring

set_option trace.profiler true in
example : @CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F s }
  (Subsemiring.toCommSemiring (Algebra.adjoin F s).toSubsemiring)  =
@Ring.toSemiring { x // x ∈ Algebra.adjoin F s } (SubringClass.toRing (Algebra.adjoin F s)) := by
  rfl -- [0.145732s]

The first example takes between 8 and 17 seconds to compile on my machine, depending on what mood it's in. The trace has one line which is taking all the time, and if you unfold it by clicking on the triangle then, after a pause, if VS Code doesn't crash, it turns into 3382 lines of trace; I have uploaded them here. Most of the entries are super-quick, but there are four, all the same, which take over 1 second. Here's one of them, unfolded a little:

[] [1.895163s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain
        { x // x ∈ Algebra.adjoin F s } ▼
    [tryResolve] [1.895058s] ✅ IsDomain { x // x ∈ Algebra.adjoin F s } ≟ IsDomain { x // x ∈ Algebra.adjoin F s } ▼
      [isDefEq] [0.987253s] ✅ IsDomain { x // x ∈ Algebra.adjoin F s } =?= IsDomain { x // x ∈ ?m.11010 } ▼
        [] [0.000256s] ✅ { x // x ∈ Algebra.adjoin F s } =?= { x // x ∈ ?m.11010 } ▶
        [] [0.986885s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring ▶
      [isDefEq] [0.907486s] ✅ ?m.10431 =?= SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing (Algebra.adjoin F s) ▼
        [] ?m.10431 [assignable] =?= SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing
              (Algebra.adjoin F s) [nonassignable]
        [] [0.907405s] ✅ IsDomain { x // x ∈ Algebra.adjoin F s } =?= IsDomain { x // x ∈ Algebra.adjoin F s } ▼
          [] [0.000002s] ✅ { x // x ∈ Algebra.adjoin F s } =?= { x // x ∈ Algebra.adjoin F s }
          [] [0.907329s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring ▶

Each of the (equal) 1.8 seconds problems splits into two equal problems each taking 0.9 seconds, meaning that a sizeable proportion of the 10 seconds is spent solving, 8 times, CommSemiring.toSemiring =?= Ring.toSemiring, and taking about a second each time. But the second example in the code block above shows that rfl solves this really quickly.

Is this sort of behaviour expected? Is the example an unreasonable question for typeclass inference in some way? Note that bypassing typeclass inference by writing

example : Algebra { x // x ∈ Algebra.adjoin F s }
    { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F s } {a} } :=
  Subalgebra.algebra (Algebra.adjoin { x // x ∈ Algebra.adjoin F s } {a})

is 0.1 seconds. So right now I propose hacking some proofs by overriding type class inference and simply telling it the answer. Is this a reasonable path to go down?

Added two weeks later: the example above is misleading. The issue is I think coming from instances higher up the chain which are not visible in the example.

[Riccardo Brasca]

The trace of the second example looks like

[0.214863s] example :
        @CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F s }
            (Subsemiring.toCommSemiring (Algebra.adjoin F s).toSubsemiring) =
          @Ring.toSemiring { x // x ∈ Algebra.adjoin F s } (SubringClass.toRing (Algebra.adjoin F s)) :=
      by rfl ▼
  [step] [0.132841s] expected type: Sort ?u.24838, term
      @CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F s }
          (Subsemiring.toCommSemiring (Algebra.adjoin F s).toSubsemiring) =
        @Ring.toSemiring { x // x ∈ Algebra.adjoin F s } (SubringClass.toRing (Algebra.adjoin F s)) ▼
    [] [0.132825s] expected type: Sort ?u.24838, term
        binrel% Eq✝
          (@CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F s }
            (Subsemiring.toCommSemiring
              (Algebra.adjoin F
                  s).toSubsemiring))(@Ring.toSemiring { x // x ∈ Algebra.adjoin F s }
            (SubringClass.toRing (Algebra.adjoin F s))) ▼
      [] [0.014974s] expected type: <not-available>, term
          @CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F s }
            (Subsemiring.toCommSemiring (Algebra.adjoin F s).toSubsemiring)
      [] [0.117559s] expected type: <not-available>, term
          @Ring.toSemiring { x // x ∈ Algebra.adjoin F s } (SubringClass.toRing (Algebra.adjoin F s)) ▼
        [] [0.114713s] expected type: Ring { x // x ∈ Algebra.adjoin F s }, term
            (SubringClass.toRing (Algebra.adjoin F s)) ▼
          [] [0.114697s] expected type: Ring { x // x ∈ Algebra.adjoin F s }, term
              SubringClass.toRing (Algebra.adjoin F s) ▼
            [Meta.synthInstance] [0.090839s] ✅ SubringClass (Subalgebra F K) K ▶
            [Meta.isDefEq] [0.021623s] ✅ ?m.25433 =?= Subalgebra.instSubringClassSubalgebraToCommSemiringToSemiringInstSetLikeSubalgebra ▶
  [step] [0.035314s] rfl ▶

while in the first one I see

[] [1.089981s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring ▼
          [] [1.089745s] ✅ (Subalgebra.toCommSemiring (Algebra.adjoin F s)).1 =?= (SubringClass.toRing (Algebra.adjoin F s)).1 ▼
            [] [1.089608s] ✅ Semiring.mk (_ : ∀ (a : { x // x ∈ (Algebra.adjoin F s).toSubsemiring }), 1 * a = a)
                  (_ : ∀ (a : { x // x ∈ (Algebra.adjoin F s).toSubsemiring }), a * 1 = a)
                  Semiring.npow =?= Semiring.mk (_ : ∀ (a : { x // x ∈ Algebra.adjoin F s }), 1 * a = a)
                  (_ : ∀ (a : { x // x ∈ Algebra.adjoin F s }), a * 1 = a) Monoid.npow ▼
              [] [0.026117s] ✅ Semiring.npow =?= Monoid.npow ▶
              [] [0.000571s] ✅ { x // x ∈ (Algebra.adjoin F s).toSubsemiring } =?= { x // x ∈ Algebra.adjoin F s } ▶
              [] [0.305916s] ✅ Semiring.toNonUnitalSemiring =?= NonUnitalSemiring.mk
                    (_ : ∀ (a b c : { x // x ∈ Algebra.adjoin F s }), a * b * c = a * (b * c)) ▶
              [] [0.388143s] ✅ Semiring.toOne =?= AddMonoidWithOne.toOne ▶
              [] [0.368348s] ✅ Semiring.toNatCast =?= AddMonoidWithOne.toNatCast ▶

It seems it is taking different paths, right?

[Kevin Buzzard]

I'm very confused about the difference between set_option profiler true and set_option trace.profiler true so I'm not sure if it's taking different paths. Is one output from one option and the other from the other?

[Riccardo Brasca]

Ah, that's possible...

[Eric Rodriguez]

I will note that I did change both of these files reasonably recently, so maybe it's worth looking at the past duffs for solutions. (on mobile, can't find the PRs) I don't remember the changes having a super performance impact in lean3, but maybe it's different now.

[Riccardo Brasca]

The file with the definition of AdjoinRoot is already slow, and I don't think you modified it

[Riccardo Brasca]

It's the base case of the induction that caused all the diamond, so it was probably irrelevant to your problem

[Gabriel Ebner]

Kevin Buzzard said:

I'm very confused about the difference between set_option profiler true and set_option trace.profiler true so I'm not sure if it's taking different paths. Is one output from one option and the other from the other?

This is indeed confusing:

1. set_option profiler true adds timing information to trace messages, but you need to enable the trace messages yourself.
2. set_option trace.profiler true enables all trace messages that take more than 10 milliseconds, and as a bonus also adds the timing information.

[Sebastian Ullrich]

Perhaps we should remove the trace messages behavior of profiler. The reason the two options exist is that profiler gives you a grand total per Lean component (for each declaration and the whole file), while trace.profiler gives you a structured view of the processing of a specific declaration. So they have slightly different purposes.

[Gabriel Ebner]

Perhaps we should remove the trace messages behavior of profiler.

I very much like the behavior you get by enabling profiler. While trace.profiler is great to get a first bearing on the culprit, I find it really hard to see what's going on when the majority of trace messages are missing.

[Gabriel Ebner]

My ideal UI would be one where traces always included timing information, and you could (optional) enable color-coding in the editor where slow parts are highlighted. And for trace.profiler there should be a button to expand the hidden messages.

[Gabriel Ebner]

But in the meantime we should keep profiler.

[Eric Wieser]

Can we put a docstring in profiler that alerts users to the existence of trace.profiler?

[Eric Wieser]

Coming from Lean 3, the muscle memory is profiler but the behavior I actually want is usually trace.profiler

[Gabriel Ebner]

[...] profiler gives you a grand total per Lean component (for each declaration and the whole file), while trace.profiler gives you a structured view of the processing of a specific declaration.

I don't think this helps the confusion. Both options give a structured view, they both have the same output format, they only differ in the way they filter which trace messages to show.

[Sebastian Ullrich]

That is only a happy little side effect of profiler that I added, I think not that long ago? The main task of profiler, going back to Lean 3 or earlier, is producing the "elaboration (of X took) 100ms" messages, it used to have nothing to do with traces. Always including timing in trace nodes (or introducing an opt-out setting for that) would indeed help with making the two options orthogonal again

[Sebastian Ullrich]

You can also set trace.profiler.threshold to 0 :) ... but I assume you might only want to view a specific trace class

[Sebastian Ullrich]

profiler/--profile is also what drives the speedcenter categories

[Gabriel Ebner]

I know that it used be different. But the new behavior is so much more useful. :smile: Introducing a new option for the timing info is obviously fine as well.

[Eric Wieser]

Kevin Buzzard said:

Eric wrote a paper about it but it's top secret.

arxiv#2306.00617 (this version doesn't address reviewer comments on content)