simps and simpNF linter

Stream: mathlib4

[Johan Commelin]

It looks like in category theory (where we use a lot of simps) there are many complaints by the simpNF linter about lemmas generated by simps. Can we make the linter less strict?

[Johan Commelin]

See e.g.: https://github.com/leanprover-community/mathlib4/pull/2206/files#diff-67a442ca7af88b3eaf1884a67020cd1ad87fcc27122f52efd091fc0297346030R173-R195

[Reid Barton]

What lemmas is it generating? Hard to imagine how they could trigger the linter

[Reid Barton]

Unless the projections themselves are not in simp NF?

[Johan Commelin]

In https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/CategoryTheory.2EAdjunction.2EBasic 6/8 complaints are "simp can prove this". That could mean that we can just remove simps. But I don't think that's desirable.

I have not yet looked in detail into the complaints in the PR linked in OP.

[Reid Barton]

That is also hard to understand, unless one simps lemma is a prefix of another?

[Johan Commelin]

Yeah, I agree. It is also hard to see how it could be problematic.

[Reid Barton]

Maybe there are more simp lemmas getting later which interfere?

[Johan Commelin]

Here another example that Yury just pointed out to me:
On the branch YK-coe-fn-grp go to the file GroupTheory.Subsemigroup.Operations and add

example (e : M ≃* N) (S : Subsemigroup M) (x : { x // x ∈ Subsemigroup.map (MulEquiv.toMulHom e) S }) :
    ((MulEquiv.symm (MulEquiv.subsemigroupMap e S)) x) = (MulEquiv.symm e) x :=
  by simp

all the way at the bottom of the file, but just before the end MulEquiv. You'll get a nasty timeout.
Whereas simp should just find MulEquiv.subsemigroupMap_symmApply_coe, and indeed if you feed that lemma to simp only then all is fine.

[Floris van Doorn]

This likely happens because of misconfigured initialize_simps_projections. Note that !4#2042 and !4#2045 are improving the default behavior for Lean 4 and fixing a bunch of them.