Coq合一顺序控制：解决依赖参数场景下的合一失败问题

问题核心：Coq默认采用从左到右的合一顺序，对于参数存在依赖的函数，若左侧参数的合一约束包含未求值符号（如示例中的?n1 + 0）会直接失败，但右侧的依赖参数实际已经包含了元变量的完整求解信息。

可行方案 #

方案1：调整参数顺序（无额外依赖，改造成本最低） #

参数依赖不需要打破，只需将依赖参数（证明项）前置，搭配隐式参数即可：

Definition is_nice {f : Formula} (pf : FProof f) : bool := true.

修改后你示例中的apply impl_5_is_nice'可直接执行，合一会优先处理证明项，从中提取元变量?n1的约束。如果约束包含算数类的简单化简需求，可以同时在脚本开头加Set Keyed Unification.，让合一自动应用n+0 = n这类基础恒等式。

方案2：使用Canonical Structure重排合一逻辑（无需修改现有调用逻辑） #

按照你提到的Canonical Structure技巧，给公式和证明的配对定义结构，让Coq合一时自动优先从证明项推导信息：

Structure ProofWithContext := ProofWithContext {
  ctx_f : Formula;
  ctx_pf : FProof ctx_f
}.
Canonical Structure pf_in_ctx f (pf : FProof f) := ProofWithContext f pf.

Definition is_nice (c : ProofWithContext) : bool := true.

这个方案不需要改动你已经写好的所有impl_*_is_nice引理，也不需要修改调用语法，Coq会自动完成证明项到上下文结构的注入，优先求解证明项中的元变量。

方案3：用UniCoq/Keyed Unification直接解决（零代码修改） #

• 不想改任何定义的话，直接在脚本开头加Set Keyed Unification.即可，该选项会让Coq的合一算法优先匹配头符号，自动从依赖参数中提取元变量约束，不需要调整代码就能让你示例中的apply成功。
• 如果你已经安装了UniCoq，开启Set UniCoq.即可，它的合一算法原生支持依赖导向的求解顺序，天然支持这类场景。

方案4：通用tactic封装 #

如果以上方案都不适用，你不需要为每个引理单独写match goal逻辑，封装一个通用tactic即可覆盖所有同类引理：

Ltac apply_nice lem :=
  eapply lem;
  try match goal with
  | |- FProof _ => assumption
  | _ => reflexivity
  end.

所有同类引理都可以直接用apply_nice impl_5_is_nice'调用，自动处理合一顺序问题。

内容的提问来源于stack exchange，提问作者Jan Tušil