Pi instance names in Lean 4 core

Stream: lean4

[Bhavik Mehta]

The instances docs3#pi.inhabited and docs3#pi.subsingleton are auto-named in Lean 4 core, and called docs#instInhabitedForAll_1 and docs#instSubsingletonForAll instead - a few porting notes also comment on this. Would it be sensible to try to rename these? I'd be happy with a mathlib alias or a change in core, since we do have docs#Pi.Fintype and docs#Pi.Nonempty

[Scott Morrison]

@Bhavik Mehta, could you add them as aliases in mathlib, with a link to lean4#2343?

[Eric Wieser]

Is there any reason not to rename these in core, besides being a waste of reviewer time? At this point I've probably spent more time trying to figure out if alias is safe for instances...

[Scott Morrison]

Sorry about this. Just the usual answer: reviewing external PRs at Lean4 is still occupying more time that we have available for it, so wherever possible if fixes can be done downstream we'd prefer that.

Renaming instances by hand is time that could be spent on lean4#2343 instead. :-)

[Bhavik Mehta]

Coming back to this, is this still the best way forward? The previously mentioned issue lean4#2343 is closed, but the names here are still the sub-optimal ones, and there are still outstanding porting notes for this.

[Kim Morrison]

@Bhavik Mehta, yes, I'm happy to rename these. Could you either tell me exactly what you want changed, or make a PR?

[Bhavik Mehta]

Yes:

The instance

instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
  Nonempty.intro fun _ => Classical.ofNonempty

on line 760 in lean/Init/Prelude.lean should have name Pi.instNonempty.

The instance

instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
  default := fun _ => default

on line 769 in lean/Init/Prelude.lean should have name Pi.instInhabited.

The instance

instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
  allEq f g := funext fun a => Subsingleton.elim (f a) (g a)

on line 1840 in lean/Init/Core.lean should have name Pi.instSubsingleton.

There are also instances on lines 757 and 766 which appear - to me - unnecessary, but I'll leave the question of what to do there up to you.

[Kim Morrison]

@Bhavik Mehta, lean#5447

[Bhavik Mehta]

Thank you! I expect that the mathlib breakage here should be easy to fix, but regardless I'm happy to help with fixing it in any way

[Kim Morrison]

There were no breakages, I think. Oops, indeed some, but minor.