Coq 中是否有可能将统一错误转化为目标？

Question

我一直致力于 Coq 中流程演算的形式化（此处为存储库），并且不断发现自己尝试应用一个因等效但语法不同的子术语而失败的函数。这种情况经常是由于de Bruijn 变量的操纵而发生的。当统一失败时，我通常会事先明确替换行为不当的子项，然后应用我需要的函数。一个简单的代码作为我的意思的例子：

Require Import Lia.

Goal
  forall P: nat -> Prop,
  (forall a b c, P (a + (b + c))) ->
  forall a b c, P (b + c + a).
Proof.
  intros.
  (* Unification fails here. *)
  Fail apply H.
  (* Replace misbehaving subterms explictly. *)
  replace (b + c + a) with (a + (b + c)).
  - (* Now application succeeds. *)
    apply H.
  - (* Show now they were the same thing. *)
    lia.
Qed.

所以，我的问题是：是否有一种策略，或者是否可以用 ltac 编写一个策略，它类似于 apply，但将统一错误转化为额外的平等目标而不是失败？

Answer 1

applys_eq编程语言基金会的LibTactics将实现这一目标。从文档（截至本书版本 6.1）：

applys_eq H有助于从得出结论 的P x1 .. xN[原文如此] 假设中证明形式的目标，其中参数和可能可转换，也可能不可转换。所有不统一的论证都会产生等式。HP y1 .. yNxiyi

该策略调用equates所有参数，然后调用applys K，并尝试对等式进行自反性。