Suppose I have a tactic like this (taken from HaysTac), that searches for an argument to specialize a particular hypothesis with:
Ltac find_specialize_in H :=
multimatch goal with
| [ v : _ |- _ ] => specialize (H v)
end.
However, I'd like to write a tactic that searches for n arguments to specialize a tactic with. The key is that it needs to backtrack. For example, if I have the following hypotheses:
y : T
H : forall (x : T), x = y -> P x
x1 : T
x2 : T
Heq : x1 = y
If I write do 2 (find_specialize_in H), it might choose x2 to instantiate it, then fail trying to find a second argument. So I need my repeat loop to be able to backtrack with which arguments it chooses to specialize earlier arguments.
Is it possible to do this? How can I make a tactic loop that backtracks with its choices of previous iterations?
