simp normal form for `e.to_equiv.symm`

Stream: general

[Yury G. Kudryashov]

I've just noticed that docs#continuous_linear_equiv.symm_to_linear_equiv and docs#continuous_linear_equiv.symm_to_homeomorph simplify similar expressions in the opposite directions. Each form e.symm.to_weaker_equiv and e.to_weaker_equiv.symm has its advantages but I think that we should decide which one should be the simp normal form.

[Yury G. Kudryashov]

/poll Which form is better as the simp normal form?

[Gabriel Ebner]

I think we typically try to push symm and trans as far down as possible.

[Yury G. Kudryashov]

In case of e.symm.to_weaker_equiv we can automatically simplify (e.symm.to_weaker_equiv : M → N). In the other case we can automatically apply lemmas like weaker_equiv.trans_symm

[Yury G. Kudryashov]

Lemmas about continuous_linear_equiv.to_linear_equiv and symm/trans go in the opposite direction.

[Yury G. Kudryashov]

And I don't want to work on a refactor here without a poll.

[Floris van Doorn]

My instinct is the same as that of Gabriel, but I'm not sure about the particular advantages/disadvantages of each decision.

Yury G. Kudryashov said:

In case of e.symm.to_weaker_equiv we can automatically simplify (e.symm.to_weaker_equiv : M → N). In the other case we can automatically apply lemmas like weaker_equiv.trans_symm

We will still have to prove trans_symm for the stronger equivalences as well, independent of our choice here, right? So I'm not sure if the second point is a big advantage.

[Eric Wieser]

docs#equiv.trans_symm refers to expressions like e.symm.to_weaker_equiv.trans e.to_weaker_equiv, right?

[Yury G. Kudryashov]

If you have e : M ≃L[R] M' then with the second approach you can simplify e.symm.to_linear_equiv.trans e.to_linear_equiv.

[Eric Wieser]

But I guess as long you also have a lemma sending f.to_weaker_equiv.trans g.to_weaker_equiv to (f.trans g).to_weaker_equiv then that should be ok

[Eric Wieser]

So we need things like docs#ring_equiv.to_add_equiv_trans, which I assume we don't currently have?

[Floris van Doorn]

