simp normal form for symm and coercions

Stream: mathlib4

[Sébastien Gouëzel]

The following two lemmas are registered as simp lemmas in mathlib:

lemma foo (e : E ≃L[𝕜] F) : e.symm.toLinearEquiv = e.toLinearEquiv.symm :=
  ContinuousLinearEquiv.symm_toLinearEquiv _

lemma bar (e : E ≃ₗ[𝕜] F) : e.toEquiv.symm = e.symm.toEquiv :=
  LinearEquiv.coe_toEquiv_symm _

They dont' simplify in the same direction, which means that e.toLinearEquiv.toEquiv.symm = e.symm.toLinearEquiv.toEquiv is not provable by simp. Do we have a prefered canonical direction?

[Sébastien Gouëzel]

(And a prefered naming scheme, also?)

[Eric Wieser]

#general > simp normal form for `e.to_equiv.symm` @ 💬

[Eric Wieser]

(should we merge the threads?)

[Sébastien Gouëzel]

Ah, it's true. I guess this is one of these things where we will never make a decision, then. I'll just change the direction of one of the lemmas above for local coherence, then. It's not as good as a global decision, but still better than the status quo.

[Sébastien Gouëzel]

There is also the issue of naming with dot notation here. We have the next lemmas in the library, following each other:

@[simp]
theorem symm_toLinearEquiv (e : M₁ ≃SL[σ₁₂] M₂) : e.symm.toLinearEquiv = e.toLinearEquiv.symm := by
  ext
  rfl

@[simp]
theorem symm_toHomeomorph (e : M₁ ≃SL[σ₁₂] M₂) : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

They use a normal form in reverse directions, but they are named similarly!

[Eric Wieser]

While the vote was split, it was also barely voted upon, so a global decision feels possible

[Kevin Buzzard]

This feels similar to the problem we had with casts until we got norm_cast and push_cast. But at least with casts we are consistent with directions!

[Sébastien Gouëzel]

ok, let me summarize the discussion and then open a poll.

[Sébastien Gouëzel]

Given e a continuous linear equiv, there are two ways to consider the inverse as a linear equiv: e.symm.toLinearEquiv and e.toLinearEquiv.symm (similarly for trans, and similarly for many equiv classes in the library, the above is just a representative example).

We should choose a simp normal form, pushing symm either to the left, as in e.symm.toLinearEquiv, or to the right as in e.toLinearEquiv.symm. There are arguments in favor of one or the other, so there is no obvious better form, but still for coherence and predictability we should make a choice, as otherwise various simp lemmas will fight against each other.

A few remarks:

(a) For refl, we should push it to the right: the normal form of ContinuousLinearEquiv.refl.toLinearEquiv should obviously be LinearEquiv.refl

(b) For function applications, we should push it to the left: if x is a point, then e.toLinearEquiv.symm x should be simplified to e.symm x.

(c) For an analogy, consider f an equiv between E and F, and the coercion to functions. Then (with made up dot notation) f.symm.coe makes sense, but f.coe.symm does not make sense, so in this case the only possible thing is to push symm to the left.

(d) For another analogy, let c be an additive group morphism, and let neg be negation. Then we simplify c (- x) to - c x, i.e., we change x.neg.c to x.c.neg, i.e., we push neg to the right. As neg is a clear analogue of symm, this is in favor of pushing to the right.

[Sébastien Gouëzel]

Initially, I was really convinced by (d), but thinking more of it the reason we push addition and negation to the right is usually so that we can try to simplify the remaining expression with abel or friends, which is not really relevant in an equiv-like context. So, I don't have a strong opinion. Maybe I'd err somewhat on the side of pushing to the left.

[Sébastien Gouëzel]

/poll Should the simp normal form be e.symm.toLinearEquiv or e.toLinearEquiv.symm?
e.symm.toLinearEquiv
e.toLinearEquiv.symm
I don't care, but we should make a coherent choice
I don't care, and I don't even think we should make a coherent choice

[Sébastien Gouëzel]

Comments on other examples in the library where one direction is more convenient than the other are most welcome. As well as other arguments, information I don't have about how things are handled in the category theory folders, and so on!

[Yaël Dillies]

Sébastien Gouëzel said:

(b) For function applications, we should push it to the left: if x is a point, then e.toLinearEquiv.symm x should be simplified to e.symm x.

e.toLinearEquiv.symm x = e.symm x is a projection lemma for toLinearEquiv. Therefore point (b) doesn't matter, as if we are pushing the symm right-wards then we should simply add that projection lemma

[Sébastien Gouëzel]

