Using `inferInstance` as partial fills in instance defs

Stream: mathlib4

[Yakov Pechersky]

Consider:

instance : Group αˣ :=
  { (inferInstance : MulOneClass αˣ) with
    one := 1,
    mul_assoc := fun _ _ _ => ext <| mul_assoc _ _ _,
    inv := Inv.inv, mul_left_inv := fun u => ext u.inv_val }

In mathlib3, we often refer to explicit instance names when doing such partial fills. In lean4, the anonymous instance names are pretty different, and have to be guessed or retrieved via a #synth. Is there a downside (defeq issues?) to using inferInstance as I have above?

[Scott Morrison]

I think it's okay. If anything it's more informative to have the type here than the term! Hopefully also without old_structure_cmd we may be able to omit more of these anyway...?

[Alex J. Best]

Side note: you can use docs4#inferInstanceAs here instead

[Gabriel Ebner]

And you can also use the __ := shorthand syntax:

instance : Group αˣ where
  __ := inferInstanceAs (MulOneClass αˣ)
  one := 1
  -- ...

[Patrick Massot]

Is there any documentation for this syntax?

[Gabriel Ebner]

Of course, but probably not in the place you'd be looking for. https://github.com/leanprover-community/mathlib4/blob/df8292b7dbdb00bfa90d626ba7c83af2eff1ce37/Mathlib/Tactic/Spread.lean#L14-L24

[Patrick Massot]

So this is what was denoted by .. in Lean 3?

[Gabriel Ebner]

Yeah, it simulates that.

[James Gallicchio]

(Is there a reason to use this instead of { e with one := 1 }?)

[Scott Morrison]

@James Gallicchio, I think the point of this thread is when you don't have a term such as e readily at hand, and want typeclass search to find it for you.

[Mario Carneiro]

although that doesn't quite answer the question since inferInstanceAs (MulOneClass αˣ) is exactly such an e

[James Gallicchio]

Can you have multiple __ operators in a single structure? i.e. is it a generalization of the with syntax?

[Mario Carneiro]

I believe the answer is that when Mathlib.Tactic.Spread was written structures could only have one explicit source { e with ... }

[Mario Carneiro]

this restriction has since been lifted, so it's possible that it is not needed anymore except that the where syntax shown above does not accept explicit sources

[James Gallicchio]

I wonder if we can merge these syntaxes. I wouldn't mind the { e with ...} syntax changing, honestly, since it doesn't really suggest that multiple sources can be used (which I think the __ := syntax actually does)

[Gabriel Ebner]

Yes, you can have multiple __ := fields.

[Gabriel Ebner]

{ __ := a, __ := b } is desugared into { a, b with }. The advantage of __ := is that you can also use it in where-blocks.

[Gabriel Ebner]

(Side note: before multiple explicit sources were allowed, the expansion of __ := was a lot more complicated.)