如何为Coq自定义tactic添加in参数以指定应用位置

这类需求完全可以实现，通过Tactic Notation定义不同调用语法的变体，配合Ltac的上下文匹配逻辑，即可实现和内置tactic完全一致的使用体验。

实现步骤 #

1. 核心思路 #

内置tactic的in H、in *语法本质是不同的语法入口，最终映射到不同的tactic执行逻辑。我们可以为同一种核心逻辑定义多个Tactic Notation入口，分别处理不同的调用形式。
对于只需要在目标上执行的原始tactic，要迁移到假设上执行，最简便的方式是将目标假设revert到目标结论中，执行原tactic后再重新引入假设，不需要修改原有的tac2核心逻辑。

2. 完整代码示例 #

首先将你原有tac2的核心逻辑重命名为非对外的底层实现，避免和语法层定义重名冲突：

(* 底层核心实现，不直接对外暴露 *)
Ltac tac2_core arg := tac1 arg _.

添加如下Tactic Notation定义即可扩展三种常用调用语法：

(* 原有直接调用语法：作用于目标结论 *)
Tactic Notation "tac2" constr(arg) :=
  tac2_core arg.

(* 新增指定假设调用语法：tac2 arg in H *)
Tactic Notation "tac2" constr(arg) "in" ident(H) :=
  revert H; tac2_core arg; intro H.

(* 新增全局作用语法：tac2 arg in * *)
Tactic Notation "tac2" constr(arg) "in" "*" :=
  (* 将所有假设临时合并到目标结论中统一处理 *)
  repeat match goal with [ H : _ |- _ ] => revert H end;
  tac2_core arg;
  (* 处理完成后重新恢复所有假设 *)
  intros.

3. 扩展说明 #

• 如果你的tac2逻辑不依赖当前上下文的假设结构，上述方案可以直接复用，不需要修改原有核心逻辑。
• 如果你的tac2有更复杂的逻辑，不能用revert+intro的方案，可以直接在Ltac中匹配目标上下文，对指定假设的类型做单独处理，例如：

  Tactic Notation "tac2" constr(arg) "in" ident(H) :=
    let ty := type of H in
    (* 自定义对ty的处理逻辑，完成后替换H的类型 *)
    let new_ty := ltac:(let t := (eval cbv in ty) in exact t) in
    replace ty with new_ty in H.
  

  这种方式可以实现任意复杂度的自定义逻辑，完全可以达到内置tactic的功能丰富度。

内容的提问来源于stack exchange，提问作者Kristian