Syntax for unpacking structures

Stream: mathlib4

[Adam Topaz]

What's the correct syntax to unpack a structure in Lean4/Mathlib4?
For instance, the lean3 code

instance {R M N : Type*} {r : monoid R} [add_monoid M] [add_monoid N]
  [distrib_mul_action R M] [distrib_mul_action R N] : distrib_mul_action R (M × N) :=
{ ..prod.distrib_smul }

is converted by mathlib3port into

instance {R M N : Type _} {r : Monoid R} [AddMonoid M] [AddMonoid N] [DistribMulAction R M]
    [DistribMulAction R N] : DistribMulAction R (M × N) :=
  { Prod.distribSmul with }

which doesn't work.

[Floris van Doorn]

Is it possible that the instance name has changed? That syntax should work otherwise.

[Adam Topaz]

oh, that's probably it...

[Adam Topaz]

the auto-generated name is instDistribSMulProdInstAddZeroClassSum :face_palm:

[Kevin Buzzard]

This reminds me of German lessons

[Ruben Van de Velde]

I'd suggest you go back and give the instance an explicit name

[Adam Topaz]

I asked this before re porting this file (group_theory/group_action/prod) and the answer was to keep the auto-generated name (which is how it's currently done in lean3)

[Ruben Van de Velde]

Or replacing the name by inferInstanceAs (...), but I think we didn't like that?

[Floris van Doorn]

I think this is a real issue.
These names get exponentially long, since they include other instance names occurring in the type. I'm worried that automatically generated instance names will get literally thousands of characters long...

[Kevin Buzzard]

People have definitely been renaming instances as per Ruben's first suggestion, in other ported files.

[Adam Topaz]

Is there a consistent naming convention for instances in mathlib4?

[Ruben Van de Velde]

I think we've been doing all possible options :)

[Floris van Doorn]

Adam Topaz said:

Is there a consistent naming convention for instances in mathlib4?

I'm quite sure that is a no

[Ruben Van de Velde]

Also { ‹DivisionRing α›, (inferInstance : Semiring α) with }

[Adam Topaz]

what's the naming convention for terms of prop-y typeclasses? E.g. distribMulAction : DistribMulAction seems natural to me, but is this correct?

[Adam Topaz]

BTW, @Floris van Doorn if you don't mind, could you take a look at mathlib4#1056 to make sure I ported all the to_additive stuff properly?

[Floris van Doorn]

Yes, it looks good, besides current limitations of the to_additive attribute. Note that for most declarations you can even do something like

@[simp, to_additive (reorder := 6)]
theorem pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c :=
  rfl
attribute [to_additive] smul_fst
#align prod.pow_fst Prod.pow_fst
#align prod.smul_fst Prod.smul_fst
#align prod.vadd_fst Prod.vadd_fst

@[simp, to_additive (reorder := 6)]
theorem pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c :=
  rfl
attribute [to_additive] smul_snd
#align prod.pow_snd Prod.pow_snd
#align prod.smul_snd Prod.smul_snd
#align prod.vadd_snd Prod.vadd_snd

then to_additive generates both the smul and the vadd lemma. It doesn't work for everything though, as discussed before. And the output of to_additive? is very misleading, since it only prints the proof term without the type of the lemma.

I'll try to support the more general reordering of arguments, so that we can properly translate pow_mk and other lemmas.

[Adam Topaz]

Yes I know I can cut things down, but I wanted to stay as close as possible to the mathlib3 file. I'll add a porting note note in the module doctring

[Thomas Murrills]

Adam Topaz said:

what's the naming convention for terms of prop-y typeclasses? E.g. distribMulAction : DistribMulAction seems natural to me, but is this correct?

I think that since DistribMulAction M A : Type is a structure at the end of the day, it makes sense to use lowerCamelCase for its terms/structure instances, in keeping with all other structure instances. The individual field projections (which have return types which are Props) are the things that will get named with snake_case. At least, that’s how it is under current naming conventions… :)

[Thomas Murrills]

Also, as it happens, I had this same issue with references to explicit instances while porting!

I wonder how widespread this issue will be during the port. It might be worth coming up with a standard way to rename instances (by at least making them shorter).

[Thomas Murrills]

How have people who have renamed instances renamed them so far?

[Adam Topaz]

okay, maybe distrib_mul_action was a bad example since it's not actually prop-y (I thought it was a mixin on top of mul_action, but it's not as it extends it). A better example is something like docs#local_ring

[Adam Topaz]

The class will be called LocalRing, and it takes values in Prop, but it's still a class. Would terms be named localRing or local_ring?

[Adam Topaz]

With Lean4 it seems like we use every single naming convention that exists. It's confusing.

[Adam Topaz]

My vote is for localRing as opposed to local_ring in this case.

[Thomas Murrills]

They would be named local_ring according to current conventions! Terms of things which are Props are always lower_snake_case. I was a bit overeager saying “like all other structure instances”—for a second I assumed all structures were Types 😅

[Thomas Murrills]

(Of course, we could change the conventions—I’m just reporting how they work as written right now.)

[Adam Topaz]

I don't recall seeing anything about naming terms of structures all of whose fields are props.

[Thomas Murrills]

Right; but this doesn’t use that, does it? It just refers to the fact that LocalRing … : Prop

[Adam Topaz]

It does. Classes are structures, and if all the fields of a structure are props, then the structure will take values in Prop as well

[Adam Topaz]

The naming convention listed on the porting wiki mentions that theorem names are snake-case. Yes in some sense the fact that a given ring is local is a theorem, but in practice we declare these as instances.

[Thomas Murrills]

