Making variable in class field explicit

Stream: mathlib4

[Adam Topaz]

What's the Lean4 way to accomplish the following lean3 code?

import logic.equiv.defs

class foo (X : Type) :=
(e : X ≃ X)

#check foo.e

class bar (X : Type) :=
(e [] : X ≃ X)

#check bar.e

Adding the [] doesn't seem to work in Lean4.

[Notification Bot]

This topic was moved here from #new members > Making variable in class field explicit by Adam Topaz.

[Adam Topaz]

(I posted in the wrong stream accidentally)

[Adam Topaz]

BTW @Moritz Firsching , I'm trying to get mathlib4#1889 to compile, I hope that's okay with you (the PR is tagged with "help needed")

[Moritz Firsching]

Perfect!

[Adam Topaz]

well, I got the file to build, but there is still explicit/implicit variable issue in the IsFreeGroup class.

[Eric Rodriguez]

I think the current lean4 solution is making it as a dot notation thing separately and priming the structure field. It's not great.

[Adam Topaz]

Yeah that's not ideal. So what should we do to move this porting PR along? The issue is that lean3's

class is_free_group (G : Type u) [group G] :=
(generators : Type u)
(mul_equiv [] : free_group generators ≃* G)

has become

class IsFreeGroup (G : Type u) [Group G] where
  Generators : Type u
  MulEquiv : FreeGroup Generators ≃* G

with the G implicit in the second version but explicit in the first version.

[Adam Topaz]

It doesn't really make sense to rename to MulEquiv' and add a separate def since we also have docs#is_free_group.to_free_group

[Eric Rodriguez]

I'd just do that, see for example docs4#Countable.exists_injective_nat

[Eric Rodriguez]

and maybe we should make a lean4 feature request

[Eric Rodriguez]

i think it was removed because the syntax was weird (and it is) but the feature is useful still

[Jireh Loreaux]

And see what I just did for docs4#Bornology

[Adam Topaz]

yeah okay, I made a separate def. But it still feels wrong.

[Adam Topaz]

anyway, the PR should be ready to review

[Jireh Loreaux]

I know, it felt wrong to me too, but if we can completely avoid the primed versions (by fixing the simps projections and the ext lemmas), then it should work; it's just a headache. Worst case, if you ever end up with a primed version, you can rewrite backwards with the equation lemma for the non-primed version.

[Yury G. Kudryashov]

I have the same issue with docs#fiber_bundle. Using primed versions (or defs in the root namespace instead of export) seems wrong because we have instances involving this data. What should I do? Use reducible defs a.k.a. abbrevs? Something else? @Mario Carneiro @Gabriel Ebner ?

[Yury G. Kudryashov]

BTW, how should I #align these definitions/theorems?

[Eric Wieser]

I think you should align the things that actually have the same signature

[Eric Wieser]

So that would mean the auxiliary def in lean 4 against the projection in lean 3