Stream: new members

Topic: Instances and coercion

Nicolò Cavalleri (Aug 23 2020 at 17:49):

Suppose I have to structures, foo and bar, such that foo extends bar and there is a coercion from foo to bar. If there's an instance of e.g. comm_group bar, what is the easiest and quickest way to transfer it to foo?

Kevin Buzzard (Aug 23 2020 at 22:10):

instance : comm_group foo := { ..bar.comm_group} maybe

Scott Morrison (Aug 23 2020 at 23:22):

I'm not sure your question makes sense. There's content: you need to know that the product of two bars which came from foos can be given the additional structure of a foo.

Nicolò Cavalleri (Aug 24 2020 at 12:47):

Yes you are right but the whole proof of this is in the has_mul instance. Is there not a way to do the rest in like one line? In any case this was the wrong example, I wrote a random class but I was thinking more of classes like partial_order where you have an induced order and you do not need to prove anything for it.

Reid Barton (Aug 24 2020 at 12:52):

Nicolò Cavalleri said:

Yes you are right but the whole proof of this is in the has_mul instance.

Well, no--you have to prove the new function is associative, and that the identity is a foo, and so on. (From the rest of your message I'm guessing foo extends bar with extra properties only and not extra data, but you didn't mention this.)

Is there not a way to do the rest in like one line? In any case this was the wrong example, I wrote a random class but I was thinking more of classes like partial_order where you have an induced order and you do not need to prove anything for it.

For a partial order, you can use docs#partial_order.lift if you have an injection foo -> bar.
In general, this procedure depends on the nature of the class (partial_order here).

Nicolò Cavalleri (Aug 24 2020 at 15:16):

What about lifting instances through equivalences? Is there a general way to do it under possibly some additional hypotheses or should I manually define a lift for the structures I'm intrested in?

Nicolò Cavalleri (Aug 24 2020 at 15:16):

(Are lifts through equivalences generally defined?)

Last updated: May 16 2021 at 05:21 UTC