将 "in" 部分添加到策略以指定应用它的位置

Question

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

Ltac tac2 arg := tac1 arg _.

然后这按我预期的那样工作，但我真的希望能够根据假设调用 tac2，例如 tac2 arg in H。我可以看到我可以将假设作为一个额外的参数给出，但是我不能在目标中使用它，我也希望能够像 tac2 arg in *.

那样使用它

这样的事情可能吗？如何实现？

我找到了 about how you add intro patterns to tactics you define, and it lead me to this page 关于 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 的终止（参见）。

将 "in" 部分添加到策略以指定应用它的位置

Adding "in" part to tactic to specify where to apply it

coq

ltac