Why is `simpNF` complaining here?

Stream: general

[Anne Baanen]

I'm getting a simpNF linter error on #5834:

 /- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.RingTheory.AlgebraicIndependent
Error: ./Mathlib/RingTheory/AlgebraicIndependent.lean:428:1: error: AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply.{u_3, u_2, u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CommMonoidWithZero (Polynomial (MvPolynomial ι R))
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

The statement of docs#AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply doesn't involve Polynomial (MvPolynomial ι R) but I suppose that arises from an attempt at simping?

The thing that I really don't understand is that this search also times out on master:

import Mathlib

noncomputable example {ι : Type u_1} {R : Type u_2}
    {A : Type u_3} {x : ι → A} [CommRing R] [CommRing A] [Algebra R A]
    (hx : AlgebraicIndependent R x) (y : MvPolynomial (Option ι) R) :
    CommMonoidWithZero (Polynomial (MvPolynomial ι R)) := by
  infer_instance

(It requires set_option synthInstance.maxHeartbeats 60000 approximately to not time out.)

[Anne Baanen]

With

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

it looks like applying an IsDomain instance to Polynomial (MvPolynomial ι R) always takes at least half a second of unification:

  [] [0.612743s] ❌ apply @Field.isDomain to IsDomain (Polynomial (MvPolynomial ι R)) ▼
    [tryResolve] [0.612692s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) ≟ IsDomain ?m.7460 ▼
      [isDefEq] [0.612139s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) =?= IsDomain ?m.7460 ▼
        [] [0.000033s] ✅ Polynomial (MvPolynomial ι R) =?= ?m.7460 ▶
        [] [0.611988s] ❌ CommSemiring.toSemiring =?= DivisionSemiring.toSemiring ▶
        [onFailure] [0.000013s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) =?= IsDomain ?m.7460
        [onFailure] [0.000007s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) =?= IsDomain ?m.7460

and #5834 adds a new instance IsDedekindDomain.toIsDomain which adds to the search time. The search was already timing out so that is not a problem, right?

[Anne Baanen]

Maybe I should try merging #5959 and see if that makes things work better?

[Anne Baanen]

Nope, doesn't seem to help. Does anyone want to help debugging this?

[Kevin Buzzard]

#eval Lean.Meta.getInstancePriority? `CommGroupWithZero.toCommMonoidWithZero -- 1000
#eval Lean.Meta.getInstancePriority? `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero -- 1000
#eval Lean.Meta.getInstancePriority? `CancelCommMonoidWithZero.toCommMonoidWithZero -- 1000
#eval Lean.Meta.getInstancePriority? `CommSemiring.toCommMonoidWithZero -- 100 (not 1000)

These instances like LinearOrderedCommMonoidWithZero.toCommMonoidWithZero always apply and should have low priority; however the only time that a priority is lowered is the one instance which you want, so Lean goes on several wild goose chases before finding the right path.

A cheap trick would be

attribute [instance 1001] CommSemiring.toCommMonoidWithZero in
noncomputable example {ι : Type u_1} {R : Type u_2}
    {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] :
    CommMonoidWithZero (Polynomial (MvPolynomial ι R)) := by
  infer_instance

and a perhaps more principled approach would be to globally lower the priority of all those other 1000 instances (perhaps to slightly less than 100 ;-) )

[Anne Baanen]

Didn't this regression in setting priority of extends recently get fixed?

In any case, I'm hesitant to make this change globally, since CommSemiring has a whole bunch of the instance hierarchy above it so it would certainly fail slower in many cases... I'd much prefer to speed up the isDefEq check on IsDomain (Polynomial (MvPolynomial ι R)) =?= IsDomain ?m.7460.

[Kevin Buzzard]

regression fixed: not as far as I know. I was trying to minimise something recently so was looking through a bunch of low-level mathlib files and it seems to me that instance priorities are right now a chaotic mess in places. The example above is a case in point I guess.

Global change: but I only changed it in one example! You say it would fail slower in many cases but I'm not sure I know a single example of a CommMonoidWithZero which isn't also a semiring, so I think priority 1001 is not so unreasonable :-)

