!4#4852 heartbeats of the linter

Stream: mathlib4

[Moritz Firsching]

I'm seeing the following error, but only in the ci, locally with #lint in the file there are 0 errors.

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Topology.ContinuousFunction.Ideals
Error: ./Mathlib/Topology/ContinuousFunction/Ideals.lean:203:1: error: ContinuousMap.idealOfSet_of_ideal_eq_closure.{u_2, u_1} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  IsClosed ↑I
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

Any ideas how to fix it? (Or before that perhaps reproduce it locally?)

[Moritz Firsching]

I tried to disable it, adding nolint simpNF, which worked in one case, but not in the other.
Really a bit strange.

[Jireh Loreaux]

I've diagnosed the problem as being the result of the simp lemma docs4#Ideal.closure_eq_of_isClosed. The problem is that in this lemma isClosed (I : set R) is an instance argument. In doing simpNF linting on ContinuousMap.idealOfSet_ofIdeal_eq_closure, Lean applies simp which sees the Ideal.closure I and tries to apply Ideal.closure_eq_of_isClosed, which makes it go looking for an isClosed I instance. With all the hypotheses in the context of ContinuousMap.idealOfSet_ofIdeal_eq_closure, Lean spends too much time failing to find this instance (because it honestly can't, but it takes a long time to figure that out).

I suspect that the issue is that docs4#Ideal.closure_eq_of_isClosed should just take the isClosed argument explicitly instead of as an instance, and it should not be marked simp. I expect this would be a problem that could crop up repeatedly. Thoughts?

[Jireh Loreaux]

I think this doesn't show up with #lint in the file Topology.ContinuousFunction.Ideals by itself only because the class hierarchy isn't as large. The simpNF linter only needs set_option synthInstance.maxHeartbeats 26000 in order to succeed here, so it isn't a huge timeout.

[Yaël Dillies]

Why is IsClosed a typeclass in the first place ? Shouldn't we just use [Fact (IsClosed s)]?

[Mario Carneiro]

that looks strictly worse to me

[Jireh Loreaux]

I'm not sure exactly why it was done originally, but one way it's important is that when you quotient a Banach space by a closed subspace, you want to conclude it is normed, not just seminormed. And if you want this to be an instance, you need the fact that the subspace is closed to be an instance too.

[Jireh Loreaux]

FYI: I've made the change I suggested above and marked it awaiting-review

[Sebastien Gouezel]

IsClosed is a typeclass precisely because it is what is needed to make sure that one gets a norm on the quotient, and it's important that typeclass inference can find it. fact would also work, but it is just worse because there it is a completely generic instance, so it would be harder to find.