Sure, (b) is not incompatible with pushing to the left, we just need to add the correct simp lemma. I think there is no global obstruction to picking either left or right, we will just need to adjust the simpset.

[Sébastien Gouëzel]

(If we push to the left, we just need to add the simp lemma e.toLinearEquiv x = e x, while if we push to the right we need to add both e.toLinearEquiv x = e x and e.toLinearEquiv.symm x = e.symm x, so pushing to the right is slightly more expensive than pushing to the left in this respect. This is why I am saying that (b) is in favor of pushing to the left.)

[Jovan Gerbscheid]

If the goal is coherence and predictability, and if toLinearEquiv is a coercion, then shouldn't we use the convention for coercions? i.e. toLinearEquiv going inward and symm going outward.

[Sébastien Gouëzel]

Is there really a convention for coercions?

[Jovan Gerbscheid]

Doesn't e.g. docs#Int.cast_add follow the general pattern?

[Sébastien Gouëzel]

For numerical casts, yes, definitely, because you want things to become elementary atoms to which operations are applied, to be able to use abel or friends. That's (d) in the above discussion. But it's not clear to me that it applies in general.

[Yaël Dillies]

Jovan's point is a strong argument for toLinearEquiv going inwards

[Jovan Gerbscheid]

If we do decide to follow that logic, we should unsimp docs#LinearEquiv.comp_coe, right?

[Yaël Dillies]

That lemma is the wrong way around!

[Sébastien Gouëzel]

ok, if everyone agrees that this lemma is the wrong way around, this is another argument for pushing symm to the right.

[Eric Wieser]

What should happen to (f e).toLinearEquiv.symm.toAddEquiv? Often there's a simp lemma of the form (f e).symm = f e.symm, which obviously can't apply unless the symm is pushed to the left

[Eric Wieser]

Is the answer that we should write extra simp lemmas like (f e).toLinearEquiv = fLinear e (possibly introducing intermediate bundlings along the way?)

[Sébastien Gouëzel]

If we decide we want to push symm to the right, yes, we should add the corresponding simp lemmas for concrete fs. Do you have a specific example in mind?

[Eric Wieser]

I'm thinking of things like docs#Finsupp.domLCongr

[Sébastien Gouëzel]

Or we could have a simp lemma (f e).toLinearEquiv = fLinear e.toLinearEquiv, and then if symm is pushed to the right you just need the simp lemma (fLinear e).symm = fLinear e.symm.

[Eric Wieser]

This is a little bit annoying for cases when the map is already the weakest interesting bundling, as the weaker bundlings have no reason to exist beside simp confluence; but pragmatically these symm chains probably never appear in those cases anyway

[Andrew Yang]

If we push symm outwards, do we now have to write the lemmas E.toSomeEquiv.symm.toSomeOtherMap = E.symm.toSomeOtherMap for all coercion chains E -> SomeEquiv -> SomeOtherMap?

[Jovan Gerbscheid]

That rewrite can just be done by a lemma saying E.toSomeEquiv.symm = E.symm

[Andrew Yang]

And we almost never want simp lemmas with LHS E.toLinearEquiv but we sometimes do have E.symm = ? lemmas. This is another reason why I prefer pushing symm inwards.

[Andrew Yang]

Jovan Gerbscheid said:

That rewrite can just be done by a lemma saying E.toSomeEquiv.symm = E.symm

Yes. So my point is that we should make this lemma simp.

[Jovan Gerbscheid]

Are they not already tagged with simp?

[Andrew Yang]

I thought the point some people are making in thread is to turn that simp lemma around.

[Jovan Gerbscheid]

Sorry I got confused by how you wrote the lemma. The discussion is about lemmas of the form E.toSomeEquiv.symm = E.symm.toSomeEquiv

[Andrew Yang]

Is that not what you said? I thought you just forgot to add toSomeEquiv at the end. Your statement as is doesn't typecheck.

[Sébastien Gouëzel]

Andrew Yang said:

If we push symm outwards, do we now have to write the lemmas E.toSomeEquiv.symm.toSomeOtherMap = E.symm.toSomeOtherMap for all coercion chains E -> SomeEquiv -> SomeOtherMap?

I'm not sure I understand the question. It's about the case where you have a map to something else which is not an equiv, right? Like ContinuousLinearEquiv, LinearEquiv, ContinuousLinearMap, LinearMap? That's yet another normal form question: for e : ContinuousLinearEquiv, we have e.toLinearEquiv.toLinearMap = e.toContinuousLinearMap.toLinearMap, and we should choose a normal form between the two of them.

But I don't see how symm plays with this. Is your point that e.toLinearEquiv.symm.toLinearMap is bad, and that you prefer e.symm.toContinuousLinearMap.toLinearMap?

