coe and option

Stream: Is there code for X?

[Damiano Testa]

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]

I think you can spell this option.map coe

[Eric Wieser]

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]

(to match docs#lift_pair)

[Damiano Testa]

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]

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]

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

[Eric Wieser]

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

[Damiano Testa]

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]

I meant the opposite!

[Damiano Testa]

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]

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]

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]

Your instance is just as dangerous as mine

[Eric Wieser]

The one between int and nat specifically is safe

[Damiano Testa]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Just checking that you're aware

[Yakov Pechersky]

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

[Eric Wieser]

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

[Damiano Testa]

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!