Stream: general

Topic: simp normal form for e.to_equiv.symm

Yury G. Kudryashov (Mar 03 2021 at 18:23):

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 (Mar 03 2021 at 18:23):

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

Gabriel Ebner (Mar 03 2021 at 18:24):

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

Yury G. Kudryashov (Mar 03 2021 at 18:25):

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 (Mar 03 2021 at 18:26):

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

Yury G. Kudryashov (Mar 03 2021 at 18:26):

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

Floris van Doorn (Mar 03 2021 at 18:32):

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 (Mar 03 2021 at 18:34):

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

Yury G. Kudryashov (Mar 03 2021 at 18:35):

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 (Mar 03 2021 at 18:35):

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 (Mar 03 2021 at 18:36):

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

Floris van Doorn (Mar 03 2021 at 18:36):

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 (Mar 03 2021 at 18:37):

docs#ring_equiv.to_ring_hom_trans also goes in the wrong direction

Eric Wieser (Mar 03 2021 at 18:39):

Unless we decide that e.to_same_hom gets different rules

Floris van Doorn (Mar 03 2021 at 18:45):

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 (Mar 03 2021 at 19:04):

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 (Mar 03 2021 at 19:06):

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 (Mar 03 2021 at 19:07):

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

Yury G. Kudryashov (Mar 03 2021 at 19:26):

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

Yury G. Kudryashov (Mar 03 2021 at 19:27):

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

Eric Wieser (Mar 03 2021 at 19:45):

Can norm_cast help with to_X casts?

Sebastien Gouezel (Mar 03 2021 at 20:06):

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 (Mar 03 2021 at 20:08):

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

Sebastien Gouezel (Mar 03 2021 at 20:31):

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 (Mar 03 2021 at 20:41):

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 (Mar 03 2021 at 20:41):

So, I move to "undecided".

Yury G. Kudryashov (Mar 03 2021 at 20:42):

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

Yury G. Kudryashov (Mar 03 2021 at 20:43):

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

Heather Macbeth (Mar 03 2021 at 20:49):

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 (Aug 04 2021 at 22:23):

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 (Aug 05 2021 at 05:30):

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 (Aug 05 2021 at 07:11):

Whoops, that was a typo

Sebastien Gouezel (Sep 24 2021 at 07:47):

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 (Sep 24 2021 at 07:55):

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

Scott Morrison (Sep 24 2021 at 07:56):

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 (Sep 24 2021 at 08:37):

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 (Sep 24 2021 at 08:38):

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 (Sep 24 2021 at 09:55):

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

Reid Barton (Sep 24 2021 at 09:57):

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 (Dec 16 2022 at 17:55):

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 (Dec 16 2022 at 17:58):

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 (Dec 16 2022 at 18:02):

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).

Last updated: Aug 03 2023 at 10:10 UTC