Relying on instance names

Stream: mathlib4

[Wojciech Nawrocki]

There are places in mathlib (e.g. algebra.group.type_tags) which do the following thing:

instance [semigroup α] : add_semigroup (additive α) :=
{ add_assoc := @mul_assoc α _,
  ..additive.has_add }

instance [comm_semigroup α] : add_comm_semigroup (additive α) :=
{ add_comm := @mul_comm _ _,
  ..additive.add_semigroup }

where the definition of the latter instance depends on the auto-generated name of the former. Since the instance name generation changed in Lean 4, I am wondering what to do here. Since relying on autogenerated names is never a good idea, my intuition is to either

• manually name the first instance Additive.addSemigroup; or
• define the latter instance by

instance [CommSemigroup α] : AddCommSemigroup (Additive α) :=
  { inferInstanceAs (AddSemigroup _) with add_comm := @mul_comm α _ }

I am leaning towards the second option because it doesn't rely on any name, autogenerated or not. The only worry is that it picks up the wrong instance; but since in this particular case (Additive/Multiplicative) I think the instances should be canonical, maybe that is not a worry?

[Eric Wieser]

Doesn't inferInstanceAs create a different term (essentially with an id wrapper function)? Does it work for cases like ..foo.add_monoid, ..foo.monoid?

[Wojciech Nawrocki]

This example works:

instance [h : Monoid α] : AddMonoid (Additive α) :=
  { inferInstanceAs (AddZeroClass _), inferInstanceAs (AddSemigroup _) with
    zero := 0
    add := (· + ·)
    nsmul := @Monoid.npow α h
    nsmul_zero := @Monoid.npow_zero α _
    nsmul_succ := @Monoid.npow_succ α _ }

Relative to what mathport gave, I had to explicitly specify α in the last two fields since it was inferring Additive α, but that is an elaboration change for which the inferInstanceAs part doesn't seem to matter.

[Wojciech Nawrocki]

The original is:

instance [h : monoid α] : add_monoid (additive α) :=
{ zero     := 0,
  add      := (+),
  nsmul    := @monoid.npow α h,
  nsmul_zero' := monoid.npow_zero',
  nsmul_succ' := monoid.npow_succ',
  ..additive.add_zero_class,
  ..additive.add_semigroup }

[Eric Wieser]

Something else to consider when relying on generated names; referring to instances in docstrings such that #docs4 links them

[Wojciech Nawrocki]

Note that inferInstanceAs is an abbrev so there should be no extra function application. Looks like I made this up, apologies. There is a special definition kind and reducibility hint which are tracked.

[Eric Wieser]

Are abbrevs in Lean 4 unfolded immediately like coe? (in Lean 3 it was a bit less clear than that)

[Wojciech Nawrocki]

Eric Wieser said:

Something else to consider when relying on generated names; referring to instances in docstrings such that #docs4 links them

Here is an example autogenerated name.

[Eric Wieser]

My view here would be that we should teach mathport some heuristics to align instance names; because in the long term we can then use the resulting #align data to clear up instance-references in comments

[Eric Wieser]

I think @Mario Carneiro has expressed opinions related to this in another thread at some point

[Kevin Buzzard]

I'm interested in the answer to the original question because this evening I just ported a bunch of code by changing instance names to the new lean 4 instance names without even thinking that this might be a problem

[Scott Morrison]

Whenever a problem comes up that involves instance names, I've been adding manual names and using those.

[Scott Morrison]

I'd be happy with the inferInstanceAs solution.

[Jireh Loreaux]

I have also been using manual names. I actually prefer to name instances, just so we can refer to them if we want to (which does come up from time to time), or else have the autogenerated names be nice and predictable.

[Wojciech Nawrocki]

Alrighty, I will write down the manual lean3-style instance names when needed, despite this being less automated, since Eric is right to point out that they are not exactly the same term and iirc instances can be annoyingly sensitive to this kind of detail (it is unclear to me whether an abbrev, being "very-reducible", could cause issues; but just in case).

[Jireh Loreaux]

Would (inferInstance : insert-type-here) have the same problem as inferInstanceAs? I would expect not, but I could be wrong.

[Mario Carneiro]

Eric Wieser said:

My view here would be that we should teach mathport some heuristics to align instance names; because in the long term we can then use the resulting #align data to clear up instance-references in comments

The names are not really related by any kind of direct map. Lean 4 names take into consideration a lot more of the type and as a result they can be very long. The simplest way to do what you are suggesting would be to just run the instance name generator on the synthesized lean 4 type for any instance which is not named; but one difficulty with this is that binport is the one doing the naming (by going over the lean 3 environment) and synport is the one that knows whether the instance is named (because it goes over the lean 3 syntax), and binport runs first

[Mario Carneiro]

The fact that inferInstance inserts a literal term (an application of inferInstance which is an identity function) also bothers me. The synth_instance tactic is actually just sugar for exact inferInstance so it also introduces this extra term, and this is something we have to go to pains to avoid in the implementation of the ring/norm_num tactics

[Mario Carneiro]

It would be great if they could just magically disappear at elaboration time, but the magic for coe is specific to it and if we wanted to do something similar for inferInstance it would have to be a macro

[Wojciech Nawrocki]

Mario Carneiro said:

The fact that inferInstance inserts a literal term (an application of inferInstance which is an identity function) also bothers me. The synth_instance tactic is actually just sugar for exact inferInstance so it also introduces this extra term, and this is something we have to go to pains to avoid in the implementation of the ring/norm_num tactics

This is getting a little off-track but why is the extra term an issue for ring?

[Wojciech Nawrocki]

Since it has the abbrev reducibility hint, it's not quite the same from the typechecker's point of view as inserting id.

[Mario Carneiro]

it is an extra constant factor on the construction of expressions, and the typechecking of the result, and it's just an unnecessarily longer proof

[Mario Carneiro]

because we are talking about an additional identity function wrapping every single + and * and lemma inside the generated proof

[Jon Eugster]

In mathlib4#902 I've encountered a few instance names (in already ported files) that are rediculously long by default: instance WithBot.instNoTopOrderWithBotInstLEWithBot [LE α] [NoTopOrder α] [Nonempty α] : NoTopOrder (WithBot α) :=. Since I need to use them explicitely as above discussed, I wonder if there is an opinion on whether they should be manually shortened to WithBot.instNoTopOrder or just bite the bullet and spell out the name every time.

[Scott Morrison]

Please rename to just WithBot.noTopOrder.

[Kevin Buzzard]

By the way, another possibility which was under discussion recently was to avoid using the names completely and to use instance synthesis, but I tried this in Algebra.Group.WithOne.Defs and just found that it still made the code longer without any obvious gain. The long name is hilarious. Maybe this is just a transient issue -- I'm not sure that in the big theory files people are explicitly using instance names.

[Kevin Buzzard]

Re the renaming suggestion above -- you want no inst at all in the name?