Implement Coq-style goal-matching tactic

[hol-theorem-prover]

Implement Coq-style goal-matching tactic

[xrchz]

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

[xrchz]

Started in 3d4f44c

[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).