Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

> I am not sure to understand your question but you can always use
> rewriting to single out a subterm with a dummy identity.

We tried something like this. We even used "lock" to make stuff less
convertible. We still ended up with Coq diverging, in the next part of
the tactic, that has to do something like

match goal with
|- context[locked ?x] => unlock; real_cancel x || fail 2
end

What I want, speaking in code, is a tactic "find_pat" that I pass a
pattern (i.e., an open_constr), and a term of type "constr -> tactic".
find_pat should match the pattern with all subterms of the goal, and if
it finds a match, call the tactic with the matched subterm.
(As a bonus, it should support matching against any term, not just the
goal. And if we could control whether it only tries top-level matching,
or checks all subterms in all contexts, that may also be useful in some
cases.)

Right now, we have this:

Ltac find_pat pat tac :=
  match goal with |- context [?x] => unify pat x; tac x || fail 2
end.

but this diverges on patterns where, e.g., "rewrite [pat]lock" works fine.

Maybe adding a "marker" into the term with rewrite could be made to work
(it should not be lock, in order not to interfere with the user using
lock, and it should be all stripped out again before "tac" is called),
but that seems like a rather round-about way - and I don't think it can
work with matching against arbitrary terms, rather than matching against
the goal.
Somewhere in ssreflect, there has to be a primitive like find_pat that
is used by rewrite (or so I imagine), and it'd be great to have access
to that.

Kind regards,
Ralf