在Coq中能否将合一失败错误转化为额外的证明目标？

可用方案 #

1. 现有生态内置战术 #

Coq 标准库的setoid_apply战术可以直接满足需求：它支持在应用引理时自动引入所需的等价性证明作为子目标，无需手动做替换操作。如果你项目中导入了SSReflect扩展，直接使用apply:战术也能实现相同效果，遇到语法不匹配但语义等价的情况会自动生成相等证明目标。

如果涉及de Bruijn索引操作中常用的自定义等价关系（如上下文等价、α等价等），只需要将对应等价关系注册为Setoid，上述战术就能自动适配，不需要额外修改。

2. 自定义轻量Ltac实现 #

如果你不想引入额外依赖，可以自己实现一个极简的战术，核心逻辑如下：

Ltac apply_eq H :=
  match goal with
  | |- ?G =>
    let ty_H := type of H in
    match ty_H with
    | forall args, ?P =>
      (* 生成引理的实例化通配项 *)
      evar (inst : ty_H);
      let eq_goal := fresh "eq_goal" in
      assert (eq_goal : G = P) as []; [ | apply H ]
    end
  end.

使用时直接替换原来的apply H为apply_eq H即可：当合一失败时，会自动生成G = P的相等子目标，你只需要证明该等式即可，完全复现你原来手动replace的流程。

针对你给出的示例代码，使用该战术的证明可以简化为：

Proof.
  intros.
  apply_eq H.
  lia.
Qed.

效率优化技巧 #

针对你开发进程演算、频繁操作de Bruijn索引的场景，可以把移位、替换相关的等价引理加入autorewrite自定义数据库，调用apply_eq后直接用autorewrite with my_db就能自动证明绝大多数相等子目标，不需要手动交互。

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