Coercions and simp-normal form

Stream: mathlib4

[David Loeffler]

Short question: when there are multiple "paths" to coerce a complicated object into a simpler one, how should one go about determining which is preferred either by coe or by simp?

I've hit this issue working with equivalences of algebras over a ring. If A, B are two algebras over R, then we can form the type A ≃ₐ[R] B of R-algebra equivs. I want to take one of these, and regard it as an R-linear map (forgetting the ring structure and the bijectivity).

Mathematically this is completely straightforward: one class of maps is trivially a subset of the other. In Mathlib, however, to get from the bundled algebra-equiv type A ≃ₐ[R] B to the bundled linear-map type A →ₗ[R] B, there are many ways of walking through the type hierarchy (I found at least five). Confusingly, which one gets picked for the (↑) coercion depends on which subset of mathlib you're importing, since maps defined in later files seem to take priority over earlier ones; if you import the whole of mathlib, then it takes you on a rather unexpected detour via LieHom.

The problem is that while all these are defeq, they are not reducibly defeq, so simpdoesn't recognise them as being the same, and we need to add simp lemmas (proved by rfl) to tell it so. However, I tried to do this and got into an awful muddle trying to assign a direction to the lemmas! Ideally we'd want to do this in such a way that all paths through the digraph of types from A ≃ₐ[R] B to A →ₗ[R] B get simp-ed to a unique preferred simp-normal form. However, my head started to spin trying to do this in a "minimal" way without creating infinite simp loops; and there seems to be no way to guarantee that the simp-normal path is also the one that's picked up by the coercion framework.

Surely there must be a better way?

[Eric Wieser]

I think this is made worse by the fact that in some places were have three coercions for such diamonds; e.toLinearEquiv.toLinearMap, e.toAlgHom.toLinearMap, and something like LinearMapClass.mk e.

[Eric Wieser]

I think consensus is forming that we should drop the last one

[Eric Wieser]

I hadn't considered until now that the problem of deciding which way to flip these diamonds in simp lemmas cannot be solved by a totally arbitrary choice; indeed if you have a cube of conversions (with arrows forgetting continuity, inverses, and multiplicative properties), then misconfiguration of simp lemmas that flip each face could send your three-edge path in a cyclic walk around the cube.

[Kevin Buzzard]

Maybe the choice should be an ordering of the forgettable things, and then you could simp to put the forgettings in the right order. Example: to get from a continuous AlgEquiv to a linear map you really do need to forget three things (and indeed if you make a random simp lemma choice for each of the 6 faces of the cube you seem to be able to get it circling forever)

[Yaël Dillies]

I have argued in the past that the data of an inverse should be the last thing you forget

[Eric Wieser]

I suspect that deciding that there will be a global order of forgetting is more important than what the order is

[Eric Wieser]

But to enforce this order with a linter, we'd need to tag edges with what they are forgetting.

[Yaël Dillies]

Eric Wieser said:

I suspect that deciding that there will be a global order of forgetting is more important than what the order is

I tend to agree, except for simplifications of the form e o e.symm

[Jireh Loreaux]

Totally half-baked idea: some of these shouldn't be simp lemmas? Only grind lemmas so that you get equality saturation instead of directionality? This may be total garbage, but I wanted to say it before I stop thinking about it.