Named instance parameters

Stream: mathlib4

[Christian Merten]

Is there a policy on named instance parameters? Are they to be avoided in general or is it okay to skip some heartbeats? Example:

import Mathlib

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]

count_heartbeats in
example [hf : Module.Finite R M] : True := by
  obtain ⟨s, hs⟩ := hf
  trivial
-- 674 heartbeats

count_heartbeats in
example [Module.Finite R M] : True := by
  obtain ⟨s, hs⟩ := Module.Finite.out (R := R) (M := M)
  trivial
-- 979 heartbeats

The named instance parameter pattern is quite frequent in the Module.Finite, Algebra.Finite, Module.FinitePresentation etc. cases.

[Yaël Dillies]

Do you know you can do obtain ⟨s, hs⟩ := ‹Module.Finite R M›?

[Christian Merten]

Yaël Dillies said:

Do you know you can do obtain ⟨s, hs⟩ := ‹Module.Finite R M›?

I did not, thanks! Is this the same as obtain ⟨s, hs⟩ := (inferInstance : Module.Finite R M)? Heartbeat wise your suggestion is at 982.

[Johan Commelin]

‹Foo› is the same as (by assumption : Foo)

[Johan Commelin]

I think named instance params are fine.

[Yaël Dillies]

Heartbeats for ‹_› should be basically zero

[Christian Merten]

Yaël Dillies said:

Heartbeats for ‹_› should be basically zero

If more then 300 slower is "basically zero", then I agree (I guess compared to the max of 200000 it is indeed basically zero).

[Christian Merten]

Johan Commelin said:

I think named instance params are fine.

So is there a preference? Up to personal style or is the ‹_› variant preferred?

[Kyle Miller]

I don't think changing a proof to use a named instance argument is worth 300 heartbeats. I personally think it's better to only interact with instances through the typeclass system, since it helps ensure that you're only dealing with the instances you'd actually get through typeclass search. For a Prop-valued class this matters less, but it's the principle of it.

(It's a bit unfortunate that Module.Finite.out doesn't take its R and M arguments explicitly. I suspect this inconvenience is why you might see so many uses of explicit instances for Module.Finite.)

[Kim Morrison]

I would say a good rule of thumb is that if a heartbeat savings is less than about 10,000, it must come at no cost to readability.

[Eric Wieser]

Note also that naming instances doesn't just affect readability in your proof; it also changes how your lemma appears in the docs / when people hover over it.