How does Lean filter simplification rules?

Stream: new members

[Mr Proof]

When you apply the simp tactic, I'm wondering what the algorithm is to filter which simplification rules to try. I'm just fascinated by how it works so quickly. :thinking: Given there are thousands of rules.

The way I'd probably go about it, if I were to attempt to implement it might be:

• Order simplification rules from smallest to largest
• Create a dictionary of every atomic term in every simplification rule. e.g. "zero"=0, "S"=1, "add"=2
• Against each word store the number of each simplification rule that contains that word (reverse index)
• Sort dictionary by rarest word to most common
• Precompute the set of atomic terms for each simplification rule.
• Translate those into numbers from the dictionary. So the expression might have R[3]={3,6,4,14}
• Collect a set of the atomic terms in the expression. e.g. E= {5,6,11,17}
• Using the reverse index start with the rarest word and start filtering the rules.

• Try each rule from the filtered list in turn until find a match.

• Could possibly do something clever by noting which parts of the formula had changed. e.g. it would be no good trying to match a sub expression in the same place again if that part of the tree hadn't changed.

• Repeat

Is this something close to what's done? Or is it more heuristically based?

Maybe filtering the sentences would actually be more costly than just trying each one at each point in the tree.

[Bolton Bailey]

I do not know much about it, but I believe a keyword search term is "discrimination tree".