Zulip Chat Archive

I'm not a computer scientist, so I don't know the precise reason for distinguishing Coe, CoeHead, CoeTail, etc. When using them mathematically, e.g. constructing a bundled homomorphism from a coercion map, one has to refer to the coe function itself. In mathlib3, you just say coe, but in mathlib4 it seems that you have to say Coe.coe, CoeHead.coe, CoeTail.coe, etc, depending on how the coercion was defined. From a design perspective, shouldn't the mathematician's sensibilities be protected from this distinction, i.e. a single coe should automatically refer to whichever CoeXXX was used in the definition?

Moritz Doll (Nov 26 2022 at 23:56):

I don't think you should refer to coe, but the map that it is used for the coercion. With FunLike it has become more weird and so if you have a FunLike instance, then you have to refer to FunLike.coe.

Winston Yin (Nov 27 2022 at 00:11):

What about theorems that refer to ↑ generally, irrespective of how it's implemented? For example in this section, I had to explicitly call Coe.coe: https://github.com/leanprover-community/mathlib4/blob/4ceaeb25193e7d30b2c19230690fac7de911f00b/Mathlib/Algebra/Hom/Group.lean#L1538

Moritz Doll (Nov 27 2022 at 00:45):

don't quote me on it, but I think this is a bad class in Lean 4. I would expect that it is not necessary either. If you have something like an embedding of a subspace into the full space, then the coercion gets automatically replaced by the inclusion map and for that map the correct lemma should already exist in some other class.

Moritz Doll (Nov 27 2022 at 00:49):

Again I might be wrong here, but it sounds very similar to this:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathlib4.23557/near/308688698

Winston Yin (Nov 27 2022 at 01:13):

That makes sense. Let me write a comment in the PR

Winston Yin (Nov 27 2022 at 01:14):

And I'm going to quote your comment :sweat_smile:

Gabriel Ebner (Nov 27 2022 at 04:30):

That file shouldn't be ported for now. We might need to revert the whole coeismulhom etc. API.

Gabriel Ebner (Nov 27 2022 at 04:31):

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Please.20stop.20adding.20generalized.20API.20around.20coercions/near/310898388

Jireh Loreaux (Nov 27 2022 at 04:31):

If we're going to do that, can we make it happen ASAP?

Jireh Loreaux (Nov 27 2022 at 04:32):

We're going to start hitting it porting everywhere.

Gabriel Ebner (Nov 27 2022 at 04:35):

Yes.. we didn't decide on anything in n that thread. I think nobody wants to be the one who pulls the trigger, a revert is a pretty harsh reaction after all. But if we're actively hitting it during porting now, then we have no other choice.