!4#3119

Stream: PR reviews

[Scott Morrison]

Following up on propose, this PR adds a rewrites tactic, which will print a list of all available rewrites on the current goal, along with the results.

It uses a discrimination tree, looking up all subexpressions of the goal, to find candidate lemmas, and then tries them out.

After !4#3404 is merged (instant start-up for library_search) I can implement the same caching strategy for propose and rewrites.

It would be lovely (but not in this PR!) for someone to write some basic premise selection code, available in mathlib, that could help inform which rewrites to attempt.

If this proves useful we can easily implement rewrites at h, as well. There is a MetaM level plumbing tactic provided if anyone wants to use this as a component of other tactics.

[Kevin Buzzard]

I'm staring at a broken simp proof in a porting file thinking that this feature would be really great to have right now :-)