Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

For our current Coq project, we'd like some of our tactics to support
patterns. So, for example,

  cancel (_ -* _)

should find a magic wand in the goal, and then perform canceling on that
hypothesis.

Robbert asked about how to do this a while ago [1], and we ended up with

  Tactic Notation "cancel" open_constr(z) :=
  match goal with
  | _ : context [?z'] |- _ => unify z z'; real_cancel (z) || fail 2
  end.

where real_cancel takes a closed term.
However, we do have some subterms in our goals where the unifier pretty
much diverges when matching against certain patterns. But even with
those patterns and subterms, ssreflect's rewrite works fine.

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?
If this means custom tactics support ssreflect's contextual patterns and
what not, that would be welcome :)

For now, we ended up sealing our definitions with modules to help the
unifier. But is still rather frustrating to know that there is this
great pattern-matching engine that we use all the time for rewriting,
and that we cannot use for our own tactics.

[1] <https://sympa.inria.fr/sympa/arc/coq-club/2014-11/msg00023.html>

Kind regards,
Ralf