set_option maxSynthPendingDepth 2

Stream: mathlib4

[Sébastien Gouëzel]

Currently, a few places in mathlib need set_option maxSynthPendingDepth 2 in (otherwise, some instances are not found). Some time ago, there was a discussion whether it could be worth it setting this as a global setting in mathlib, if the performance penalty is not too bad. Does someone know how I could test this change over all mathlib?

[Sébastien Gouëzel]

(I mention this because #20691 removes an ad hoc instance, at the price of adding this incantation at three places. I think it's good, but it would be even better if the incantation was not needed at all...)

[Kyle Miller]

Do we know which instance synthesis problems this option is helping with specifically?

[Sébastien Gouëzel]

I think it's always related to putting norms on spaces of continuous linear maps or continuous multilinear maps.

[Kim Morrison]

You can put this option in the lakefile and then rebuild.

[Kim Morrison]

I tried this at some point, and from memory there were failures, so I didn't even get to the point of measuring performance.

[Kyle Miller]

One reason I'm wondering is that when I added the feature where all parent classes yield instances (it used to be only a subset of them), some tests contributed by Kevin Buzzard stopped needing a higher maxSynthPendingDepth.

Currently Mathlib's parent class orders are not consistent. Potentially, if we take more care with making sure parent classes are in consistent orders, we might stop seeing failures. I don't have any theory to support this though. It would just be nice if somehow more tweaks to class parent handling would magically have a positive effect.

[Sébastien Gouëzel]

I'm currently testing, in #21887. For now, I've seen one failure (where simp became more powerful, applying a lemma it could not apply before), and issues in the infamous JacobiZariski (where I had to unfold the definition of delta to help Lean -- why is this monstrous definition not an irreducible_def, by the way?)

[Sébastien Gouëzel]

Everything builds, with minor changes. Instructions count goes up by 0.24%, some files get worse, some files get better. Given that this removes a weird behavior, which is hard to understand or debug when it creates problems, I think we should merge this unless someone has a better solution.

[Eric Wieser]

I think it's going to be confusing having the web editor with a different value for this setting than mathlib

[Eric Wieser]

Should we push for the default in core to change at the same time?

[Sébastien Gouëzel]

I agree it would be better to have the same change in core, but I'm not sure it would be welcome (@Kim Morrison , what do you think?). Otherwise, it would be just like autoimplicits. Is there a way to make the web editor pick up mathlib settings?

[Eric Wieser]

We can edit the "mathlib" web editor settings at https://github.com/leanprover-community/lean4web/blob/main/Projects/mathlib-demo/lakefile.toml

[Eric Wieser]

But remember that "mathlib" is the default setting for the web editor, so I'm not sure changes there would be welcome either.

[Kim Morrison]

Yes, if Mathlib is happy, I'm happy to change the default in core.

[Sébastien Gouëzel]

I've done some experiments with other values for maxSynthPending, as recommended by @Matthew Ballard, and the result is interesting: for small values like 3 or 5, everything works just like for 2. But for a large value (I tried 50), I get just 3 failures throughout mathlib (see #22035). I wonder if these failures are the symptom of bad instances somewhere, but I can't find the trace settings to investigate what is going on (and I don't really understand what pending instances are).

[Kevin Buzzard]

We're at the triage meeting and have been sidetracked by this issue because it comes up in #20691 . The reason that setting the pending depth to 50 causes a random timeout in RingTheory.Valuation.ValuationSubring is that typeclass inference gets into some kind of nested loop, where it wants to prove decidability of x1 ≤ x2 in a linear order but in order to do this it needs to prove decidability of x1 ≤ x2 and if the pending depth is large then it just keeps going. As the pending depth increases, the time taken to process the instance le_total_ideal takes longer and longer, and for pending depth over 28 this leads to a timeout. Here's the trace for the loop:

[] [0.863126] ✅️ apply @instDecidableLe_mathlib to DecidableRel fun x1 x2 ↦ x1 ≤ x2 ▼
[tryResolve] [0.862980] ✅️ Decidable ((fun x1 x2 ↦ x1 ≤ x2) a b) ≟ Decidable (a ≤ b) ▼
[isDefEq] [0.862380] ✅️ Decidable ((fun x1 x2 ↦ x1 ≤ x2) a b) =?= Decidable (?m.114929 a b ≤ ?m.114930 a b) ▼
[] [0.862364] ✅️ (fun x1 x2 ↦ x1 ≤ x2) a b =?= ?m.114929 a b ≤ ?m.114930 a b ▼
[] [0.862355] ✅️ a ≤ b =?= ?m.114929 a b ≤ ?m.114930 a b ▼
[synthInstance] [0.861936] ✅️ Ideal ↥A → Ideal ↥A → LinearOrder (Ideal ↥A) ▼
[] [0.000062] new goal Ideal ↥A → Ideal ↥A → LinearOrder (Ideal ↥A) ▶
[] [0.001501] ✅️ apply ValuationRing.instLinearOrderIdealOfDecidableRelLe to Ideal ↥A → Ideal ↥A → LinearOrder (Ideal ↥A) ▶
[] [0.000324] ✅️ apply @ValuationRing.toPreValuationRing to PreValuationRing ↥A ▶
[] [0.010446] ✅️ apply @instValuationRingSubtypeMem to ValuationRing ↥A ▶
[resume] [0.000017] propagating ValuationRing ↥A to subgoal ValuationRing ↥A of PreValuationRing ↥A ▶
[resume] [0.000079] propagating PreValuationRing ↥A to subgoal PreValuationRing ↥A of Ideal ↥A → Ideal ↥A → LinearOrder (Ideal ↥A) ▶
[resume] [0.000184] propagating Ideal ↥A → Ideal ↥A → PreValuationRing ↥A to subgoal Ideal ↥A → Ideal ↥A → PreValuationRing ↥A of Ideal ↥A → Ideal ↥A → LinearOrder (Ideal ↥A) ▶
[] [0.000953] ❌️ apply @Ord.instDecidableRelLe to DecidableRel fun x1 x2 ↦ x1 ≤ x2 ▶
[] [0.000799] ❌️ apply @instDecidableRelLe to DecidableRel fun x1 x2 ↦ x1 ≤ x2 ▶
[] [0.823767] ✅️ apply @instDecidableLe_mathlib to DecidableRel fun x1 x2 ↦ x1 ≤ x2 ▼

(and away we go again)

[Kevin Buzzard]

Mathematically Lean wants to know why ideals in a valuation subring are linearly ordered (this is true mathematically) and it runs into this in mathlib:

instance [DecidableRel ((· ≤ ·) : Ideal A → Ideal A → Prop)] : LinearOrder (Ideal A) :=
  have := decidableEqOfDecidableLE (α := Ideal A)
  have := decidableLTOfDecidableLE (α := Ideal A)
  Lattice.toLinearOrder (Ideal A)

and it's the decidability which seems to throw it into a loop.

[Sébastien Gouëzel]

Why is that a have and not a let?

[Kevin Buzzard]

That's an interesting question!

Another question which I've never been clear about is: why do we have all this decidable stuff in the definition of a linear order anyway?

[Edward van de Meent]

in words (and abstracting a bit), the loop is "I need to find DecidableRel (. <= .) for some type A. this means, for any I and J, i need to be able to decide I <= J. I can do that if there is LinearOrder A. There is an instance saying that there is LinearOrder A if there is DecidableRel (. <= .)" This is a non-trivial loop, because for every loop, the context grows by two variables, namely I and J.

[Kevin Buzzard]

Unfortunately changing the haves to letIs doesn't stop the timeout at pending depth 50. Isn't this a loop in the typeclass system? If decidableRel ≤ then LinearOrder, but if LinearOrder then decidableRel ≤ (i.e. what Edward said)

[Sébastien Gouëzel]

Why not go fully classical here, and just have

instance : LinearOrder (Ideal A) := by
  classical
  exact Lattice.toLinearOrder (Ideal A)

[Chris Wong]

Kevin Buzzard said:

That's an interesting question!

Another question which I've never been clear about is: why do we have all this decidable stuff in the definition of a linear order anyway?

I think it's because Ord.compare would imply that they are decidable anyway?

[Sébastien Gouëzel]

I see that many lemmas throughout mathlib assume [DecidableEq (Ideal T)]. If there are some concrete implementations of this decidability for specific rings, then my suggestion above to go fully classical is bad, as it will create diamonds. If this is never used to compute, though, maybe we could even register a global instance DecidableEq (Ideal T) as the classical instance, and then there would be no diamond as the two instances would agree (they would both be the classical one).

[Kevin Buzzard]

The second failure in #22035 is of a completely different nature. Letting the pending depth be huge allows Lean to do the following thing:

                    [Meta.isDefEq] [0.011209] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact ⇑(LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f)))
                          ⇑(LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g))) ▶
                    [Meta.isDefEq] [0.016898] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f))))
                          ⇑(LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g)))) ▶
                    [Meta.isDefEq] [0.023949] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f)))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g))))) ▶
                    [Meta.isDefEq] [0.032511] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f))))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g)))))) ▶
                    [Meta.isDefEq] [0.042677] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f)))))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g))))))) ▶
                    [Meta.isDefEq] [0.054752] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f))))))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g)))))))) ▶
                    [Meta.isDefEq] [0.067871] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M
                                        (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f)))))))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M
                                        (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g))))))))) ▶
                    [Meta.isDefEq] [0.083441] ✅️ Function.Exact ⇑?l12
                          ⇑?l23 =?= Function.Exact
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M
                                        (LinearMap.rTensor M
                                          (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M f))))))))))
                          ⇑(LinearMap.rTensor M
                              (LinearMap.rTensor M
                                (LinearMap.rTensor M
                                  (LinearMap.rTensor M
                                    (LinearMap.rTensor M
                                      (LinearMap.rTensor M
                                        (LinearMap.rTensor M
                                          (LinearMap.rTensor M (LinearMap.rTensor M (LinearMap.rTensor M g)))))))))) ▶
