rewrites tactic, !4#3119

Stream: PR reviews

[Scott Morrison]

It seems I didn't make a thread about this.

!4#3119 adds the rewrites tactic which is to rw what library_search is to exact/refine and propose is to have: it attempts to find lemmas which can rewrite the current expression. It uses a discrimination tree to index lemmas, so is not simply trying everything in the library.

The PR is not actually that complicated. It is mostly just boilerplate copying the framework of library_search, beyond:

• adding getSubexpressionMatches in Mathlib/Lean/Meta/DiscrTree.lean
• initialize rewriteLemmas in Mathlib/Tactic/Rewrites.lean which collects the lemmas
• rewritesCore in the same place, which decides what order to try them in.

If we can merge this, I will do some cleanup work moving some of the goodies library_search has received lately over to propose and rewrites. (!4#3771, !4#3743, !4#3725, !4#3720, !4#3404)

Later I'd like to add rewrites at h functionality, and possibly with widgets, support for rewriting subexpressions by selecting them in the goal view.

[Eric Wieser]

Does this replace lean 3's docs#tactic.interactive.rewrite_search?

[Scott Morrison]

No. The rewrite_search in mathlib3 was a partial re-implementation of a nice but unmergeable rewrite_search that a student and I wrote a long time ago... rewrites in !4#3119 just does one rewrite. It's purpose is to hint to the user things they might do.

That said, the plumbing underneath it (finding all possible rewrites at a point) would be helpful for writing a new rewrite_search, and I would like to see that happen sometime!