SubfieldClass slowness

Stream: mathlib4

[Sébastien Gouëzel]

While trying to unbundle normed structure, I have encountered a performance issue which is blocking my progress. This shows up also on current mathlib, with the following mwe:

import Mathlib

class MyFoo (α : Type*) [Ring α] : Prop where

instance ofSubfieldClass {S F : Type*} [SetLike S F] [Field F] [SubfieldClass S F]
    (s : S) : MyFoo s where

lemma soSlow {𝕜 A : Type*} [Ring A] [Field 𝕜]
    [Algebra 𝕜 A] (s : Subalgebra 𝕜 A) : MyFoo s := by
  infer_instance

soSlow fails, of course, because there is no instance for it, but it makes several seconds to do so. I don't really see why, because ofSubfieldClass should not apply: there is no SubfieldClass around, so the assumptions of the instance are not satisfied. Still, Lean goes on trying to see if some weird things are defeq (the culprit being that we have rings, semirings, several possible paths, and with the path taken here things are not obviously defeq of not obviously non-defeq if I understand correctly). Any idea?

[Anne Baanen]

I tried playing around with the definitions and set_synth_order (see code below), without much success. docs#SubfieldClass.toField and docs#Subringclass.toRing both have the fast_instance% elaborator on there, which I thought would prevent this kind of slow structure defeq...

import Mathlib

namespace Lean.Meta

/-- Specify the synthesization order for instances. -/
def Instances.setSynthOrder (declName : Name) (synthOrder : Array Nat) : CoreM Unit := do
  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName |
    throwError "'{declName}' does not have [instance] attribute"
  instanceExtension.add { entry with synthOrder } entry.attrKind

end Lean.Meta

namespace Lean.Elab.Command

open Meta

