The Coq mailing list

[Joey Eremondi <joey.eremondi AT gmail.com>]

Disclaimer: cross-posted on StackOverflow at https://stackoverflow.com/questions/51905979/ltac-repeating-a-tactic-n-times-with-backtracking

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?

Thanks,

Joey