...

and this seems to stop only when we get to the pending depth, whereupon Lean bails and then has to prove

  AddCommGroup
    (((((((((((((((((((((N ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R] M) ⊗[R]
                        M) ⊗[R]
                      M) ⊗[R]
                    M) ⊗[R]
                  M) ⊗[R]
                M) ⊗[R]
              M) ⊗[R]
            M) ⊗[R]
          M) ⊗[R]
        M) ⊗[R]
      M)

[Kevin Buzzard]

So this second timeout is caused by aesop trying to solve the following goal

R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
iff_exact : ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)} [inst_2 : AddCommGroup N2]
  [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3] [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2)
  (l23 : N2 →ₗ[R] N3), Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
⊢ ∀ ⦃N N' N'' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
  [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
  Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)

and trying to use iff_exact (in the "forward direction", i.e. "make the goal more complicated") to solve the goal.

[Kevin Buzzard]

this is docs#Module.FaithfullyFlat.iff_exact_iff_rTensor_exact in RingTheory/Flat/FaithfullyFlat/Basic.lean

Basically if MaxSynthPendingDepth is 50 then Lean will keep tensoring with M 50 times, it seems.

[Kevin Buzzard]

Sébastien Gouëzel said:

Why not go fully classical here, and just have

instance : LinearOrder (Ideal A) := by
  classical
  exact Lattice.toLinearOrder (Ideal A)

This change in the instance fixes the synthpendingdepth problem: the proof now compiles instantly even on depth 50. I'll open a new discussion for the decidable equality on ideals issue so it doesn't derail this one. (edit: discussion here )

[Sébastien Gouëzel]

As a middle ground, I think setting maxSynthPendingDepth = 3 looks reasonable: it avoids the above monstrosities, but it's large enough for all mathematics we have already seen in mathlib (in fact, 2 would be enough) and should be future-proof tanks to the little margin (3 instead of 2). This is done in #22012.

[Johan Commelin]

Should the default value be changed in core instead? I think @Kim Morrison indicated something along those lines...

[Matthew Ballard]

Understanding these things would be much easier if there was a report on the changes to particular instance synthesis problems to complement the existing benchmarking.

A low tech way would be to make a big file/folder with a curated list of problems

[Sébastien Gouëzel]

Yes, @Kim Morrison said core would be ok with changing the value there. But if we change it first in mathlib, it will simplify a bit the core/mathlib dance, I think.

[Matthew Ballard]

I think if you want a core change you will have to build on of nightly_testing.

[Matthew Ballard]

Kevin Buzzard said:

So this second timeout is caused by aesop

Why is aesop being used here to begin with? Replacing with

fun _ _ _ => iff_exact ..|>.1

seems ok.

[Matthew Ballard]

docs#instIsCommutativeOfIsCyclicSubtypeMemSubgroup and docs#IsSimpleGroup.isCyclic are a similarly problematic pair when trying synthesize a commutative group structure on a subgroup.

[Eric Wieser]

Kevin Buzzard said:

That's an interesting question!

Another question which I've never been clear about is: why do we have all this decidable stuff in the definition of a linear order anyway?

Long ago we had separate linear_order and decidable_linear_order type classes, but the distinction was considered unhelpful so they were merged.

[Kim Morrison]

Can we just make LinearOrder fully classical?!

[Violeta Hernández]

What would be the new way to spell out a linear order with decidable ordering? That's something I care about in e.g. my ordinal notations project

[Kevin Buzzard]

I guess we have to understand whether "fully classical" means "just drop the DecidableLE and DecidableEq fields" (which was how I interpreted it) or "drop the fields and then furthermore globally inhabit them with classical instances" (which sounds like a bad idea because I should think that there are plenty of constructive instances of <= in mathlib). Going fully classical by just dropping the fields might mean throwing in a bunch of DecidableLE assumptions throughout mathlib but we already have this with e.g. finsets.

[Matthew Ballard]

#22326 removes the problematic aesop call.

[Matthew Ballard]

Bumping the question: do we have a design proposal for un-deciding LinearOrder?

[Eric Wieser]

Here's the original proposal that led to the status quo

[Eric Wieser]

Personally I think the status quo is fine

[Matthew Ballard]

Thanks for the link Eric. It appears one interpretation of the proposal above also came up then: just remove the Decidable fields.

[Sébastien Gouëzel]

Back to the maxSynthPendingDepth question, should we merge #22012 (which sets it to 3) now, or wait until it's done in core first? @Kim Morrison

[Kim Morrison]

Are we happy with the slow-down this produces?

[Kim Morrison]

If so, then yes, let's merge this first.

[Jireh Loreaux]

I think the slowdown is worth the lack of headache. There have been a number of times where I've been beating my head against a wall trying to figure out why something doesn't work, only to finally figure out I needed to increase the synthPendingDepth. I know @Frédéric Dupuis has also experienced this.

[Eric Wieser]

Will this be in the next Lean release, or do we need to wait a month? If the later, I think we should change the default in the web editor as well

[Kim Morrison]

Probably not. We're hoping to cut v4.18.0-rc1 from the nightly that comes out in about 6 hours.

[Kim Morrison]

We've decided not to change the default until we have a minimisation of a realistic appearance of the need for maxSynthPendingDepth 2 from Mathlib, that we can install in the test suite. Currently the only test is https://github.com/leanprover/lean4/blob/master/tests/lean/run/3313.lean, which no longer requires maxSynthPendingDepth at all.

I won't have time to prepare this minimisation in the short-term, but if anyone would like to that would be super helpful!