Implement Coq-style goal-matching tactic

[mn200]

An “ltac” is perhaps of the form

([hyppat1, hyppat2, ...], goalpat, 
 (fn ([matchvar1, matchvar2, ...], [hypth1, hypth2, ...], goalterm) => tactic))

where the hyppat and goalpat are terms that are matched against the goal. The instantiation is obviously kept from one match to the next. If a goal matches the provided function is called, and passed the instantiations for the matches (in the order they appear) as well as theorems corresponding to the matched hypotheses. (Should the matched hypotheses be removed from the hypotheses? Maybe; the user can always put them back.)

E.g.,

([`P ==> Q`, `P`], `goal`, (fn (_, [imp, a], _) => ASSUME_TAC (MP imp a)))

would be a bit like a RES_TAC, but which only eliminated one literal pair.

WIth a bit of care over the matching, a matching version would also work:

([`!x. P x ==> Q x`, `P v`], `goal`, (fn (_, [imp, a], _) => ASSUME_TAC (MATCH_MP imp a)))

(The code would have to instantiate subsequent patterns and β-reduce them.)

There are clearly all sorts of usability tweaks that might be added to this.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[xrchz]

I hope this might among other things lead to implementing some Chlipala-style seriously powerful automation tactics.

[xrchz]

Started in 3d4f44c9c46ed67a003c69a7957bf570b24d3a07

[xrchz]

@GallagherCommaJack was instrumental in making progress on this. (Noting this to connect to his GitHub profile.)

I also want to record some possible known issues with the current implementation:

• there's no higher-order matching
• matched hypotheses are kept; they can be deleted easily by the tactic but maybe that's cumbersome?
• type variables are (deliberately) always wildcards - not an issue, just a note
• there should be more shorthands/syntax for common patterns of usage
• there's no further matching in previously matched subterms or hypotheses (and no "as"-patterns either, which would be a special case)
• Jack and I thought there was also a problem with underscores not being treated as wildcards correctly (in particular when attempting to match terms containing bound variables) but I now think the current implementation is correct about that.

[xrchz]

A couple more suggestions after talking with @matichuk:

• assumptions could be stored in a term net to facilitate faster finding/matching
• matching could be done on arbitrary terms or theorems, rather than just (sub)terms/assumptions of the goal. This facilitates a certain kind of nested matching and match inversion (something closer to unification).