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 degree
s 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 coe
s 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