Zulip Chat Archive

Stream: new members

Topic: extends coercion


Raphael Appenzeller (Jul 26 2022 at 23:40):

In the following example I introduce a class my_pointed_space and then extend it to a class singular_space. Later on I would like to coerce a singular_space to a my_pointed_space. Should this not happen automatically due to the keyword extends? MWE:

class my_pointed_space (α : Type*) :=
(a : α )

class singular_space (α: Type*) extends my_pointed_space α :=
(extra_property :  x : α , x = my_pointed_space.a )

class my_map {α β : Type*} (X : my_pointed_space α ) ( Y : my_pointed_space β):=
(to_fun : α  β)
(compatibility : to_fun(X.a) = Y.a)

class inj {α β : Type*} (X : singular_space α) (Y : my_pointed_space β) extends my_map X Y

David Renshaw (Jul 26 2022 at 23:43):

does it work if you do X.to_my_pointed_space?

Kyle Miller (Jul 26 2022 at 23:45):

I haven't tested it, but you want to declare it something like this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α  β)
(compatibility : to_fun (my_pointed_space.a α) = my_pointed_space.a β)

Yaël Dillies (Jul 26 2022 at 23:45):

"coerce" has a very specific meaning in Lean, and this is probably not what you want.

Yaël Dillies (Jul 26 2022 at 23:45):

Kyle, I suspect the problem is that there are many ways to point a given type!

Kyle Miller (Jul 26 2022 at 23:45):

The purpose of classes is that you're going to rely on typeclass inference to obtain structures in an implicit way.

Yaël Dillies (Jul 26 2022 at 23:46):

Btw,my_pointed_space is docs#Pointed

Yaël Dillies (Jul 26 2022 at 23:46):

And my_map is docs#Pointed.hom

Kyle Miller (Jul 26 2022 at 23:47):

Yaël Dillies said:

Kyle, I suspect the problem is that there are many ways to point a given type!

If you're #xy'ing it, sure, but I think the proximal problem is about using classes correctly

Kyle Miller (Jul 26 2022 at 23:48):

Once you've got that my_map, then I expect something like this should work:

class inj (α β : Type*) [singular_space α] [my_pointed_space β] extends my_map α β

David Renshaw (Jul 26 2022 at 23:57):

@Kyle Miller to get your version to work I needed to change it to this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α  β)
(compatibility : to_fun (@my_pointed_space.a α _) = @my_pointed_space.a β _)

Kyle Miller (Jul 27 2022 at 00:35):

@David Renshaw Ok, that means the types didn't come out the way I expected them to on my_pointed_space. The idiomatic way to write it then is this:

class my_map (α β : Type*) [my_pointed_space α] [my_pointed_space β] :=
(to_fun : α  β)
(compatibility : to_fun (my_pointed_space.a : α) = (my_pointed_space.a : β))

Kyle Miller (Jul 27 2022 at 00:36):

I think the way to get my original version to work is to do

class my_pointed_space (α : Type*) :=
(a [] : α)

which causes my_pointed_space.a to take an explicit argument.

Kyle Miller (Jul 27 2022 at 00:37):

I believe what's going on is that Lean sees that alpha is inferrable from the return type so it makes it implicit by default.

Raphael Appenzeller (Jul 28 2022 at 07:39):

Thanks a lot for your answers. Indeed my problem was that I was not using classes correctly.


Last updated: Dec 20 2023 at 11:08 UTC