Performance of simplifyer

Stream: general

[Andrew Yang]

I have no idea how simp works, but in my mental model, the simplifier keeps track of some table, matching each symbol to a list of simp lemmas having that symbol as the head symbol of the LHS, and trying them one by one.

The caveat is that there are hundreds if not thousands of simp lemmas (including auto-generated ones) with category.comp as the head symbol of the LHS, and I imagine (with evidence from the output of set_option trace.simplify true) that the simplifier is trying every one of them each time they see a category.comp.

My main problem is that I just added a bunch more simp lemmas regarding some new morphisms that I newly defined, and I might just have pushed simp over the brink of deterministic timeouts, forcing me to change the proofs of a dozen lemmas from by { delta foo, simp }to a four line simp only ..., which is both time consuming (for me) and aesthetically unappealing.

[Andrew Yang]

Is there a better way out?
I'm thinking if putting all the new simp lemmas into a custom simp attribute might help.

[Arthur Paulino]

Does simp support some kind of hint that might improve that ordering?

[Andrew Yang]

If there is a way to simp only [namespace] or simp only [prefix] I think the resulting fix for the timeout wouldn't look that scary as well.

[Kevin Buzzard]

The group and continuity tactics I think use a "custom simp set" and perhaps this is what you might want here. tactic#group

[Kevin Buzzard]

Oh! You can't jump to source with tactics! docs#tactic.interactive.group

[Kevin Buzzard]

Hmm, looks like I'm totally wrong. My mental model of the group tactic was simp only [list of 10 lemmas which Knuth and Bendix prove will do the job]. Anyway, hopefully a custom simp attribute can be used to solve this.

[Andrew Yang]

Looking at aux_group₁, I don't think your mental model of group is that far off.

[Andrew Yang]

Trying out the custom simp attribute approach.
Does reassoc preserve the custom simp attributes of the original lemma or does it only preserves simp?