Zulip Chat Archive
Stream: mathlib4
Topic: CoeFun
Yury G. Kudryashov (Dec 23 2022 at 21:35):
I started porting group_theory.subsemigroup.operations. It turns out that coercion of an order_iso to a function yields
↑(RelIso.toRelEmbedding e).toEmbedding
where the outer ↑ is FunLike.coe.
Yury G. Kudryashov (Dec 23 2022 at 21:37):
Why does it happen? What is the proper fix?
Eric Wieser (Dec 23 2022 at 23:06):
It means there is a shortcut instance that needs removing, I think
Eric Wieser (Dec 23 2022 at 23:06):
(deleted)
Yury G. Kudryashov (Dec 23 2022 at 23:34):
Should I remove most of CoeFun instances?
Eric Wieser (Dec 24 2022 at 08:55):
I can't find the one causing the problem now
Yury G. Kudryashov (Dec 24 2022 at 15:51):
I found it, fixing.
Yury G. Kudryashov (Jan 07 2023 at 18:57):
What are our plans about CoeFun? I can update https://github.com/leanprover-community/mathlib4/pull/1219 to work with master but I don't want to spend time on this if it won't get merged.
Yury G. Kudryashov (Jan 07 2023 at 18:58):
@Mario Carneiro @Gabriel Ebner @Eric Wieser :up:
Eric Wieser (Jan 07 2023 at 19:51):
That patch looks generally like the right thing to do to me
Yury G. Kudryashov (Jan 07 2023 at 21:27):
@Mario Carneiro was not happy about it, so I'm waiting for him. Also, we didn't hear from @Gabriel Ebner about this.
Gabriel Ebner (Jan 09 2023 at 23:27):
Happy new year! I think @Yury G. Kudryashov is doing the right thing here. If we want FunLike, then we need to use FunLike.coe everywhere.
Yury G. Kudryashov (Jan 11 2023 at 19:59):
@Gabriel Ebner Happy new year! Why exactly Lean 4 doesn't unfold FunLike.coe? It seems that Lean unfolds it for a MulEquiv.
Gabriel Ebner (Jan 11 2023 at 20:00):
If it gets unfolded then it must be because of a CoeFun instance.
Yury G. Kudryashov (Jan 11 2023 at 20:05):
Could you please have a look at https://github.com/leanprover-community/mathlib4/tree/YK-coe-fn ? I can't find any relevant CoeFun instance.
Yury G. Kudryashov (Jan 11 2023 at 20:06):
But RHS of MulEquiv.coe_toMulHom unfolds to f.toEquiv.toFun
Yury G. Kudryashov (Jan 11 2023 at 22:46):
Should we drop all the custom to*Hom functions in favor of one generic *Hom.of [*HomClass F M N] per *Hom?
Gabriel Ebner (Jan 12 2023 at 01:33):
Yury G. Kudryashov said:
But RHS of
MulEquiv.coe_toMulHomunfolds tof.toEquiv.toFun
I'm not sure I can repro that. coe_toMulHome has FunLike.coe on both sides for me.
Gabriel Ebner (Jan 12 2023 at 01:34):
Yury G. Kudryashov said:
Should we drop all the custom
to*Homfunctions in favor of one generic*Hom.of [*HomClass F M N]per*Hom?
That is an interesting refactoring. But we should probably wait until after the port with that.
Eric Wieser (Jan 12 2023 at 02:03):
We can't drop the to*Hom functions, can we? They're generated by the structure keyword
Eric Wieser (Jan 12 2023 at 02:04):
Yury G. Kudryashov said:
But RHS of
MulEquiv.coe_toMulHomunfolds tof.toEquiv.toFun
I would guess that this is a transitive coercion kicking in, that we probably don't want
Eric Wieser (Jan 12 2023 at 02:06):
Yury G. Kudryashov said:
one generic
*Hom.of [*HomClass F M N]per*Hom?
This already exists, it's docs#add_hom.has_coe_t etc
Eric Wieser (Jan 12 2023 at 02:06):
But to make Lean4 happy we probably need to give those functions new names thare aren't just coe
Gabriel Ebner (Jan 12 2023 at 02:07):
Eric Wieser said:
We can't drop the
to*Homfunctions, can we? They're generated by thestructurekeyword
Ah, you're right. And they probably appear in structure instances without us being able to do anything about that.
Gabriel Ebner (Jan 12 2023 at 02:37):
Hmm, I looked at two files, Algebra.Group.WithOne.Basic and Data.Real.CauSeq and they both built with minor (non-coe related) fixes. Not sure what the issue here is.
Yury G. Kudryashov (Jan 12 2023 at 05:15):
Probably, there was a problem with cached oleans.
Yury G. Kudryashov (Jan 29 2023 at 00:15):
I merged master and I get a bunch of compile errors that I fail to understand. It seems that simp fails to use lemmas like Finset.mapEmbedding_apply for no reason.
Kevin Buzzard (Jan 29 2023 at 00:19):
Does the linter like the lemmas which simp isn't using?
Yury G. Kudryashov (Jan 29 2023 at 00:28):
Yes.
Yury G. Kudryashov (Jan 29 2023 at 00:29):
My random guess is that simp fails to unify instances.
Yury G. Kudryashov (Jan 29 2023 at 00:29):
BTW, rw can use them when simp can't.
Kevin Buzzard (Jan 29 2023 at 01:44):
Oh yeah I've seen this before; I'm pretty sure there's a Zulip thread showcasing this regression, although I don't know if anyone opened an issue about it. There is a related but different issue where the simpNF linter complains that a lemma won't fire, and it does fire in simple cases but doesn't fire the moment things get more complicated because it can't solve the higher order unification -- but that seems to be not what is going on here. Maybe worth minimising and reporting?
Yury G. Kudryashov (Jan 29 2023 at 03:32):
Related issue: I tried to fix !4#1636 and got some strange failures.
Lukas Miaskiwskyi (Feb 07 2023 at 12:09):
Hmm, since this PR seems difficult to merge, is there any hope of creating smaller PRs to fix the individual CoeFun instances one at a time? Or are they heavily intertwined? The original issue with Equivs automatically being coerced to↑(RelIso.toRelEmbedding e).toEmbedding has given me a headache more and more often recently.
Lukas Miaskiwskyi (Feb 07 2023 at 12:11):
I've been able to work around this by just sprinkling in have : ↑(RelIso.toRelEmbedding e).toEmbedding = FunLike.coe e := rfl every now and then, for what it's worth.
Arien Malec (Feb 07 2023 at 16:01):
Can you document this in the wiki? (We need a section of "stupid porting tricks")...
Arien Malec (Feb 07 2023 at 16:07):
I'm in there -- will add it rn...
Yury G. Kudryashov (Feb 07 2023 at 18:50):
I'll try to do it tomorrow. Feel free to cherry-pick from my PR if you want to have it today.
Yuyang Zhao (Mar 01 2023 at 19:58):
Yury G. Kudryashov said:
My random guess is that
simpfails to unify instances.
I think so. Writing the lemma again and using it often works.
Last updated: Dec 20 2023 at 11:08 UTC