Negative simp sets?

Stream: Is there code for X?

[Robert Maxton]

Is there a way to _remove_ a set of lemmas from a simp in one batch? A negative simp set, essentially?

I ask because specifically, there are a solid two to four ways for simp to get from an applied categorical composition (expression of the form Hom.hom (f ≫ g) x) in TopCat to a sequence of applied homs (Hom.hom g (Hom.hom f x)). This almost never works is and is almost never what I want; it could theoretically be patched by sufficient elementwise/_apply lemmas but those almost always seem to get hung up on definitional equalities or discrimination tree details so that they don't trigger as simp lemmas, so I find myself typing a whole lot of simp [-ConcreteCategory.comp_apply, -TopCat.hom_comp, -ContinuousMap.comp_apply]...

(It might also be a good idea to just de-simp some of these lemmas, but they mostly exist for decent reasons and it's only this unfortunate intersection of use cases where they go wrong, is my feeling.)

[Robert Maxton]

(Actually, maybe just making ConcreteCategory.comp_apply a simp↑ lemma, so that it tries to simplify on the categorical level first, then tries to simplify elementwise? Or a simproc that tries to go back and forth until it doesn't make progress, maybe?)

[Violeta Hernández]

Assuming that there are legitimate reasons for the lemmas to be simp, I think the best solution is a local attribute [-simp].

[Violeta Hernández]

Had to do something similar with WithTop.coe_add and WithTop.coe_mul once. Both are perfectly legitimate simp lemmas, but I was using them in a context where I only cared about the ordering on my WithTop (R[X]) type and not the arithmetic, so they were firing on my polynomials and giving me nonsense expressions.