simp_attr

Stream: general

[Kenny Lau]

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?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

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.

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

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.

[Kenny Lau]

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

[Johannes Hölzl]

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.

[Sean Leather]

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.

[Johannes Hölzl]

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

[Johannes Hölzl]

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.

[Johannes Hölzl]

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.

[Sean Leather]

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

[Sean Leather]

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

[Reid Barton]

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.

[Kenny Lau]

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

[Reid Barton]

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

[Reid Barton]

I'm not sure.

[Reid Barton]

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