/-- Specify the synthesization order for instances. -/
elab "set_synth_order " name:ident synthOrder:term : command => do
  let q := Term.MatchExpr.toDoubleQuotedName name
  elabCommand (← `(command| run_meta Instances.setSynthOrder $q $synthOrder))]

[Kevin Buzzard]

Probably everyone reading is well aware of this, but one achilles heel of mathlib does seem to be typeclass inference on subtypes. We had a huge slowdown with rings of integers when they were defined as Subrings but everyone was using them as types; when we changed the definition to be a type directly, things got much better. From mathlib:

/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
-/
def RingOfIntegers : Type _ :=
  integralClosure ℤ K

The type of integralClosure is Subalgebra R A but the trick of making it into a type means that typeclass inference never sees that it's a subtype and this solved a lot of timeout problems in this corner of mathlib. The general issue was that there are many instances in Mathlib of the form Foo S -> Foo (t : Subthing S) but for integer rings it would often be the case that something would be true for the integers but not the field it was the integers of (e.g. searching for actions of the integers on something would suddenly start searching for actions of the full field on the thing, where the action didn't extend).

[Kevin Buzzard]

The chaos starts at

                    [isDefEq] [0.840193] ❌️ MyFoo ↥S =?= MyFoo ↥?m.16 ▼
                      [] [0.840046] ❌️ S.toRing =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
                        [] [0.839921] ❌️ S.toSubring.toRing =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
                          [] [0.839877] ❌️ SubringClass.toRing S.toSubring =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
                            [] [0.839840] ❌️ SubringClass.toRing S.toSubring =?= SubringClass.toRing S ▶

You can kind of see why typeclass inference is confused. The second =?= in the above snippet, namely S.toRing =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing, is a term with holes on the RHS such as ?m.13 : Field A, so the RHS term cannot ever be made metavariable-free and no doubt typeclass inference would fail quickly if asked to fill in this hole. However typeclass inference decides not to worry about this for now, and instead try and figure out SubringClass.toRing S.toSubring =?= SubringClass.toRing S (the last =?= in the snippet, now with no explicit mention of A). This is the sort of typeclass problem that is usually solved very quickly, but unfortunately the RHS now has a Field.toCommRing.toRing term in it still containing this Field A metavariable, which presumably typeclass inference has now got down as "deal with later, let's first check that the multiplications and the zsmuls etc etc agree. Unfold, unfold, unfold, and then finally

           [] [0.016315] ❌️ n • x =?= n • x ▼
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000005] ❌️ Field A ▶
             [synthInstance] [0.000005] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [synthInstance] [0.000004] ❌️ Field A ▶
             [synthInstance] [0.000003] ❌️ Field A ▶
             [] 155 more entries... ▶

Oops!

[Kevin Buzzard]

In total, typeclass inference tries to solve Field A over 1000 times in Sebastien's code, always failing very quickly (at least after the first time), the problem is perhaps that it's postponing asking this question until it has wasted far too much time unfolding the two Ring S instances (the actual time sink), one genuine and one with this unfillable Field A metavariable.

[Kevin Buzzard]

It's a shame that this happens:

        [] [0.880830] ❌️ Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯ =?= Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▼
          [delta] [0.020898] ❌️ Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯ =?= Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▼
            [] [0.020664] ❌️ ZeroMemClass.zero S.toSubring =?= ZeroMemClass.zero S ▼
              [] [0.020574] ❌️ { zero := ⟨0, ⋯⟩ } =?= { zero := ⟨0, ⋯⟩ } ▼
                [] [0.020536] ❌️ ⟨0, ⋯⟩ =?= ⟨0, ⋯⟩ ▼
                  [] [0.020487] ❌️ 0 =?= 0 ▼
                    [delta] [0.020427] ❌️ 0 =?= 0 ▼
                      [] [0.020395] ❌️ Zero.toOfNat0 =?= Zero.toOfNat0 ▼
                        [delta] [0.011125] ❌️ Zero.toOfNat0 =?= Zero.toOfNat0 ▶
                        [synthInstance] [0.000006] ❌️ Field A ▶
              [repeat 50 times]
                        [synthInstance] [0.000006] ❌️ Field A ▶
          [] [0.859734] ❌️ let __src := Function.Injective.addGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
              let __src_1 := Function.Injective.addMonoidWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
              { intCast := Int.cast, toNatCast := __src_1.toNatCast,
                toAddMonoid := __src.toAddMonoid, toOne := __src_1.toOne, natCast_zero := ⋯,
                natCast_succ := ⋯, toNeg := __src.toNeg, toSub := __src.toSub,
                sub_eq_add_neg := ⋯, zsmul := SubNegMonoid.zsmul, zsmul_zero' := ⋯,
                zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, intCast_ofNat := ⋯,
                intCast_negSucc :=
                  ⋯ } =?= let __src :=
                Function.Injective.addGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
              let __src_1 := Function.Injective.addMonoidWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯;
              { intCast := Int.cast, toNatCast := __src_1.toNatCast,
                toAddMonoid := __src.toAddMonoid, toOne := __src_1.toOne, natCast_zero := ⋯,
                natCast_succ := ⋯, toNeg := __src.toNeg, toSub := __src.toSub,
                sub_eq_add_neg := ⋯, zsmul := SubNegMonoid.zsmul, zsmul_zero' := ⋯,
                zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, intCast_ofNat := ⋯,
                intCast_negSucc := ⋯ } ▶

My understanding of this is that it says: "Let's try and prove that two AddGroupWithOne structures on ↥S are defeq, one of which has a (unfillable) hole (?m.13 : Field A). Well, if they're equal, then they'd better have the same zero! Let's unfold a very small amount. Oh wait a minute, the very existence of the zero on the RHS relies on the fact that A is a field! Is it? No! OK so that didn't work, let's go back to the beginning of figuring out if these AddGroupWithOne's are equal, unfold one more step making matters much worse, and then start all over again." The zero failure calculation takes just 0.02 seconds on my machine but unfortunately this is not enough to get Lean to bail, and we ask many more (some much more complex) questions of this nature before finally giving up.

[Yaël Dillies]

Do you remember blog#86 ? I would like to finish it and publish it eventually. Please let me know if some of my past insights are now outdated or if you discover new ones!

[Sébastien Gouëzel]

To me, there are two issues here. The first is that the defeq checking is slow. But the second is that we should never get to this defeq: the instance it's trying to apply has assumptions {S F : Type*} [SetLike S F] [Field F] [SubfieldClass S F]. The SetLike one is satisfied in our context, for Subalgebra 𝕜 A, the Field one is satisfied by 𝕜, but the SubfieldClass S F is not. If Lean tried to synthetize this instance, it would bail out right away, instead of trying to solve an undefined defeq problem (undefined because there's a metavariable in it, which would be coming from the SubfieldClass S F it it could solve it). I know the order in instance synthesis is something of a dark magical art, but here Lean is doing something really weird.

[Kevin Buzzard]

I think there's a minor typo in the above -- it's Field A not Field \k (so this should also fail), but your point remains.

[Sébastien Gouëzel]

You're right, it's Field A. Which is not even true, so it should stop one step earlier than what I wrote!

[Eric Wieser]

Kevin Buzzard said:

It's a shame that this happens:

        [] [0.880830] ❌️ Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯ =?= Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▼
          [delta] [0.020898] ❌️ Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯ =?= Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▼
            ...

Function.Injective.addGroupWithOne should almost never appear in traces; if it does a fast_instance% is missing

[Kevin Buzzard]

I'm afraid I have no idea what fast_instance% is, but (looking at where things start to go wrong) docs#Subalgebra.toRing doesn't have it and the (unrelated to this problem, but similar-looking to my naive eyes) docs#Subfield.toDivisionRing does, so at least that looks to me like an inconsistency.

[Kevin Buzzard]

I have some spare CPU cycles right now (I'm about to spend 2 hours reading email) so can try adding fast_instance% to Subalgebra.toRing and recompiling mathlib to see if this helps, even though I'm happy to admit that I don't really know what I'm doing.

[Kevin Buzzard]

Thanks to whoever wrote #min_imports, that was quick! It's still slow but the trace has changed.

[Eric Wieser]

What's the new trace?

[Kevin Buzzard]

Sorry, I'm lying :-( I had misremembered, we're still faced with exactly the same problem. I'm assuming that Field.toDivisionRing shouldn't be a fast_instance% -- Field extends DivisionRing.

[Kevin Buzzard]

Here's the trace including the bad life choices right down to the suspicious Function.Injective:

 [Meta.synthInstance] [0.858099] 💥️ MyFoo ↥S ▼
   [] [0.000014] new goal MyFoo ↥S ▶
   [] [0.858069] ❌️ apply @ofSubfieldClass to MyFoo ↥S ▼
     [tryResolve] [0.858054] ❌️ MyFoo ↥S ≟ MyFoo ↥?m.16 ▼
       [isDefEq] [0.858051] ❌️ MyFoo ↥S =?= MyFoo ↥?m.16 ▼
         [] [0.857903] ❌️ S.toRing =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
           [] [0.857774] ❌️ S.toSubring.toRing =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
             [] [0.857722] ❌️ SubringClass.toRing S.toSubring =?= (SubfieldClass.toField (Subalgebra 𝕜 A) S).toDivisionRing.toRing ▼
               [] [0.857670] ❌️ SubringClass.toRing S.toSubring =?= SubringClass.toRing S ▼
                 [] [0.857507] ❌️ { toSemiring := SubsemiringClass.toSemiring S.toSubring, toNeg := NegMemClass.neg,
                       toSub := AddSubgroupClass.sub, sub_eq_add_neg := ⋯, zsmul := AddGroupWithOne.zsmul,
                       zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
                       toIntCast := SubringClass.toHasIntCast S.toSubring, intCast_ofNat := ⋯,
                       intCast_negSucc :=
                         ⋯ } =?= { toSemiring := SubsemiringClass.toSemiring S, toNeg := NegMemClass.neg,
                       toSub := AddSubgroupClass.sub, sub_eq_add_neg := ⋯, zsmul := AddGroupWithOne.zsmul,
                       zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯,
                       toIntCast := SubringClass.toHasIntCast S, intCast_ofNat := ⋯, intCast_negSucc := ⋯ } ▼
                   [] [0.857124] ❌️ AddGroupWithOne.zsmul =?= AddGroupWithOne.zsmul ▼
                     [delta] [0.857015] ❌️ AddGroupWithOne.zsmul =?= AddGroupWithOne.zsmul ▼
                       [] [0.856608] ❌️ Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                             ⋯ =?= Function.Injective.addGroupWithOne Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ▶

[Eric Wieser]

src#SubsemiringClass.toSemiring is missing a fast_instance% too

[Eric Wieser]

(as are most of the Subtype.val_injective.foos in that file)

[Kevin Buzzard]

Eric Wieser said:

src#SubsemiringClass.toSemiring is missing a fast_instance% too

Not on master? https://github.com/leanprover-community/mathlib4/blob/582a39f64a00646d46ec665298a21080835e230f/Mathlib/Algebra/Ring/Subsemiring/Defs.lean#L101-L105

[Kevin Buzzard]

Eric Wieser said:

(as are most of the Subtype.val_injective.foos in that file)

If you're talking about Mathlib.Algebra.Ring.Subsemiring.Defs I can't find a single missing fast_instance% in that file.

[Eric Wieser]

Ugh, I'm blind and missed it at the end of the line

[Matthew Ballard]

Ah, I think this was why I dilly-dallied on merging the elaborator. I wanted it to check that an argument was a projection from a class instance that itself could be normalized by fast_instance%.

[Sébastien Gouëzel]

Investigating further, it looks to me that this is an issue with fast_instance% that these Function.injective show up. Just before the instance docs#SubringClass.toRing, an element of a subring class has a $\Z$-action given by docs#AddSubgroupClass.zsmul:

#synth SMul ℤ s -- AddSubgroupClass.zsmul
#print AddSubgroupClass.zsmul -- smul := fun n a ↦ ⟨n • ↑a, ⋯⟩

So, a nice definition without any Function.injective. Then, we define

/-- A subring of a ring inherits a ring structure -/
instance (priority := 75) SubringClass.toRing : Ring s := fast_instance%
  Subtype.coe_injective.ring Subtype.val rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) fun _ => rfl

With #print SubringClass.toRing, you can see the field zsmul inside the structure, and it's given by

@AddGroupWithOne.zsmul (↥s) (Function.Injective.addGroupWithOne Subtype.val ...)

This looks very weird to me because the Subtype.coe_injective constructors are supposed to take all the existing data instances and add proof fields. I definitely don't understand what is going on here, and I don't have the knowledge to open up fast_instance% further...

[Eric Wieser]

I suspect the issue is that docs#AddGroupWithOne.zsmul is not a SMul instance, and so there is no existing instance to populate it with

[Sébastien Gouëzel]

But why should it use docs#AddGroupWithOne.zsmul? The Subtype.coe_injective.ring function uses in its definition the ambient instance, i.e., docs#AddSubgroupClass.zsmul, which is indeed an instance.

[Eric Wieser]

The heuristics of fast_instance% are to replace each parent and/or field (I forget which) with instances that can be synthesized

[Eric Wieser]

This works for toMul, toOne etc, but zsmul doesn't expand to a smaller instance (it's a plain function not an SMul` object) so doesn't participate

[Eric Wieser]

I think this would be fixed by replacing the field with [toZSMul : SMul Int A], but this will surely trip up to_additive

[Sébastien Gouëzel]

But then why does it work for nsmul in docs#AddSubmonoidClass.toAddMonoid? It is defined as

@[to_additive /-- An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure. -/]
instance (priority := 75) toMonoid {M : Type*} [Monoid M] {A : Type*} [SetLike A M]
    [SubmonoidClass A M] (S : A) : Monoid S := fast_instance%
  Subtype.coe_injective.monoid Subtype.val rfl (fun _ _ => rfl) (fun _ _ => rfl)

and the nsmul field inside it is nsmul := fun n x ↦ n • x. I think I'm just confused :-)

[Matthew Ballard]

For the former, it is built with a where/spread by supplying the parent classes. For the latter, it is inlined as a field.

[Sébastien Gouëzel]

Aha. Then it means inlining it as a field should solve the issue in the thread. And indeed it works! If in the definition of Function.Injective.ring I add the explicit field zsmul := fun n x ↦ n • x, then the issue at the start of the thread is solved (instead of 4s, the failure takes 0.09s). Thanks to all for your insights!