The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Joey,

I believe the original one with multimatch has done what you want. Just `do 2 find_specialize_in H` should suffice. That's because the backtracking point from multimatch is far reaching. However, multimatch tends to backtrack too much and gives performance impact. Maximilian's solution is better from this perspective.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
Sent: August 18, 2018 7:05:22 PM
To: coq-club AT inria.fr; Joey Eremondi
Subject: Re: [Coq-Club] Doing something n times with backgtracking

 

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.