deriving has_coe and coe_inj

Stream: general

[Bernd Losert]

In my code, I have

class kent_convergence_space (α : Type*) extends convergence_space α

So given p : kent_convergence_space α, I can use p.to_convergence_space. I was wondering if there is an attribute or a tactic or something that will give me the has_coe instance and a lemma that coe is injective. Or do I always have to manually write these out?

[Eric Wieser]

Asking for this kind of thing on class instead of structure indicates you might be using the former in a place where the latter is more appropriate

[Eric Wieser]

You always have to write out the coe, because it's not all that common for it to actually be a good idea. It's a lot harder to guess what ↑↑a means than it is to guess what a.to_foo.to_bar means

[Eric Wieser]

Having said that, you could certainly write a tactic / attribute to do what you're asking, and it would be a great exercise in learning to use Lean's metaprogramming

[Bernd Losert]

Maybe I should provide a bit more background. I have a hierarchy of classes:

convergence_space
kent_convergence_space
limit_space
pseudotopological_space
pretopological_space

All these things will have a partial_order inhereted from convergence_space. I'm using partial_order.lift coe coe_injective to achieve this. I was hoping for some automation regarding coe and coe_injective. I guess I'll have to pull my sleeves up and start metaprogramming.

[Eric Wieser]

Are coercions actually useful to you vs using partial_order.lift to_convergent_space to_convergent_space_injective?

[Eric Wieser]

That is, do you use them in enough places for the short notation to be worth it?

[Bernd Losert]

Yes. And I have just barely started fleshing out the theory of kent_convergence_spaces.

[Eric Wieser]

I ask only because I can only think of one case that comes anywhere close to this kind of design in mathlib, docs#topological_group

[Eric Wieser]

Actually, that's not a class anyway