I thought it was implied in the question that if e.symm.to_weaker_equiv is simp-normal form, then (e.trans e').to_weaker_equiv is also simp-normal form. So then we can use stronger_equiv.trans_symm to rewrite (e.trans e.symm).to_weaker_equiv to weaker_equiv.refl

[Eric Wieser]

docs#ring_equiv.to_ring_hom_trans also goes in the wrong direction

[Eric Wieser]

Unless we decide that e.to_same_hom gets different rules

[Yury G. Kudryashov]

@Floris van Doorn I just forgot about this simp lemma.

[Floris van Doorn]

An argument for the second option:

If I have some (complicated) construction on stronger_equiv, like stronger_equiv_foo, then I probably want a simp lemma that
stronger_equiv_foo.to_weaker_equiv = weaker_equiv_foo. We can think of to_weaker_equiv as a "field" of stronger_equiv (independent of whether it actually is a field), so this simp lemma makes sense.
If I have some operation on stronger_equiv like the product of two such equivalences, what direction does the simp lemma go?

• (e.prod e').to_weaker_equiv = e.to_weaker_equiv.prod e'.to_weaker_equiv since to_weaker_equiv is a field?
• e.to_weaker_equiv.prod e'.to_weaker_equiv = (e.prod e').to_weaker_equiv because we want to push to_weaker_equiv to the outside, like for symm?

I'm not so sure about this case, but I think it makes sense to have the same rule for symm, trans, prod and all the other operations on equivalences.

[Eric Wieser]

I can't help feeling we're doomed to quadratically many lemmas (equiv strength x equiv operations) or worse no matter what we do

[Gabriel Ebner]

A related issue I've observed (to the explosion of simp lemmas) is that we apparently need e.symm (e x) = e for every kind of equivalence.

[Eric Wieser]

The usual way out of this type of explosion is polymorphism / multiple dispatch, which in lean would be typeclasses

[Yury G. Kudryashov]

@Sebastien Gouezel Could you please tell us what are your arguments in favor of e.to_weaker_equiv.symm?

[Yury G. Kudryashov]

I definitely don't want to start a refactor with your vote against it.

[Eric Wieser]

Can norm_cast help with to_X casts?

[Sebastien Gouezel]

My impression is that we try to push most operations to the lowest level. For instance, the canonical form of coe (f + g) is coe f + coe g, where we push the + to the weaker class. In the same way, coe (-f) is - coe f, pushing neg to the lowest level. If you replace neg with symm and coe with to_weaker_equiv, this hints at a normal form e.to_weaker_equiv.symm. But I don't feel very strongly about it, so if everyone agrees the other form is better then go for it!

[Yakov Pechersky]

While the other point of view is that to_weaker_equiv is neg in this case, while symm is coe?

[Sebastien Gouezel]

Except that to_weaker_equiv is really a form of coercion, and symm is really a form of neg. I didn't choose this example completely randomly :-)

[Yury G. Kudryashov]

One more argument for the second choice. If we have e.to_weaker_equiv.trans e'.to_weaker_equiv, where e and e' are of different types, then we can't transform it to a form similar to choice 1 without some norm_cast magic.

[Yury G. Kudryashov]

So, I move to "undecided".

[Yury G. Kudryashov]

It would be nice to have norm_cast treat all functions marked with some attribute as coercions.

[Yury G. Kudryashov]

So that we can mark theorems like coe_to_equiv with norm_cast and use them in norm_cast/push_cast.

[Heather Macbeth]

Yury G. Kudryashov said:

It would be nice to have norm_cast treat all functions marked with some attribute as coercions.

So that we can mark theorems like coe_to_equiv with norm_cast and use them in norm_cast/push_cast.

I was thinking at some point that it would be nice to let docs#polynomial.C be treated as a coercion.
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/norm_cast.20for.20algebras

[Eric Wieser]

I came across this again today; simps appears to work best with the second option that results in e.symm.to_weaker_equiv, as once the goal ends up in that state,docs#coe_to_add_equiv will strip the to_weaker_equiv and then the generated e_symm_apply will unfold the e.symm.

[Yury G. Kudryashov]

The second option makes e.to_weaker_equiv.symm the simp-normal form. This version needs a lemma like docs#diffeomorph.to_equiv_coe_symm in the API.

[Eric Wieser]

Whoops, that was a typo

[Sebastien Gouezel]

Did we finally make a decision here? I don't think the choice matters much (even though I still stand with option (2)), but I think that making a choice is important, to know what to use when writing new statements. Also, the question is both for symm and trans, i.e., should the normal form be f.to_weaker_equiv.trans g.to_weaker_equiv or (f.trans g).to_weaker_equiv? (The two questions are related, to make sure that simp works nicely).

[Scott Morrison]

Reading the thread I've added my vote to (2), but this is contrary to my initial instinct, so I remain uncertain!

[Scott Morrison]

I guess one way to think about it is "if we have an interesting strong-equiv, is it more likely that we have a nice description of its symm, or that we have a nice description of its to_weaker_equiv?" I would guess the latter, and hence 2).

[Yaël Dillies]

Don't bother about my opinion too much because I'm not using those much, but the first thing I want to do when seeing (f.trans g).to_weaker_equiv is to "simp" it to f.to_weaker_equiv.trans g.to_weaker_equiv.
My idea is that the stronger equiv is just here for its further properties, so when you don't need them you want that overbundling gone as much as possible.

[Yaël Dillies]

Also, f.to_weaker_equiv.trans g.to_weaker_equiv is closer to f.to_weaker_equiv.trans g and f.trans g.to_weaker_equiv, when only one of the equivalences has to be weakened.

[Reid Barton]

(2) is the direction consistent with docs#category_theory.functor.map_inv, docs#category_theory.functor.map_comp

[Reid Barton]

Also there's a third player here, refl--obviously we want stronger_equiv.refl.to_weaker_equiv = weaker_equiv.refl, and not the other way around

[Yaël Dillies]

I've changed my mind to the first option, because I just spent three hours fixing a simp call in #2819. There I have e (e.to_linear_equiv.to_continuous_linear_equiv.to_homeomorph.to_measurable_equiv.symm a), and all the simp lemmas were working against me!

[Yaël Dillies]

trans is already pushed down because of distributivity considerations. We don't have such considerations forsymm, so it's really up to us. And in that case, because we can simplify e.symm.to_equiv a but not e.to_equiv.symm a, I think we should push down.

[Yaël Dillies]

I am doubtful of the argument that we want the other way for simp to find things of the form e.trans e.symm because this lemma works against distributivity and this is not really simp's job (indeed, a norm_cast-like tactic would be much better suited).