[Coq-Club] Doing something n times with backgtracking

[Joey Eremondi]

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

[Maximilian Wuttke]

This post might be inappropriate. Click to display it.

[Jason -Zhong Sheng- Hu]

This post might be inappropriate. Click to display it.

[Joey Eremondi]

Yeah, it's looking like the problem I was facing were from bugs in other
tactics I'd written, both solutions work great otherwise. Thanks for the
help!

Post by Maximilian Wuttke
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*
------------------------------
*Sent:* August 18, 2018 7:05:22 PM
*Subject:* Re: [Coq-Club] Doing something n times with backgtracking
Hi Joey,
~~~~
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 <
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
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
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.