More seriously: here is the issue with speeding up the isDefEq check in IsDomain. Here are some of the wild goose chases which Lean goes on:

              [] [0.241757s] ❌ apply @Field.isDomain to IsDomain (Polynomial (MvPolynomial ι R)) ▶
              [] [0.150206s] ❌ apply @DivisionRing.isDomain to IsDomain (Polynomial (MvPolynomial ι R)) ▶
              [] [0.147619s] ❌ apply @LinearOrderedRing.isDomain to IsDomain (Polynomial (MvPolynomial ι R)) ▶
              [] [0.327188s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain
                    (Polynomial (MvPolynomial ι R)) ▶

That's pretty costly, it's a second trying to prove something which is obviously nonsense :-( The first of these unfolds to this:

              [] [0.241757s] ❌ apply @Field.isDomain to IsDomain (Polynomial (MvPolynomial ι R)) ▼
                [tryResolve] [0.241730s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) ≟ IsDomain ?m.14627 ▼
                  [isDefEq] [0.241512s] ❌ IsDomain (Polynomial (MvPolynomial ι R)) =?= IsDomain ?m.14627 ▶

so it kind of looks like an easy problem: all Lean has to do is to set ?m.14627 = Polynomial (MvPolynomial ι R) and we're done. But this won't do because Field.isDomain won't apply of course. However Lean spends ages unfolding the definition of the ring structure on Polynomial (MvPolynomial ι R)) anyway, and because the definition is convoluted we end up with goals like this:

                                                                  [] [0.037176s] ❌ CommRing.toRing.1.1.1.1.1 =?= (Function.Injective.subNegMonoid Polynomial.toFinsupp
                                                                          (_ : Function.Injective Polynomial.toFinsupp)
                                                                          (_ : 0.toFinsupp = 0)
                                                                          (_ :
                                                                            ∀ (a b : Polynomial (MvPolynomial ι R)),
                                                                              (a + b).toFinsupp =
                                                                                a.toFinsupp + b.toFinsupp)
                                                                          (_ :
                                                                            ∀ (a : Polynomial (MvPolynomial ι R)),
                                                                              (-a).toFinsupp = -a.toFinsupp)
                                                                          (_ :
                                                                            ∀ (a b : Polynomial (MvPolynomial ι R)),
                                                                              (a - b).toFinsupp =
                                                                                a.toFinsupp - b.toFinsupp)
                                                                          (_ :
                                                                            ∀ (x : Polynomial (MvPolynomial ι R))
                                                                              (x_1 : ℕ),
                                                                              (x_1 • x).toFinsupp = x_1 • x.toFinsupp)
                                                                          (_ :
                                                                            ∀ (x : Polynomial (MvPolynomial ι R))
                                                                              (x_1 : ℤ),
                                                                              (x_1 • x).toFinsupp =
                                                                                x_1 • x.toFinsupp)).1

[Anne Baanen]

You have convinced me that playing with instance priorities is the right approach! Since IsDomain depends on Semiring it makes no sense to go through all the trouble in the cancellative world when the path is already known.

[Anne Baanen]

I'll make a new PR...

[Anne Baanen]

#6145

[Kevin Buzzard]

Did you see #6011 by the way? The benchmark results were disappointing. Do you understand why? Does something else need fixing?

[Anne Baanen]

Maybe the change in extends order also leads to a change in instance order, and the wrong one is picked first more often?

[Anne Baanen]

Let me check out the class group definition...

[Anne Baanen]

Hmm, my machine seems to disagree with the benchmark, nearly all declarations in your branch's version of ClassGroup.lean are about 10% faster than on the main branch. And one that appeared slower disappeared on rebuild.

[Anne Baanen]

Although the vast majority of build time (over a minute) is taken by docs#ClassGroup.mk0_surjective, probably this means the slowdown is an artifact?

[Anne Baanen]

Aha, looks like the definition of the inverse image in there is being unfolded so much that every equality check thrashes for about a second.

[Anne Baanen]

That specific issue is fixed in #6146, let me now take a look at FreeModule.PID.

[Anne Baanen]

In FreeModule.PID I can't find a real example of the timings getting worse (everything is within about 10% of the master branch) or anything obviously wrong. The huge recursion of docs#Submodule.basis_of_pid_aux is slow but not horribly so. I find it hard to distinguish these outcomes from noise...

[Anne Baanen]

#6145 indeed helps, thanks @Kevin Buzzard!

[Anne Baanen]

Mathlib.Combinatorics.HalesJewett also shows up in this benchmark as slowing down by 30% or so. Let me check what is going on there...

[Anne Baanen]

Very weird: everything takes < 0.02 seconds except for the main theorem, which takes 8.5 seconds on my branch and 9 seconds on the relevant master commit.

[Anne Baanen]

How can I get VelCom to graph the ~Mathlib.Combinatorics.HalesJewett — instructions measure?

[Anne Baanen]

Aha, go to the commit details and click on the line.

[Anne Baanen]

Profiling output on exists_mono_in_high_dimension' is very weird, looks like the elaborator is done in less than a second, linting for unused variables takes 3s(!) and the remainder is gone. Are we hitting a slow path in the kernel?

[Eric Wieser]

Anne Baanen said:

Aha, go to the commit details and click on the line.

How do I get to that page?

[Anne Baanen]

Here's the graph I was looking for: http://speedcenter.informatik.kit.edu/mathlib4/repo-detail/e7b27246-a3e6-496a-b552-ff4b45c7236e?zoomXStart=1687564800000&zoomXEnd=1690502400000&dimensions=~Mathlib.Combinatorics.HalesJewett%3Ainstructions&dayEquidistant=true

[Eric Wieser]

How did you get there? A naive attempt to replace the module name with Mathlib.RingTheory.Kaehler doesn't seem to work for me

[Anne Baanen]

Step by step instructions: go to the benchmark comparison page I linked before, then under the heading "First Run Information" click the name of the commit and you'll go to the commit details page. Under the heading "run result" go to the next page using the arrows on the bottom right until you find the name of the benchmark to compare. Click on that line and you'll go back to the "repo overview" page but with the right things selected.

[Anne Baanen]

I tried URL manipulation too and failed, so not sure how that works...

[Anne Baanen]

Kaehler comparison graph

[Eric Wieser]

Ah, so clicking on the rows only does something when not in the diff view!

[Anne Baanen]

Anne Baanen said:

Profiling output on exists_mono_in_high_dimension' is very weird, looks like the elaborator is done in less than a second, linting for unused variables takes 3s(!) and the remainder is gone. Are we hitting a slow path in the kernel?

I tried splitting out some parts but haven't figured out where the surprising slowdown comes from. Replacing the last lines with sorry makes it finish quickly, but replacing other lines with sorry tends to make the proof break due to unassigned metavariables.

I don't think I can figure out more without knowledge of what is going on, would someone more experienced in combinatorics like to figure out where the slowness is coming from?

[Bhavik Mehta]

Anne Baanen said:

I don't think I can figure out more without knowledge of what is going on, would someone more experienced in combinatorics like to figure out where the slowness is coming from?

I looked at this a little a while back but I don't know enough about how to profile to figure out what's happening. Perhaps together we could figure it out? :D

[Anne Baanen]

Thank you very much for the offer! Unfortunately I will be minimally active here for the coming two weeks at least, but if you're happy to wait a bit more I'd love to come together :D