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

Question

我一直在研究Coq中的过程演算的形式化(存储库在这里)，并不断发现自己试图应用一个函数，该函数由于等价但语法不同的子术语而失败。这种情况经常发生是因为对德布鲁因变量的操作。当统一失败时，我通常只是事先显式地替换行为不正常的子项，然后应用我需要的函数。一个简单的代码作为我的意思的例子:

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编写一种策略，这与应用类似，但将统一错误转化为额外的平等目标而不是失败?

Answer 1

applys_eqfromProgramming Language Foundations' LibTactics将完成这个任务。从文档(截至本书的6.1版):

applys_eq H有助于从得出P y1 .. yN的[sic]假设H证明P x1 .. xN形式的目标，其中参数xi和yi可能是可转换的，也可能不是可转换的。为所有不统一的参数生成等式。

该策略在所有参数上调用equates，然后调用applys K，并在两边相等上尝试自反性。