The Coq mailing list

[Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>]

Hi Joey,


You can try to do recursion on a Coq number in Ltac:

~~~~
Ltac find_specialize_in H n :=
lazymatch n with
| 0 => idtac
| S ?n' =>
match goal with
| [ v : _ |- _ ] => specialize (H v); find_specialize_in H n'
end
end.

Goal forall (T:Type) (P: T -> Prop) (y:T) (H : forall (x:T), x=y -> P x) (x1 : T) (x2 : T) (Heq : x1 = y), P x1.
Proof.
intros. now find_specialize_in H 2.
Qed.
~~~~

This is equivalent to `find_specialize_in H; find_specialize_in H` (with your version using multimatch).
Note that I replaced the multimatch with match.
This works, because when the recursive tactical call fails, the match backtracks (i.e. chooses another `v`).
If you want something like `find_specialize_in H 1; find_specialize_in H 1` to work, you can again replace the `match` with `multimatch`.

Note that the second argument of the tactic (i.e. the number of repeats), is an actual Coq term.
For example, the `lazymatch` fails if you call `find_specialize_in H true`.


Sincerely
Maximilian

On August 19, 2018 12:34:05 AM GMT+02:00, Joey Eremondi <joey.eremondi AT gmail.com> wrote:

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

-- 
Sent from my Android device with K-9 Mail.