如何为Coq Ltac策略添加可选变量名功能？

嘿，我来帮你搞定这个需求！你想要让原来的save策略既能自动生成新鲜变量名，又支持用户传入自定义名字（比如save a），其实不用搞复杂的归纳类型，利用Coq Ltac的重载特性就能轻松实现，而且代码更简洁直观。

最终解决方案 #

直接定义两个同名的save策略，分别处理无参数和带参数的情况：

Require Import Classical.

(* 无参数版本：自动生成新鲜变量名 *)
Ltac save :=
  let H := fresh in apply NNPP; intro H; apply H.

(* 带参数版本：使用用户指定的名字（自动保证新鲜，避免冲突） *)
Ltac save n :=
  let H := fresh n in apply NNPP; intro H; apply H.

用法说明 #

• 无参数调用：直接写save，策略会自动生成一个不与上下文冲突的新鲜变量（比如H、H0等）：

  Lemma auto_gen_example : ~~P -> P.
  Proof.
    save.  (* 等价于：let H := fresh in apply NNPP; intro H; apply H *)
  Qed.
  

• 自定义变量名调用：传入你想要的名字，比如save my_hyp，策略会生成以该名字为前缀的新鲜变量（如果上下文已有my_hyp，会自动变成my_hyp0）：

  Lemma custom_name_example : ~~Q -> Q.
  Proof.
    save my_hyp.  (* 等价于：let H := fresh my_hyp in apply NNPP; intro H; apply H *)
  Qed.
  

为什么不用你原来的归纳类型方案？ #

你尝试定义ltac_No_arg来处理无参数的情况，其实有点绕了。Coq的Ltac天然支持同名策略重载——只要参数个数或类型不同，就可以定义多个同名策略，Coq会根据调用时的参数自动匹配对应的实现，这样代码更简洁，也符合Coq用户的常规使用习惯。

额外优化：强制使用用户指定的名字（不自动新鲜化） #

如果你确实想要完全使用用户传入的名字（即使上下文已有同名变量，愿意承担冲突风险），可以把带参数版本改成这样：

Ltac save n :=
  apply NNPP; intro n; apply n.

但这种方式如果上下文已有同名变量，intro n会报错，所以更推荐前面带fresh的版本，更健壮。

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