TC loops

Stream: mathlib4

[Johan Commelin]

I just did a little experiment introducing a TC loop:

chore(Algebra/Group/Action/Defs): make SMulCommClass.symm an instance #23941

This introduces an instance SMulCommClass A B C -> SMulCommClass B A C.
On master, that is a lemma.

The results by bench do not look good. Whereas I would have hoped that this is the sort of loop that is detected almost instantaneously...

[Eric Wieser]

Here's an explanation of why this is expensive:

• We have a graph of instance that derive SMulCommClass A B (F C) from SMulCommClass A B C
• Your new instance effectively creates a copy of this graph with A and B swapped, and adds bidirectional crosslinks between the two graphs
• While the search isn't following loops, the number of non-looping paths has still increased by O(2^graph_depth)

[Johan Commelin]

Ah, thanks!

[Johan Commelin]

I must say that it is quite inconvenient that we can't have this instance :cry:

[Eric Wieser]

Eg, if I want to synthesize SMulCommClass A B (ULift (ULIft X)), previously the path was uniquely:

• SMulCommClass A B C
SMulCommClass A B (ULift X)
SMulCommClass A B (ULift (ULift X))

but now there are lots of paths

• SMulCommClass A B C
SMulCommClass A B (ULift X)
SMulCommClass A B (ULift (ULift X))

• SMulCommClass A B C
SMulCommClass B A C
SMulCommClass B A (ULift X)
SMulCommClass A B (ULift X)
SMulCommClass A B (ULift (ULift X))

• SMulCommClass A B C
SMulCommClass B A C
SMulCommClass B A (ULift X)
SMulCommClass B A (ULift (ULift X))
SMulCommClass A B (ULift (ULift X))

[Eric Wieser]

This probably gets even worse because SMulCommClass is a dependent typeclass, and the instances it is passed are themselves likely to depend on `SMulCommClass.

[Kevin Buzzard]

Example of why this is inconvenient: If we want to do representation theory purely by typeclasses then this means that we need to choose, and to stick to, either [SMulCommClass k G V] or [SMulCommClass G k V].

[Eric Wieser]

Johan Commelin said:

I must say that it is quite inconvenient that we can't have this instance :cry:

Maybe the answer is to consume [SMulCommClass A B C] but declare instance : SymmSMulCommClass A B C, where the latter implies the former in both directions

[Eric Wieser]

This doesn't help with choosing variables though in Kevin's situation

[Eric Wieser]

Johan Commelin said:

I must say that it is quite inconvenient that we can't have this instance :cry:

I think TC search needs native support for "this class is symmetric, so force an arbitrary order on its parameters"

[Eric Wieser]

Or framed another way, SMulCommClass.symm is an "instance_proc" which only fires if B_expr.lt A_expr

[Johan Commelin]

Kevin Buzzard said:

Example of why this is inconvenient: If we want to do representation theory purely by typeclasses then this means that we need to choose, and to stick to, either [SMulCommClass k G V] or [SMulCommClass G k V].

That's exactly the source of my experiment. But (my new design plan for) [Representation k G V] can have instances to both. So the issue isn't very pressing for me right now.

[Kevin Buzzard]

docs#Representation

[Johan Commelin]

See #maths > Representation Theory @ 💬

[Kevin Buzzard]

(comment moved to that thread)

[Yury G. Kudryashov]

I've added some TC loops for topological space properties a while ago (e.g., T0Space X -> RegularSpace X -> T3Space X). Should I try to remove them, fix compile, and !bench to see how much do they hurt performance?

[Kevin Buzzard]

It would be interesting to see!