Zulip Chat Archive

Stream: Is there code for X?

Topic: coe and option


Damiano Testa (Jul 08 2022 at 07:27):

Dear All,

I would like to have a coercion between with_bot ℕ and with_bot ℤ, to work more smoothly with degrees of polynomials and Laurent polynomials. It seems that what is below works for me. However, I am surprised that I could not find it: is there some problem with the definitions/instances below? Are they in mathlib somewhere already?

Thanks!

import order.bounded_order

def option.coe {α β} [has_coe α β] : option α  option β
| none     := none
| (some a) := some a

instance option.has_coe {α β} [has_coe α β] : has_coe (option α) (option β) :=
option.coe

instance with_bot.has_coe {α β} [has_coe α β] : has_coe (with_bot α) (with_bot β) :=
option.has_coe

Eric Wieser (Jul 08 2022 at 08:06):

I think you can spell this option.map coe

Eric Wieser (Jul 08 2022 at 08:07):

It's not clear to me whether such a function is special enough to be give a has_coe instance. Maybe a docs#has_lift instance is reasonable

Eric Wieser (Jul 08 2022 at 08:09):

(to match docs#lift_pair)

Damiano Testa (Jul 08 2022 at 08:10):

Thanks! This works:

instance with_bot.has_coe {α β} [has_coe α β] : has_coe (with_bot α) (with_bot β) :=
option.map coe

As for it being an instance, I am not too worried about this. I can always make it a local instance for degrees of Laurent polynomials, if I see that I need to insert option.map coes everywhere.

Damiano Testa (Jul 08 2022 at 08:12):

Is the one below the instance that you are suggesting?

instance option.has_lift {α β} [has_coe α β] : has_lift (option α) (option β) :=
option.map coe

Eric Wieser (Jul 08 2022 at 08:13):

The second has_coe should also say has_lift_t (edit: _t)

Eric Wieser (Jul 08 2022 at 08:15):

Although I'm worried there might be a diamond here considering casting option X to option (option X)

Damiano Testa (Jul 08 2022 at 08:15):

instance option.has_lift {α β} [has_coe α β] : has_lift_t (option α) (option β) :=
option.map coe

(I left has_coe as an assumption and list_t as instance, assuming I parsed things correctly!)

Eric Wieser (Jul 08 2022 at 08:15):

I meant the opposite!

Damiano Testa (Jul 08 2022 at 08:15):

Ok, I'll just leave it be: I am going to try using option.map coe: it may be that I only need it in a couple of lemmas, and then it gets shielded away by the API.

Eric Wieser (Jul 08 2022 at 08:17):

Regarding the diamond; none : option X is sent by the existing coercion to some none : option (option X), but via your coercion (with the [has_coe] argument populated by the existing one) to none : option (option X)

Damiano Testa (Jul 08 2022 at 08:18):

Ok, I won't bother changing the instance above to what you had meant, since it seems like it is not a good idea anyway!

Eric Wieser (Jul 08 2022 at 08:18):

Your instance is just as dangerous as mine

Eric Wieser (Jul 08 2022 at 08:18):

The one between int and nat specifically is safe

Damiano Testa (Jul 08 2022 at 08:19):

Yes, I am just not going to add any instance for the moment. I'll play without it and see what happens.

As you say, I might simply put one locally and for nat to int.

Damiano Testa (Jul 08 2022 at 08:19):

(which ultimately is all that I need at the moment)

Yakov Pechersky (Jul 08 2022 at 12:58):

Damiano, my recent PR switched the definition of degree to no longer rely on option

Yakov Pechersky (Jul 08 2022 at 12:58):

Just checking that you're aware

Yakov Pechersky (Jul 08 2022 at 12:59):

I think the dangerousness of the instance goes away if you use has_coe_t

Eric Wieser (Jul 08 2022 at 13:17):

I'm pretty sure it remains just as dangerous; but I guess the easy thing to do is try it and see

Damiano Testa (Jul 08 2022 at 13:18):

Ah, as I had never really used degree, I did not know what to expect. I'll make sure to merge master before I continue gluing the degree that I'm defining on Laurent polynomials to the "latest" one on mathlib. Thanks for the head up!


Last updated: Dec 20 2023 at 11:08 UTC