rewrite_search: solving goals by searching for a series of rewrites. #

rewrite_search is a tactic for solving equalities or iff statements by searching for a sequence of rewrite tactic applications.

Algorithm sketch #

The fundamental data structure behind the search algorithm is a graph of expressions. Each vertex represents one expression, and an edge in the graph represents a way to rewrite one expression into another with a single application of a rewrite tactic. Thus, a path in the graph represents a way to rewrite one expression into another with multiple applications of a rewrite tactic.

The graph starts out with two vertices, one for the left hand side of the equality, and one for the right hand side of the equality. The basic loop of the algorithm is to repeatedly add edges to the graph by taking vertices in the graph and applying a possible rewrite to them. Through this process, the graph is made up of two connected components; one component contains expressions that are equivalent to the left hand side, and one component contains expressions that are equivalent to the right hand side. The algorithm completes when we discover an edge that connects the two components, creating a path of rewrites that connects the left hand side and right hand side of the graph. For more detail, see Keeley's report at https://hoek.io/res/2018.s2.lean.report.pdf, although note that the edit distance mechanism described is currently not implemented, only plain breadth-first search.

This algorithm is generally superior to one that only expands nodes starting from a single side, because it is replacing one tree of depth 2d with two trees of depth d. This is a quadratic speedup for regular trees; our trees aren't regular but it's still probably a much better algorithm. We can only use this specific algorithm for rewrite-type tactics, though, not general sequences of tactics, because it relies on the fact that any rewrite can be reversed.

File structure #

• discovery.lean contains the logic for figuring out which rewrite rules to consider.
• search.lean contains the graph algorithms to find a successful sequence of tactics.
• explain.lean generates concise Lean code to run a tactic, from the autogenerated sequence of tactics.
• frontend.lean contains the user-facing interface to the rewrite_search tactics.
• types.lean contains data structures shared across multiple of these components.