Nonempty regression

Stream: mathlib4

[Patrick Massot]

Next regression in trying to bump MIL to 4.8.0:

import Mathlib.GroupTheory.Index

open Fintype Classical

lemma aux_card_eq {G : Type*} [Group G] {H K : Subgroup G} [Fintype G]
    (h' : card G = card H * card K) : card (G ⧸ H) = card K := by
  have := calc
    card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card]
    _                     = card K * card H := by rw [h', mul_comm]

  have foo : Nonempty H := One.instNonempty
  exact Nat.eq_of_mul_eq_mul_right card_pos this

used to work with the have foo. Any idea?

[Matthew Ballard]

That might be more recent: see eg the most recent commit #12386

[Patrick Massot]

Sorry, I got distracted by something else on this website. I don’t understand what you mean. Did you quote the PR you intended to quote?

[Matthew Ballard]

Just saying after the bump that working PR had a nonempty regression also

[Riccardo Brasca]

Yes, I had the same problem, a nonempty instance is not found anymore.

[Riccardo Brasca]

In my case it is a very low priority instance (20 I think, I don't if this matters)

[Jireh Loreaux]

Wasn't there some talk of disabling a bunch of these generic instances (for Nonempty, Subsingleton, etc.) for performance reasons? Did that happen?

[Jireh Loreaux]

Or scoping them.

[Patrick Massot]

I see how this could impact performance but again it would be really sad if Lean needs help to figure out that a group is not empty.

[Patrick Massot]

I totally get that we don’t want to prove a type is not empty by chasing a module structure over an unspecified ring. But a group, please…

[Patrick Massot]

Note that the foo line is quoting docs#One.instNonempty that is indeed an instance

[Yaël Dillies]

Jireh Loreaux said:

Wasn't there some talk of disabling a bunch of these generic instances (for Nonempty, Subsingleton, etc.) for performance reasons? Did that happen?

No, Kyle created docs#Lean.Meta.FastSubsingleton, docs#Lean.Meta.FastIsEmpty instead

[Patrick Massot]

And I’m pretty sure that going from Group to One is also a global instance.

[Jireh Loreaux]

I think this is the message I had in mind.

[Patrick Massot]

And the priority of docs#One.instNonempty is indeed very low (20).

[Patrick Massot]

For people who did’t try the snippet, the trace is

[Meta.synthInstance] ❌ Nonempty ↥H ▼
  [] new goal Nonempty ↥H ▶
  [] ❌ apply instNonemptyElemCommutatorSet to Nonempty ↥H ▶
  [] ❌ apply @Finset.instNonemptyElemToSetInsert to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyRange to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyElemImage to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Iio_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Ioi_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Iic_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.nonempty_Ici_subtype to Nonempty ↥H ▶
  [] ❌ apply @Set.instNonemptyElemInsert to Nonempty ↥H ▶
  [] ❌ apply @Set.univ.nonempty to Nonempty ↥H ▶
  [] ❌ apply @nonempty_lt to Nonempty ↥H ▶
  [] ❌ apply @instNonemptyOfMonad to Nonempty ↥H ▶
  [] ✅ apply @instNonemptyOfInhabited to Nonempty ↥H ▶
  [] ✅ apply @Subtype.instInhabited to Inhabited ↥H ▶
  [resume] propagating (x_0 : G) → x_0 ∈ H → Inhabited ↥H to subgoal Inhabited ↥H of Nonempty ↥H ▼
    [] size: 1
    [] skip answer containing metavariables instNonemptyOfInhabited

[Patrick Massot]

So I think this must be related to the idea of not trying harder when something failed.

[Patrick Massot]

Here Lean thinks instNonemptyOfInhabited is promising, this fails and nothing else is tried? or something else?

[Patrick Massot]

I have no idea what the propagating part is about.

[Patrick Massot]

I’m blind. Lean was trying to tell me who is guilty here: it’s docs#Subtype.instInhabitedSubtype. How can this be an instance?

[Kyle Miller]

@Jireh Loreaux I only noticed mathlib4#12445 as a change to the Subsingleton instances (which sped up compilation by about 0.8%)

[Patrick Massot]

I guess this instance never ever fired, but it was ignored until the recent changes.

[Patrick Massot]

It was added four years ago!

[Patrick Massot]

Kyle, could you bring this up in the FRO?

[Patrick Massot]

I could produce a Mathlib-free example but hopefully looking at the instance in isolation is enough?

[Kyle Miller]

Patrick Massot said:

It was added four years ago!

Even better, Jeremy added it 10 years ago! https://github.com/leanprover-community/lean/commit/3afad10a7294fd183f66cc9d4723511b799ac4ff#diff-4e22e2bb74f004d2ff7cdabcb5c01429abbc906e20befe2517679e257b4387e4R41

and then Leo made it an instance shortly after: https://github.com/leanprover-community/lean/commit/8743394627865655d2aa83522f326f8b3ce8bd73#diff-c9d2d4fb99a5e01195239dfdfaf733704ef95daf710493cc3c5125a6445f198bR42

It's been copied from Lean version to Lean version ever since.

[Patrick Massot]

And still some people manage to complain Lean is not stable enough. I don’t know what it would take to please them…

[Kyle Miller]

I'm curious to see if removing this instance will have any affect on mathlib benchmarks. Draft: lean4#4055

[Kevin Buzzard]

I love that lean is still such an adventure! We are still discovering ways to make the software better.

[Mario Carneiro]

Patrick Massot said:

I’m blind. Lean was trying to tell me who is guilty here: it’s docs#Subtype.instInhabitedSubtype. How can this be an instance?

Why didn't the impossibleInstance linter catch this?

[Eric Wieser]

Probably because the linter only runs against mathlib?

[Riccardo Brasca]

So in practice is it ok to add the instance by hand at the moment?

[Patrick Massot]

Do you mean remove? Yes you can remove it by hand, this is what I did in MIL.

[Eric Wieser]

If this is a regression and the fix is a simple upstream deletion, can we backport this so that it ends up in rc2?

[Kyle Miller]

Something I was trying to do with lean4#4055 was benchmark the removal on mathlib, but I'm not sure what the right way to do it is (and as you can see from the PR, there's a bunch of force pushes as I tried to get all the lean-pr-testing branches on the right versions). I think it could be merged right away, but I'm curious.