RingTheory.Adjoin.Field is slow

Stream: mathlib4

[Kevin Buzzard]

I was trying to get to the bottom of

set_option maxHeartbeats 950000 in
set_option synthInstance.maxHeartbeats 140000 in
...

in RingTheory.Adjoin.Field. One of the (several) problems in this file is some kind of typeclass unification issue. On this (quite fast) machine I see (in the exact at the end):

 [] [7.158198s] ✅ CommSemiring.toSemiring =?= CommSemiring.toSemiring

in the traces. This is taking 7 seconds and the pattern is the following. First it unfolds a bit, then it explodes:

                      [] [7.158198s] ✅ CommSemiring.toSemiring =?= CommSemiring.toSemiring ▼
                        [] [7.158189s] ✅ CommRing.toCommSemiring.1 =?= CommRing.toCommSemiring.1 ▼
                          [] [7.158163s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
                            [] [7.158157s] ✅ CommRing.toRing.1 =?= CommRing.toRing.1 ▼
                              [] [7.157881s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
                                [] [7.157873s] ✅ (Function.Surjective.ring Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
                                        (_ : Quotient.mk'' 0 = Quotient.mk'' 0) (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (-x) = Quotient.mk'' (-x))
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x - x_1) = Quotient.mk'' (x - x_1))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℕ),
                                            Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℤ),
                                            Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℕ),
                                            Quotient.mk'' (x ^ x_1) = Quotient.mk'' (x ^ x_1))
                                        (_ : ∀ (x : ℕ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)
                                        (_ :
                                          ∀ (x : ℤ),
                                            Quotient.mk'' ↑x =
                                              Quotient.mk''
                                                ↑x)).1 =?= (Function.Surjective.ring Quotient.mk''
                                        (_ : Function.Surjective Quotient.mk'') (_ : Quotient.mk'' 0 = Quotient.mk'' 0)
                                        (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (-x) = Quotient.mk'' (-x))
                                        (_ :
                                          ∀ (x x_1 : { x // x ∈ Algebra.adjoin F ↑s }[X]),
                                            Quotient.mk'' (x - x_1) = Quotient.mk'' (x - x_1))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℕ),
                                            Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℤ),
                                            Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                                        (_ :
                                          ∀ (x : { x // x ∈ Algebra.adjoin F ↑s }[X]) (x_1 : ℕ),
                                            Quotient.mk'' (x ^ x_1) = Quotient.mk'' (x ^ x_1))
                                        (_ : ∀ (x : ℕ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)
                                        (_ : ∀ (x : ℤ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)).1 ▶

And then things calm down a bit and you run into things like

 [] [1.024850s] ✅ Monoid.npow =?= Monoid.npow

and

 [] [3.193706s] ✅ AddMonoidWithOne.toAddMonoid =?= AddMonoidWithOne.toAddMonoid

and

[] [1.133736s] ✅ MulZeroClass.toMul =?= MulZeroClass.toMul

and all of them follow the same pattern -- they unfold a bit and then explode and then calm down and basically it's taking forever.

Is there a trick where something could be made irreducible, or something, to stop this happening?

[Mario Carneiro]

My reading is that there are two ways to prove that whatever type this is is a Ring and they are not obviously defeq

[Mario Carneiro]

probably this is the same issue that came up before, the field structure does not extend the ring structure and so you have to work it down to individual pieces

[Riccardo Brasca]

This instances are about AdjoinRoot, right?

[Kevin Buzzard]

Yes, CommSemiring.toSemiring is actually @CommSemiring.toSemiring (AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)) CommRing.toCommSemiring : Semiring (AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a))(both of them look like this but presumably they're not syntactically equal with pp.all on, unfortunately pp.all is a bit hectic).

Yes, the issue is that these things are defeq but it takes a fast machine 7 seconds to prove this. What do we do about this? That's what I don't understand.

[Reid Barton]

I guess there is some defeq diamond way at the bottom and then Lean has to unfold some fully massive construction applied to this to see that the results are still defeq

[Kevin Buzzard]

So you think there _is_ a diamond?

Mathematically the issue is that $k[x]/(f)$ is always a ring, and it's a field if $f$ is irreducible, but the field structure doesn't extend the ring structure. Maybe this can be fixed?

[Reid Barton]

Well otherwise I suppose Lean would see that the terms are syntactically equal which would not take 7 seconds

[Kevin Buzzard]

Wait -- I thought I had fixed this last week:

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { AdjoinRoot.instCommRing f,
    Quotient.groupWithZero (span {f} : Ideal K[X]) with
    ratCast := fun a => of f (a : K)
    ratCast_mk := fun a b h1 h2 => by
      letI : GroupWithZero (AdjoinRoot f) := Ideal.Quotient.groupWithZero _
      -- porting note: was
      -- `rw [Rat.cast_mk' (K := ℚ), _root_.map_mul, _root_.map_intCast, map_inv₀, map_natCast]`
      convert_to ((Rat.mk' a b h1 h2 : K) : AdjoinRoot f) = ((↑a * (↑b)⁻¹ : K) : AdjoinRoot f)
      . simp only [_root_.map_mul, map_intCast, map_inv₀, map_natCast]
      . simp only [Rat.cast_mk', _root_.map_mul, map_intCast, map_inv₀, map_natCast]
    qsmul := (· • ·)
    qsmul_eq_mul' := fun a x =>
      -- porting note: I gave the explicit motive and changed `rw` to `simp`.
      AdjoinRoot.induction_on (C := fun y => a • y = (of f) a * y) x fun p => by
        simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.rat_smul_eq_C_mul]
  }

[Mario Carneiro]

did it get reverted?

[Mario Carneiro]

IIRC the result of our live debugging session was to use toCommRing := AdjoinRoot.instCommRing f

[Kevin Buzzard]

I think that you still get the same term. I just changed the definition of field locally to

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { Quotient.groupWithZero (span {f} : Ideal K[X]) with
    toCommRing := AdjoinRoot.instCommRing f
    ratCast := fun a => of f (a : K)
...

and we still take forever to solve [] [11.496132s] ✅ CommSemiring.toSemiring =?= CommSemiring.toSemiring . I will try braving pp.all.

[Eric Rodriguez]

it seems that that is taking a different path than through the toCommRing projection :/

[Eric Wieser]

You made the change in !4#4507, and src4#AdjoinRoot.field says it wasn't reverted. You must be looking at old code.

[Eric Wieser]

I suspect that the toCommRing fix you made is the tip of the iceberg; we'll have the same problem in things like docs4#Function.surjective.field too.

[Eric Wieser]

Speculatively, the new-style structures give us a mild performance boost if we use them perfectly, but are a foot-gun in the presence of with notation that pretty much means they get used "incorrectly" every time

[Eric Wieser]

(and are arguably therefore not worth the trouble for algebra, if they're so easy to use incorrectly)

[Jireh Loreaux]

Eric, can you write something up (if you know, I suppose) about how to avoid the foot-gun with with? I understand it's about things being unpackaged and repackaged, but I'm not sure what the correct syntax is to avoid problems.

[Eric Wieser]

The "correct" syntax is to write toBaseOne := _, toBaseTwo := _ for every "preferred" base class that the current structure has

[Eric Wieser]

Of course, the fact that toCommRing is a "preferred" base class but toDivisionRing isn't is silly and non-mathematical

[Eric Wieser]

So to know what the base class is, you can't appear to any mathematical insight and you instead have to #print Field.mk and look at the constructor arguments

[Kevin Buzzard]

So I was indeed looking at old code (failure to understand how git works) but current mathlib master still exhibits the same problem. And pp.all takes my VS code down. Is there an option for just showing instance names explicitly?

[Jireh Loreaux]

Isn't that set_option pp.explicit true?

[Riccardo Brasca]

Kevin Buzzard said:

So you think there _is_ a diamond?

Mathematically the issue is that $k[x]/(f)$ is always a ring, and it's a field if $f$ is irreducible, but the field structure doesn't extend the ring structure. Maybe this can be fixed?

I think the "original sin" is something else. AdjoinRoot is slow even without irreducible f, so without the Field instance.

[Kevin Buzzard]

@Riccardo Brasca I was just looking at the RingTheory.Adjoin.Field file because the
terrifying

set_option maxHeartbeats 950000 in
set_option synthInstance.maxHeartbeats 140000 in

caught my eye and I thought I'd try and understand it. Can you give me an example where something is slow and fields aren't involved?

[Riccardo Brasca]

I don't have access to Lean for about 1 hour, but IIRC declarations around docs4#AdjoinRoot.modByMonicHom are already quite slow. You can maybe have a look at the whole file (the declarations at the end are already slow in Lean3, but less slow).

[Eric Wieser]

I reckon pp.proofs false would make the trace a lot shorter, even with pp.explicit true