Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Feb 24, 2016 at 01:35:01PM +0100, Ralf Jung wrote:
> Is there a way to use the pattern matcher that is also used by
> ssreflect's rewrite, which seems to be "smarter" than [unify], in my own
> tactics?

The pattern matching machinery of Ssr is exported to ML with a
documented API:

  
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli

I did a long ago hoping it would be merged in Coq.

Given that I've very little experience with Ltac I did not advertise
that it is also somewhat exported to Ltac.
The ltac symbol is called "ssrpattern [pattern]"

  
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4#L1292

What it does is to turn your goal "G" intro "let selected_term := t in G'".
This API is clearly incomplete (wrt the ML one) that lets one call an
arbitrary continuation on the terms selected by the pattern in order to
produce G' (and is well tested, since Ssr's rewrite is based on it).

So I'm happy to receive feedback and suggestions, pull requests...

Best,
-- 
Enrico Tassi