Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Feb 24, 2016 at 02:43:28PM +0100, Ralf Jung wrote:
> Hi Enrico,
> 
> > 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.
> 
> That would indeed be (have been?) awesome.
> 
> > 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).
> 
> Thanks for the pointer!
> 
> I tried to write find_pat or even directly our cancel tactic on top of
> this, but was unable to extract the matched term:
> 
> ssrpattern [... some pattern ...].
> match goal with | |- let _ := ?x in _ => real_cancel(x) end.

Again, I did not play much with it, but I'd do a

  ssrpattern [pat]; intro selected; foo_tac selected; unfold selected; clear 
selected

> Furthermore, I was unable to even write a tactic that "forwards" a
> pattern into ssrpattern (like find_pat or cancel would have to):

I see what you mean, but I discovered "tactic notations" way after this
API was designed.  I hope it is possible to register custom tactic
arguments, but I don't know how to do it. Help is welcome.

>   Tactic Notation "mypat" open_constr(arg) := ssrpattern [arg].
>   mypat (f _)%I.
> 
> but then "mypat" cannot be used with contextual patterns.

Internally patterns are represented as terms, but I'd try to avoid
exploiting this fact ;-).  Better fix the previous problem.  Adding PMP
in CC since he is likely to know how tactic notations do work.

Best,
-- 
Enrico Tassi