Zulip Chat Archive

Stream: general

Topic: simp_attr


view this post on Zulip Kenny Lau (Sep 11 2018 at 11:16):

I think simp_attr is a great idea that will help us speed up many proofs and that we should use this extensively. What do you think?

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:17):

if we tag a bunch of lemmas with a certain attribute, then we can avoid having simp to try every simp lemmas, but only the lemmas with a certain attribute

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:18):

so maybe you have a bunch of simp lemmas associated with perfectoid spaces, then you can tag them all with an attribute [perfectoid], and then if you say simp only with perfectoid then simp will only try those lemmas

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:18):

@Mario Carneiro @Johannes Hölzl is this understanding correct?

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:24):

Yes, this is what the simp_attr attribute is for. I'm just not sure what a good way of splitting the simp set is. Also I'm not sure where the simplifier loses a lot of time. One problem might acutally building up the simpset, which get more expensive when do not use the standard simp set, but add our own! The simp lemmas are indexed by their head symbol. The simplifier looks at the current position and has a fast way to select all possible rewrite rules for the current head symbol. So the simplifer does not necessarily get slower with a lot of simp lemmas.

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:24):

@Kevin Buzzard I think you would like this. A long time ago you talked to a student about speeding up simp

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:25):

@Johannes Hölzl from my experience, a single simp application can take 2000 ms, while a simp only will only take 300 ms

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:25):

but simp only will get long, so if we have a set set of simp rules for a particular purpose, then we can make it shorter while still preserving the speed

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:26):

You don't know where the simplifier loses its time. It might very well be that it checks a lot of simp lemmas, but it might also be that it is the construction of the simp set itself.

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:26):

what do you mean that building the simpset will get more expensive when [we] do not use the standard simp set?

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:28):

My guess is: adding a couple of rules to the standard simp set is a fast operation, copying and adding a couple of new entries to a hash table should be a fast operation. But merging multiple simp sets (i.e. hash tables) with a lot of clashing head symbols could be expensive in itself.

view this post on Zulip Sean Leather (Sep 11 2018 at 11:29):

from my experience, a single simp application can take 2000 ms, while a simp only will only take 300 ms

I've seen the same thing. Consequently, I've occasionally considered looking through mathlib and replacing easy simps with simp only to speed up the build.

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:29):

I should say that this is just a guess. I only roughly know how the simplifier manages its simp set.

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:30):

I would be very careful with the 2000ms number. In my experience this is only the case if the simp set is not cached. So if you work interactively you often run into this case. If you run the theory in batch mode it is usually cashed from the previous tactic calls.

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 11:31):

I remember some instances where Lean told me that the simplifier needed 1s or 2s to build its simp set, but it didn't show up in the batch run.

view this post on Zulip Sean Leather (Sep 11 2018 at 11:31):

I don't work interactively. I only run lean --make.

view this post on Zulip Sean Leather (Sep 11 2018 at 11:32):

I should say that I was referring to the relative time difference, not the specific times that Kenny found.

view this post on Zulip Reid Barton (Sep 11 2018 at 11:32):

It could also be that the lemmas we could easily exclude by switching to a specialized simp set are ones which simp can immediately or cheaply reject based on the types not matching anyways.

view this post on Zulip Kenny Lau (Sep 11 2018 at 11:33):

so if we have a specialized simp set, the things inside can't be immediately or cheaply rejected?

view this post on Zulip Reid Barton (Sep 11 2018 at 11:59):

Well it may turn out that way--if you're trying to prove a statement in topology then excluding lemmas about rings from the simp set may not save very much time

view this post on Zulip Reid Barton (Sep 11 2018 at 11:59):

I'm not sure.

view this post on Zulip Reid Barton (Sep 11 2018 at 12:03):

It could depend on how you form the smaller simp sets.


Last updated: May 16 2021 at 21:11 UTC