aesop failed in NumberTheory/ModularForms/Cusps

Stream: mathlib4

[Lingyin Luo]

Hello!

While working on my PR 32152
and after applying the reviewer's suggestion which registering the finiteness proof of abelian simple group as an instance since Finite is itself a type class, I noticed aesop in the lemma in NumberTheory/ModularForms/Cusps failed:

lemma strictWidthInfty_nonneg : 0 ≤ 𝒢.strictWidthInfty := by
  unfold strictWidthInfty
  aesop

with error report

split failed:
failed to synthesize DiscreteTopology ↥𝒢.strictPeriods

I guess it is because the definition of strictWidthInfty branches on if h : DiscreteTopology 𝒢.strictPeriods then ... else 0, and relying on automation to split this seems quite sensitive to the typeclass environment?

Replacing the proof with an explicit case split makes it stable and mathlib build successfully again.

lemma strictWidthInfty_nonneg : 0 ≤ 𝒢.strictWidthInfty := by
  unfold strictWidthInfty
  by_cases h : DiscreteTopology 𝒢.strictPeriods <;> simp [h]

Would it make sense to patch the lemma in this direction?
I’m very happy to open a small PR if we agree it’s preferable.

Thanks!

Add @David Loeffler as the author of NumberTheory/ModularForms/Cusps
Add @Johan Commelin as my PR viewer

[Andrew Yang]

For context, this PR adds instance [CommGroup α] [IsSimpleGroup α] : Finite α.
I think this is not a good instance for performance reasons.

[David Loeffler]

I wouldn't have any great objection to patching this one specific proof of strictWidthInfty_nonneg; but it seems a bit worrying that 32152 causes automation that worked before to stop working, and makes me concerned that it might also be impacting other code elsewhere.

[Johan Commelin]

I also just made this remark on the PR, but @Andrew Yang do you think a scoped instance would be appropriate? Or should it just be a theorem?

[Kevin Buzzard]

Perhaps another reason why it's not a good instance is -- although it's true, can one ever imagine it being useful in practice? And conversely can one ever imagine it being misleading to typeclass inference? Maybe it should just have low priority? Right now we might be a victim of "defined late on and therefore tried first".

[Kim Morrison]

This should definitely not be a global instance! It will fire on every single type, and initial searches for CommGroup structures..

[Lingyin Luo]

For motivation of this PR : it comes from an exercise in Algebra Dummit–Foote 3.4.1, where the isomorphism between a nontrivial abelian simple group and ZMod p is stated with the explicit remark not to assume finiteness. This made me realise that the finiteness can actually be derived from the assumptions, which is why I added the corresponding lemma in mathlib.

[Yaël Dillies]

Johan Commelin said:

should it just be a theorem?

IMO yes, it should just be a theorem. Mathematically, this is not the sort of inference one is expecting to happen automatically.

[Kevin Buzzard]

Lingyin Luo said:

For motivation of this PR : it comes from an exercise in Algebra Dummit–Foote 3.4.1

Sure -- we understand the reason why we might want it to be a theorem in mathlib; the discussion here is a technical non-mathematical question about whether we want to add the theorem to the typeclass inference system by upgrading it from a theorem to an instance (with the answer being that we probably don't).