I see—I am indeed thinking of conversations I’ve had about this, not the naming convention per se! In those conversations it was said that all that matters is whether the type of something’s type is Prop or not, however it gets there. You’re right, this is not in fact clear from the naming conventions as written as I thought.

[Thomas Murrills]

This is the conversation I’m thinking of

[Mario Carneiro]

yup, I agree with Thomas Murrills as far as my current understanding of the naming convention. Instance or no, if it's a proof it is snake cased

[Mario Carneiro]

If you are going to be at the meeting we can also bring it up for discussion though

[Thomas Murrills]

Actually, reading it explicitly, this is intended to be covered by the naming convention, but I see the confusion. In the following

1. Terms of Props (proofs, theorem names) are in snake_case.

we could afford an “e.g.” in the parenthetical (since terms of things which are Props aren’t always thought of primarily as proofs, even if they technically are). I’ll put it there now…

[Jireh Loreaux]

Hmmm.... I think according to the naming conventions, the class should be called LocalRing (by 2 on the wiki), and terms of this class are terms of som Prop, so they get snake_case by (1). However, by (5) this would lead to names like: Field.to_localRing, not Field.to_local_ring, or i_am_a_localRing, not i_am_a_local_ring. (maybe this was already said above, but if it was I didn't parse it correctly.)

[Ruben Van de Velde]

I thought instances always matched defs

[Kevin Buzzard]

I wish this was called IsLocalRing because it's a Prop

[Adam Topaz]

Floris van Doorn said:

I think this is a real issue.
These names get exponentially long, since they include other instance names occurring in the type. I'm worried that automatically generated instance names will get literally thousands of characters long...

It's happening...
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Submodule/Basic.html#Submodule.instIsScalarTowerSubtypeMemSubmoduleInstMembershipInstSetLikeSubmoduleRestrictScalarsToSMulInstZeroSubtypeMemSubmoduleInstMembershipInstSetLikeSubmoduleToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstAddCommMonoidSubtypeMemSubmoduleInstMembershipInstSetLikeSubmoduleOrigModuleInstSMulSubtypeMemSubmoduleInstMembershipInstSetLikeSubmoduleToSMulToZeroToMonoidWithZeroToSMulZeroClassToSMulWithZeroToMulZeroClassToNonUnitalNonAssocSemiringToNonAssocSemiringToSMulToZeroToAddMonoidToSMulZeroClassToSMulWithZeroToMulActionWithZeroLeftToMonoidToMulAction

[Johan Commelin]

At least it is completely straightforward to figure out what this instance is all about... :oops:

[Jireh Loreaux]

To be honest, I never understood why the auto-generated naming convention for instances changed. Sure, it wasn't perfect in Lean 3, but I thought it was reasonably good.

[Floris van Doorn]

I think we have a new record holder: docs4#Subalgebra.instIsScalarTowerSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSMulZeroToZeroToMonoidWithZeroToZeroMemClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToAddSubmonoidClassSubsemiringClassToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSubsemiringInstModuleSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToNonAssocSemiringToSubsemiringToSMulToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroModule'

Contenders are very easy to find in the docs, since their names matches almost anything :-)

[Kevin Buzzard]

The logic behind the change was to make the names more readable, right?

[Mario Carneiro]

I don't think so - I'm speculating but it's probably intended to capture more of the term so as to avoid name clashes, especially across imports since these can't be easily avoided and give a nasty error message in downstream files on import

[Mario Carneiro]

a hash would probably do a better job of solving that problem though

[Eric Wieser]

There's a thread at #mathlib4 > instance names too

[Eric Wieser]

Could we have chosen to keep the mathlib3 instance names in mathport, or is this information not easy to access?

[Mario Carneiro]

It is challenging to give #align lines for anonymous instances because we don't actually know what the lean 4 name will be in mathport

[Mario Carneiro]

mathport does keep the instance name if it is provided in lean 3

[Eric Wieser]

What I meant is, can the mathport output be instance theLean3GeneratedName?

[Mario Carneiro]

it doesn't know what lean 3 instance this bit of syntax corresponds to either

[Eric Wieser]

Is changing the AST to contain this information unreasonable?

[Eric Wieser]

Or just possibly not worth the effort

[Mario Carneiro]

that's blocked on some additional lean 3 data which synchronizes between the tlean and ast.json files

[Eric Wieser]

What's the relation between tlean and ast?

[Mario Carneiro]

it's also needed to be able to handle #aligns for simps, to_additive, alias etc

[Eric Wieser]

I thought we solved aligns for simps and to_additive?

[Mario Carneiro]

we have a special case hack for to_additive and simps changed its syntax to avoid the issue

[Mario Carneiro]

but there are lots of other user commands / attributes that can make definitions and we would like #align for all of them

[Eric Wieser]

It sounds to me like there would be a lot of value to adding the hack for instance in the short term, if the right solution is hard

[Mario Carneiro]

Eric Wieser said:

What's the relation between tlean and ast?

Roughly, the ast.json file has the AST structure, and the tlean has the compiled proof terms (i.e. the stuff that goes in the olean, but in a textual format)

[Mario Carneiro]

The fix I would like to do is to add a line in the tlean every time an (AST) command is completed, so that by counting commands we can say "all the generated declarations (in the tlean) between here and here belong to this AST command"

[Mario Carneiro]

because synport is iterating over AST commands while binport (which runs previously) iterates over the tlean

[Mario Carneiro]

In the case of an instance command, we can look for that list of declarations to find out what the lean 3 name is and insert it in the syntax

[Yaël Dillies]

Kevin Buzzard said:

The logic behind the change was to make the names more readable, right?

There sure is more to read!