# Zulip Chat Archive

## 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

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

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

#### 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 for`symm`

, 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