Coq中如何避免在假设和目标中应用战术时的代码重复

方案1：单Ltac封装+约定目标标记 #

这是最贴近你设想的实现方案，仅需定义一个通用战术，就能模拟你想要的GOAL标记效果：

1. 首先定义目标的特殊标记，完全贴合你设想的GOAL语法：

(* 定义GOAL作为作用于目标的特殊标记，仅解析时生效不影响类型逻辑 *)
Notation GOAL := tt (only parsing).

2. 合并两个重复的战术为一个，通过参数判断作用位置：

Ltac my_tac loc :=
  lazymatch loc with
  (* 匹配到GOAL标记时作用于目标 *)
  | GOAL => simpl; rewrite X; other_tactic
  (* 其余情况视为假设名，作用于对应假设 *)
  | H => simpl in H; rewrite X in H; other_tactic in H
  end.

3. 使用方式：

• 作用于假设H：my_tac H
• 作用于目标：my_tac GOAL

后续修改战术逻辑时只需修改这一处定义，完全不会产生重复代码。

方案2：自动匹配目标/假设的模式 #

如果你需要匹配指定模式后自动执行逻辑，可以进一步封装模式匹配逻辑，完全消除重复的match分支：

Ltac my_tac_on_pattern pat :=
  match goal with
  | H : pat |- _ => my_tac H
  | |- pat => my_tac GOAL
  end.

使用时直接调用my_tac_on_pattern PATTERN即可，不需要手动编写两个匹配分支。

可选方案：使用SSReflect战术语言 #

如果你不排斥引入Mathematical Components生态，SSReflect的战术原生支持统一的位置修饰语法，大量减少这类重复代码，其内置的模式匹配也支持同时捕获假设和目标位置。

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