[Andrew Yang]

I think the simp normal form should be LinearMapClass.toLinearMap e.symm.

[Eric Wieser]

That's usually a pretty bad simp-normal form, as for some e : ContinuousLinearEquiv, that hides the .toLinearEquiv.toLinearMap part of the chain each of which has separate lemmas about it

[Eric Wieser]

Eg we often have fContEquiv.toLinearEquiv = fEquiv, and fEquiv.toLinearMap = fMap as lemmas but not LinearMapClass.toLinearMap fContEquiv = fMap, as having to write a lemma for every pair of connected nodes in the graph is much most costly than doing so for every edge.

[Andrew Yang]

My experience is you almost never want fContEquiv.toLinearEquiv = fEquiv or fEquiv.toLinearMap = fMap or LinearMapClass.toLinearMap fContEquiv = fMap to be simp lemmas because you are losing information.

[Yaël Dillies]

... but you are also accessing a lot more existing lemmas

[Andrew Yang]

Aren't you just missing lemmas for fContEquiv?
But anyways my argument was based on these things were not simp lemmas or weren't even lemmas at all but if there are already a bunch of such lemmas in the simp set and people rely on them, then symm probably should go outward instead.

[Eric Wieser]

Andrew Yang said:

to be simp lemmas because you are losing information.

What information are you losing?

[Sébastien Gouëzel]

@Eric Wieser, given what you explained, would you say that the simp lemma docs#LinearEquiv.coe_toAddEquiv, i.e.,

@[simp]
theorem coe_toAddEquiv : e.toAddEquiv = e :=
  rfl

is not a good simp lemma? On the right, there is an implicit application of AddEquivClass.toAddEquiv.

[Eric Wieser]

I think that AddEquivClass.toAddEquiv should not be simp-normal form; so the lemma as is currently does no harm, but I think other lemmas we don't yet have should make simpNF complain about it.

[Eric Wieser]

Yes, I think that is a bad simp lemma, and should go in the other direction

[Eric Wieser]

But I think there are many like it

[Sébastien Gouëzel]

ok, then this normal form story is definitely a mess. For e : LinearEquiv, should the normal form of e.toAddEquiv be e.toAddEquiv or the coercion from AddEquivClass? Eric says e.toAddEquiv, the library currently says the coercion. I won't start another poll!

[Yaël Dillies]

My opinion is that there should be no generic coercion at all from just AddEquivClass

[Andrew Yang]

Eric Wieser said:

What information are you losing?

For example (Algebra.TensorProduct.comm R A B).toLinearMap (x * y) should simp to Algebra.TensorProduct.comm R A B x * Algebra.TensorProduct.comm R A B y but if you add (Algebra.TensorProduct.comm R A B).toLinearMap = TensorProduct.comm R A B simp will now forget it is actually an algebra map and simp that to TensorProduct.comm R A B (x * y) (or you will have non-confluent simps)

[Eric Wieser]

I think here you can just tell it to apply f.toLinearMap x = f x first?

[Andrew Yang]

(deleted)

[Andrew Yang]

How would you achieve that? Is there a priority setting on simp lemmas?

[Eric Wieser]

Yes, as well as pre and post settings

[Eric Wieser]

In your example though the answer is to write the comm_mul lemmas, as it applies more generally for non-unital rings

[Sébastien Gouëzel]

Given the discussion, and the fact that most people don't really care about the direction, I chose to push symm to the right to follow the usual convention for coercions. PR at #25604. If people think it's a move in the right direction, I will do another PR to kill the coercion from EquivLike classes to Equivs, which messes up the normal form at several places.

A note on the naming: the goal is, for each equiv class, to have simp lemmas of the form

@[simp]
lemma coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e := rfl

@[simp]
lemma coe_symm_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv.symm = e.symm := rfl

@[simp]
lemma toEquiv_symm (e : G ≃+c[a, b] H) : e.symm.toEquiv = e.toEquiv.symm := rfl

