Zulip Chat Archive

Stream: general

Topic: coe_trans


view this post on Zulip Kenny Lau (Jul 12 2020 at 13:17):

instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t b c] [has_coe a b] : has_coe_t a c

view this post on Zulip Kenny Lau (Jul 12 2020 at 13:17):

why doesn't this instance cause loops in typeclass search?

view this post on Zulip Floris van Doorn (Jul 12 2020 at 22:32):

When looking for has_coe_t a c it first looks for instances for has_coe a ?m (which should only be a finite list, if you know a) and then looks for has_coe_t b c so as long as we restrict the has_coe instances enough (no cycles, adherence to this library note: https://leanprover-community.github.io/mathlib_docs/notes.html#use%20has_coe_t) there should not be a loop.

view this post on Zulip Floris van Doorn (Jul 12 2020 at 22:33):

(instance arguments are filled in from right-to-left, to speed-up the search for classes like algebra R A).

view this post on Zulip Johan Commelin (Jul 13 2020 at 05:36):

But the trouble with algebra_trans would come from the identity algebra R R... that would cause loops anyway )-;

view this post on Zulip Kenny Lau (Jul 13 2020 at 05:48):

@Johan Commelin we can avoid that by having algebra_t R R

view this post on Zulip Kenny Lau (Jul 13 2020 at 05:49):

you won't ever have algebra R R to cause the loop

view this post on Zulip Johan Commelin (Jul 13 2020 at 05:51):

Aah, and you are saying that we should only ever use algebra_t?
But aren't we still going to run into non-defeq diamonds?

view this post on Zulip Johan Commelin (Jul 13 2020 at 05:52):

Like, I compose the algebra instance int -> rat with rat -> real, and this will not be defeq to int -> real.

view this post on Zulip Johan Commelin (Jul 13 2020 at 05:52):

That's why I think we should have a typeclass like tower or commutes that expresses the provable equality of these instances.

view this post on Zulip Kenny Lau (Jul 13 2020 at 06:09):

fair


Last updated: May 06 2021 at 21:09 UTC