Ssreflect Users Discussion List

[Ralf Jung <>]

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.

This results in "No matching clauses for match.".
So, not being exactly an Ltac export either, I don't know how to use
ssrpattern to make other tactics "pattern-aware".

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

  Tactic Notation "mypat" ssrpatternarg(arg) := ssrpattern [arg].
  Tactic Notation "mypat" ssrpatternarg(arg) := ssrpattern [ltac:(arg)].

Both of these cannot be called with actual patterns, Coq complains about
arg being neither a term nor a tactic. This works:

  Tactic Notation "mypat" open_constr(arg) := ssrpattern [arg].
  mypat (f _)%I.

but then "mypat" cannot be used with contextual patterns.

Kind regards,
Ralf