Faster rewriting

[patrick-nicodemus]

The generalized rewriting tool is time intensive because it does a lot of unification comparisons on complicated terms.

An effective solution seems to be, for every rewrite command, replace every subterm of the goal with a variable if it is not directly relevant to the unification problem at hand.

For example, say you have the term (compose C0 c0 d0 e0 f g) in your goal, and you are trying to prove P(f \circ g), where C0, c0, d0, e0 are all explicitly given morphisms. You want to replace g with another morphism g' which is setoid-equivalent.
There is a theorem in the Proper database that says, for all categories C, c, d, e, and for all f, g, iff g \equiv g' then f \circ g \equiv f \circ g'. Because the theorem is uniform in the category C and c, d, e, you can write
set var1 := c0;
set var2 := C0;
set var3 := d0;
set var4 := e0
and the typeclass resolution algorithm will have a much easier time.

It is worth it to consider other possibilities, such as enabling certain flags in the typeclass unification algorithm.

In this PR, I define a tactic "hide" which accepts a pattern as argument. If it finds a match for this pattern in the goal, it replaces the matched term with a variable, "opaquing" it. There are two variants of this tactic depending on whether the pattern is a term t with holes (in which case it behaves like "set ( freshvar := t )" or whether the pattern contains a metavariable, in which case it behaves like "match goal with | [ |- context [ t(?z) ] ] => set (freshvar := z) end".
Each of these has two variants in turn according to whether we want to repeat the pattern match exactly n times or as many times as possible until it stops making progress.

All the tactics return a list of the new variable names created. Therefore, after executing the rewrite tactic we care about, we can apply an "unfold and clear all" function to this list of variables. If this is all done in one step then the temporary variables serving as masks are invisible to the user.

I rewrote one theorem proof in Constructions/Comma/Adjunction.v with 'hide' tacics to demonstrate the intended usage; I also illustrate a design pattern I am workshopping for combining the 'hide' tactic with rewriting. The gain in speed for a typical rewrite command is about 5-10x (from between 0.5 - 1.0 sec to ~ 0.1 sec)

Possible opportunities for improvement:

• A master function which accepts a list of flags which automatically enable a combination of common patterns to be opaqued, for example, one should be able to say easily by enabling a flag "hideCompose" that wherever a term "@compose ?Cat ?c ?d ?e _ _" appears in the goal, all the arguments Cat, c d and e should be replaced by variables.

I may add these in the future, this is just a proof of concept.

[jwiegley]

@patrick-nicodemus Hi Patrick, any further thoughts on this PR?