@[simp]
lemma toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) :
    (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv := rfl

Note how the naming I have used does not follow the dot notation order, but rather the logical order. I don't know if we have a clear convention for that, so please complain if you think I should use the opposite order (especially if you are @Yaël Dillies or @Eric Wieser, who I would trust most on these issues :-)

[Eric Wieser]

Can you also explain what the target is for the lemmas about:

• concrete equivalences with various bundling (eg docs#WithLp.linearEquiv)
• Functorial equivalences

[Sébastien Gouëzel]

Oops, I forgot the deprecations, so not ready for review.

[Yaël Dillies]

Sébastien Gouëzel said:

I will do another PR to kill the coercion from EquivLike classes to Equivs

Just warning you that it's difficult :sad: #21031

[Yaël Dillies]

Sébastien Gouëzel said:

Note how the naming I have used does not follow the dot notation order, but rather the logical order.

All in favor :+1:

[Sébastien Gouëzel]

Eric Wieser said:

Can you also explain what the target is for the lemmas about:

• concrete equivalences with various bundling (eg docs#WithLp.linearEquiv)
• Functorial equivalences

I am not planning to change anything about these, and I don't know what the targets would be. The goal here is just one tiny improvement to our rules about normal forms (push symm outside) -- and I agree there is plenty of room for improvement elsewhere!

[Andrew Yang]

Are we also killing the coercion from funlike classes to homs?

[Sébastien Gouëzel]

Yes, that's what @Yaël Dillies is doing in #21031.

By the way, #25604 is ready.

[Kenny Lau]

can anyone find the thread where it was discussed whether e.toRingEquiv.symm or e.symm.toRingEquiv was the simpNF?

[Kenny Lau]

I want to see what the arguments for both sides are

[Jireh Loreaux]

#mathlib4 > simp normal form for symm and coercions

[Kenny Lau]

I am very confused while reading this thread

[Kenny Lau]

maybe I should ask chatgpt to summarise this thread

[Kenny Lau]

ChatGPT output:
==============

:justice: Arguments for pushing symm to the left

(i.e. canonical form e.symm.toLinearEquiv)
1. Analogy with function application
If x is a point, e.toLinearEquiv.symm x should simplify to e.symm x.
This is more natural when symm is “outside”.
(Though Yaël Dillies noted this can be handled separately by projection lemmas.)
2. Fewer projection lemmas needed
If symm is on the left, you only need
@[simp] lemma e.toLinearEquiv x = e x,
whereas pushing symm right requires both that and
@[simp] lemma e.toLinearEquiv.symm x = e.symm x.
So “left” is slightly cheaper to maintain.
3. Conceptual clarity
This makes symm a property of the equivalence object itself, not of the linear map.
It mirrors how we think of e.symm as a new equivalence rather than the inverse of a map.
4. Better alignment with lemmas like (f e).symm = f e.symm
If symm is always outer, these standard functorial lemmas can apply directly.
Supporters / comments:

• Andrew Yang preferred this form because simp lemmas often have LHS e.symm = ..., not e.toSomething.symm = ....

• Pushing symm inward (right) would require extra simp lemmas for every coercion chain.

---

:gear: Arguments for pushing symm to the right

(i.e. canonical form e.toLinearEquiv.symm)
1. Coercion convention consistency
Jovan Gerbscheid and Yaël Dillies argued that since toLinearEquiv acts as a coercion, it should behave like numeric or algebraic coercions, where operations (like symm, neg, +) are pushed outward.
This matches norm_cast/push_cast conventions.
2. Analogy with negation and arithmetic
Sébastien’s point (d):
for morphisms c, c (-x) simplifies to - c x, i.e. x.neg.c → x.c.neg.
By analogy, we should push symm outward/rightward.
3. Simpler normal forms for chained coercions
If e : ContinuousLinearEquiv, we have chains like
e.toLinearEquiv.toLinearMap = e.toContinuousLinearMap.toLinearMap.
Pushing symm right gives a uniform “outermost operation” approach.
4. Convention for coercions in mathlib
Sébastien concluded that, for predictability, we should “follow the usual convention for coercions” — meaning push symm outwards (right).
Supporters / comments:

• Jovan and Yaël noted that numeric coercions already behave this way.

• Eric Wieser agreed that if coercions are treated uniformly, this is consistent.

• Sébastien later implemented this choice in PR #25604.

[Kenny Lau]

---

so I'm currently in the "left" camp just because I want e.toLinearMap.symm x = e.symm x to be more easily provable.

I don't think the analogies from the "right" camp make a lot of sense, because when you do something like f(-x) = -f(x), the role of f (which is "toLinearMap") is actually transporting from less structure to more structure, e.g. from int to ring, you never go from ring to int.

but the coercions here (i.e. toLinearMap) goes from more structure to less structure, so I don't think analogy applies.

[Kenny Lau]

I don't think "convention" is a good argument and I'm surprised people went with the right when the left has an actual argument (which is the function application above)

[Sébastien Gouëzel]

Kenny Lau said:

so I'm currently in the "left" camp just because I want e.toLinearMap.symm x = e.symm x to be more easily provable.

With the current approach, this is registered as a simp lemma, so definitely easily provable!

Both approaches have pros and cons. The main point was to make one choice, to have a coherent mathlib.