RingTheory.Polynomial.Quotient !4#3292

Stream: mathlib4

[Scott Morrison]

I've been having a look at RingTheory.Polynomial.Quotient !4#3292, which has a pretty nasty timeout issue.

I've annotated the declaration where things go wrong in the branch, if anyone would like to play with it.

[Scott Morrison]

The trace from isDefEq looks like:

-- [Meta.isDefEq] [4.966044s] 💥 (R[X] ⧸ RingHom.ker ↑(Polynomial.aeval x)) ≃ₐ[R] R =?= (R[X] ⧸ RingHom.ker ↑(Polynomial.aeval x)) ≃ₐ[R] R ▼
--   [] [0.000001s] ✅ R =?= R
--   [] [0.527869s] ✅ R[X] ⧸ RingHom.ker ↑(Polynomial.aeval x) =?= R[X] ⧸ RingHom.ker ↑(Polynomial.aeval x) ▶
--   [] [0.000001s] ✅ R =?= R
--   [] [0.000000s] ✅ CommRing.toCommSemiring =?= CommRing.toCommSemiring
--   [] [4.437865s] 💥 Ring.toSemiring =?= Ring.toSemiring ▼
--     [] [4.437795s] 💥 CommRing.toRing.1 =?= CommRing.toRing.1 ▼
--       [] [4.437271s] 💥 Ring.toSemiring =?= Ring.toSemiring ▼
--         [] [4.437137s] 💥 (Function.Surjective.ring Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
--                 (_ : Quotient.mk'' 0 = Quotient.mk'' 0) (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 + x_2) = Quotient.mk'' (x_1 + x_2))
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 * x_2) = Quotient.mk'' (x_1 * x_2))
--                 (_ : ∀ (x_1 : R[X]), Quotient.mk'' (-x_1) = Quotient.mk'' (-x_1))
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 - x_2) = Quotient.mk'' (x_1 - x_2))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℕ), Quotient.mk'' (x_2 • x_1) = Quotient.mk'' (x_2 • x_1))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℤ), Quotient.mk'' (x_2 • x_1) = Quotient.mk'' (x_2 • x_1))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℕ), Quotient.mk'' (x_1 ^ x_2) = Quotient.mk'' (x_1 ^ x_2))
--                 (_ : ∀ (x_1 : ℕ), Quotient.mk'' ↑x_1 = Quotient.mk'' ↑x_1)
--                 (_ :
--                   ∀ (x_1 : ℤ),
--                     Quotient.mk'' ↑x_1 =
--                       Quotient.mk''
--                         ↑x_1)).1 =?= (Function.Surjective.ring Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
--                 (_ : Quotient.mk'' 0 = Quotient.mk'' 0) (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 + x_2) = Quotient.mk'' (x_1 + x_2))
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 * x_2) = Quotient.mk'' (x_1 * x_2))
--                 (_ : ∀ (x_1 : R[X]), Quotient.mk'' (-x_1) = Quotient.mk'' (-x_1))
--                 (_ : ∀ (x_1 x_2 : R[X]), Quotient.mk'' (x_1 - x_2) = Quotient.mk'' (x_1 - x_2))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℕ), Quotient.mk'' (x_2 • x_1) = Quotient.mk'' (x_2 • x_1))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℤ), Quotient.mk'' (x_2 • x_1) = Quotient.mk'' (x_2 • x_1))
--                 (_ : ∀ (x_1 : R[X]) (x_2 : ℕ), Quotient.mk'' (x_1 ^ x_2) = Quotient.mk'' (x_1 ^ x_2))
--                 (_ : ∀ (x_1 : ℕ), Quotient.mk'' ↑x_1 = Quotient.mk'' ↑x_1)
--                 (_ : ∀ (x_1 : ℤ), Quotient.mk'' ↑x_1 = Quotient.mk'' ↑x_1)).1 ▼
--           [] [4.436647s] 💥 Semiring.mk
--                 (_ : ∀ (a : RingCon.Quotient (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x)))), 1 * a = a)
--                 (_ : ∀ (a : RingCon.Quotient (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x)))), a * 1 = a)
--                 Monoid.npow =?= Semiring.mk
--                 (_ : ∀ (a : RingCon.Quotient (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x)))), 1 * a = a)
--                 (_ : ∀ (a : RingCon.Quotient (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x)))), a * 1 = a)
--                 Monoid.npow ▼
--             [] [2.271145s] ✅ Monoid.one_mul =?= Monoid.one_mul ▶
--             [] [1.918150s] ✅ Monoid.mul_one =?= Monoid.mul_one ▶
--             [] [0.247062s] 💥 Function.Surjective.ring.proof_2 Quotient.mk''
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_1
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_2
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_3
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_4
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_6
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_7
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_8
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_9
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_11
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_12
--                     (Ideal.Quotient.ringCon
--                       (RingHom.ker
--                         ↑(Polynomial.aeval
--                             x)))) =?= Function.Surjective.ring.proof_2 Quotient.mk''
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_1
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_2
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_3
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_4
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_6
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_7
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_8
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_9
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_11
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x))))
--                   (RingCon.instCommRingQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToMul.proof_12
--                     (Ideal.Quotient.ringCon (RingHom.ker ↑(Polynomial.aeval x)))) ▶

