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

Question

我一直在研究 Coq ( repository here ) 中的过程演算的形式化，并不断发现自己试图应用一个由于等效但语法不同的子项而失败的函数。这通常是由于操纵 de Bruijn variables 而发生的。 .由于统一失败，我通常会事先明确替换行为不端的子项，然后应用我需要的功能。一个简单的代码作为我的意思的例子:

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 helps proving a goal of the form P x1 .. xN from an [sic] hypothesis H that concludes P y1 .. yN, where the arguments xi and yi may or may not be convertible. Equalities are produced for all arguments that don't unify.

The tactic invokes equates on all arguments, then calls applys K, and attempts reflexivity on the side equalities.