Commit 2021-01-06 11:04 137a6e0f

feat(tactic/rewrite_search): Automatically searching for chains of rewrites (#4841) This pull request is based on a branch originally developed by @semorrison , @khoek , and @jcommelin . The idea of rewrite_search is a tactic that will search through chains of potential rewrites to prove the goal, when the goal is an equality or iff statement. There are three key components: discovery.lean finds a bunch of rules that can be used to generate rewrites, search.lean runs a breadth-first-search algorithm on the two sides of the quality to find a path that connects them, and explain.lean generates Lean code from the resulting proof, so that you can replace the call to rewrite_search with the explicit steps for it. I removed some functionality from the rewrite_search branch and simplified the data structures somewhat in order to get this pull request small enough to be reviewed. If there is functionality from that branch that people particularly wanted, let me know and I can either include it in this PR or in a subsequent one. In particular, most of the configuration options are omitted. For data structures, the whole table data structure is gone, replaced by a buffer and rb_map for efficient lookup. Write access to the buffer is also append-only for efficiency. This seems to be a lot faster, although I haven't created specific performance benchmarks.