[Scott Morrison]

This is the scenario we've discussed several times in the last few days, where all the time is going into checking defeq of fields which would ideally just be by proof irrelevance once isDefEq has checked the data.

[Scott Morrison]

As you can see in the trace RingCon is particularly nasty for this. I'm not sure if there's something to be done with RingCon that would improve this situation?

[Eric Wieser]

Are the LHS and RHS syntactically identical there?

[Kevin Buzzard]

I have the file open but with pp.all set to true it's extremely painful to do anything at all.

[Kevin Buzzard]

Huh. I added pp.all, ran lake build on the command line, caught all the output in a 1 gigabyte file and searched for [Meta.isDefEq] [n where that last n is anything from 0 to 9, and all the 135487 lines of output had n=0 shrug

[Kevin Buzzard]

Maybe lake build > crap34 2>&1 doesn't capture all the debugging output? There are only four Quotient.mk''s in my 1 gig file, and there are more than that in Scott's code above.

[Kevin Buzzard]

ok so switching pp.all off I kept digging through the failure of the "they're obviously the same" proof and it randomly peters out with

[0.000050s] 💥 0 + a =?= 0 + a

:shrug:

[Kevin Buzzard]

Both 0s are @OfNat.ofNat R[X] 0 Zero.toOfNat0 : R[X], I have no idea why this is failing. Note that we are deep in some recursive argument here, there are 58 spaces before the [] [0.000050s].

[Eric Wieser]

Are the R[X]s on both sides the same?

[Kevin Buzzard]

It's really difficult to answer this. If you put pp.all on then there's too much trace argument to be manageable (there's at least a gig of text). I'm just unfolding what Scott posted, but just above the exploding 0 + a = a =?= 0 + a = a is a ticked R[X] =?= R[X] so I think they are the same.

[Kevin Buzzard]

Yeah they all seem to be @Polynomial R CommSemiring.toSemiring : Type ?u.107654

[Ruben Van de Velde]

Is the failure mode "running out of heartbeats"? What happens if you give it some more?

[Eric Wieser]

Kevin Buzzard said:

Yeah they all seem to be @Polynomial R CommSemiring.toSemiring : Type ?u.107654

Is it stuck looking for a universe variable?

[Kevin Buzzard]

I doubt it because they were all the same universe metavariable. The fact that lean thinks it needs 100,000 universe metavariables is perhaps also of some concern

[Eric Wieser]

I'm finding some very weird behavior in this PR:

image.png

The squiggle on #exit is in completely the wrong place!

[Kevin Buzzard]

If I just fire up the PR then the red squiggle is in the right place for me, but I've seen situations in the past where if you play around with the code for a bit then things can get completely confused and you have to restart Lean 4 to fix it