coq - 在策略中添加“in”部分以指定应用它的位置

Question

我是 Coq 和编写策略的新手，我一直无法弄清楚你是否可以定义更复杂的策略，比如内置策略。例如，假设我有一个tac1采用两个参数的策略，我定义tac2为

Ltac tac2 arg := tac1 arg _.

然后这就像我所期望的那样工作，但我真的很想能够tac2提出一个假设，比如tac2 arg in H. 我可以看到我可以将假设作为额外的参数给出，但是我不能在目标中使用它，我也希望能够像tac2 arg in *.

这样的事情是否可能，如何实现？

我找到了这个关于如何将介绍模式添加到你定义的策略的答案，它引导我到这个页面，Tactic Notation但我无法从中弄清楚我想要的是否可能。

Answer 1

按照这个答案，您可以像这样定义 tac2 的符号：

Tactic Notation "tac2" constr(arg) :=
  tac1 arg _.

Tactic Notation "tac2" constr(arg) "in" hyp(H) :=
  tac1 arg _ in H.

Tactic Notation "tac2" constr(arg) "in" "*" :=
  repeat match goal with
         | H:_ |- _ => tac2 arg in H
         | |- _ => tac2 arg
         end.

当然，tac1需要使用in修饰符，并且您应该小心终止repeat（参见此处）。