Zulip Chat Archive

Stream: general

Topic: Performance of simplifyer

Andrew Yang (Feb 12 2022 at 18:07):

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 (Feb 12 2022 at 18:09):

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 (Feb 12 2022 at 18:15):

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

Andrew Yang (Feb 12 2022 at 18:17):

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 (Feb 12 2022 at 18:30):

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 (Feb 12 2022 at 18:31):

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

Kevin Buzzard (Feb 12 2022 at 18:32):

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 (Feb 12 2022 at 18:39):

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

Andrew Yang (Feb 12 2022 at 18:40):

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

Last updated: Aug 03 2023 at 10:10 UTC