Zulip Chat Archive

Stream: mathlib4

Topic: coe_mk and similar lemmas

Winston Yin (Dec 05 2022 at 01:43):

Since Lean4 now enforces the new structure extension, I'd like to understand the extent to which lemmas about mk are needed at each level of extension. For example, docs#mul_equiv extends docs#equiv and docs#mul_hom. Would mul_equiv.coe_mk (which currently takes functions as arguments) be broken down into a lemma taking an equiv as argument, and another lemma equiv.coe_mk taking functions as arguments? What about mul_equiv.symm_mk?

Winston Yin (Dec 05 2022 at 01:45):

I'm currently porting all these lemmas by writing nested constructors

Floris van Doorn (Dec 05 2022 at 13:09):

Note that the statement of MulEquiv.coe_mk in Lean 4 will be syntactically the same as (MulEquiv.mk f g h₁ h₂ h₃).toFun = f, and dsimp only will do this automatically for you. Therefore, the lemma is likely not necessary anymore. I don't know if we want to keep it around for porting reasons.

Eric Wieser (Dec 05 2022 at 14:33):

If we drop it we should use #noalign

Kevin Buzzard (Dec 05 2022 at 19:45):

I just learnt about #noalign yesterday. What does the autoporter do if Lean 3 uses a declaration which has been no-aligned? Prove false?

Mario Carneiro (Dec 05 2022 at 20:06):

It uses sorry instead

Winston Yin (Dec 06 2022 at 22:24):

@Floris van Doorn As a heuristic, would you say that I can just remove all lemmas that can be proven with by dsimp only?

Floris van Doorn (Dec 06 2022 at 23:50):

Yes, that sounds like a good heuristic to me.

Chris Hughes (Feb 13 2023 at 13:19):

It seems like docs#linear_equiv.coe_mk was deleted in the port and then in !4#2250 it was added again as a have on line 425 (Not sure how to link directly to the line). Should it not have been deleted?

Eric Wieser (Feb 13 2023 at 13:35):

We should not be deleting these lemmas at all

Eric Wieser (Feb 13 2023 at 13:36):

If it was deleted, it was probably because something else was misported in the file in an earlier version

Chris Hughes (Feb 13 2023 at 13:42):

But we should be removing the simp attributes from these lemmas? They're often flagged by the linter.

Eric Wieser (Feb 13 2023 at 13:45):

Is this particular lemma flagged?

Eric Wieser (Feb 13 2023 at 13:45):

My hunch is that it was flagged by the linter when something else was misported, then we fixed the misport. The linter would have stopped flagging it; but it was already gone

Chris Hughes (Feb 13 2023 at 13:46):

Seems not https://github.com/leanprover-community/mathlib4/pull/2253

Eric Wieser (Feb 13 2023 at 13:54):

The lemma was modified to be a tautology in "some progress", and then later removed

Kevin Buzzard (Feb 13 2023 at 22:27):

Yeah this is a common gotcha

Last updated: Dec 20 2023 at 11:08 UTC