在Coq中证明eqb_trans时apply eqb_true报错的原因及解决方法

我来帮你理清这里的问题所在，以及给出具体的解决步骤：

为什么apply eqb_true会报错？ #

首先看你用到的eqb_true定理：

Theorem eqb_true : forall n m, n =? m = true -> n = m.

这个定理的逻辑方向是从「布尔等式结果为true」推导出「自然数相等」，但你当前的目标是要证明(n =? p) = true——也就是要从「自然数相等」推导出「布尔等式结果为true」，这正好是eqb_true的逆方向！Coq无法把你的目标（布尔值的等式）和eqb_true的结论（自然数的等式）统一起来，所以才会抛出Unable to unify的错误。

正确的证明步骤 #

现在你已经通过apply eqb_true得到了H1 : n = m和H2 : m = p，接下来只需要利用自然数相等的传递性得到n = p，再证明相等的自然数的布尔等式结果一定为true即可。这里有三种直观的方法：

方法1：通过改写简化目标 #

这种方法不需要额外定理，直接利用改写和自反性：

intros n m p H1 H2.
apply eqb_true in H1.
apply eqb_true in H2.
(* 先推导n = p：利用H1和H2的传递性 *)
rewrite H1 in H2. (* 此时H2变为n = p *)
rewrite H2. (* 把目标中的n替换成p，目标变为p =? p = true *)
reflexivity. (* 任何自然数和自己的eqb结果都是true，直接得证 *)

方法2：先证明逆定理再使用 #

如果你希望用类似apply的方式完成证明，可以先手动证明eqb_true的逆定理：

(* 先证明逆定理：自然数相等则布尔等式为true *)
Theorem eq_eqb : forall n m, n = m -> n =? m = true.
Proof.
  intros n m H. rewrite H. reflexivity. Qed.

(* 然后完成eqb_trans的证明 *)
Theorem eqb_trans : forall n m p, n =? m = true -> m =? p = true -> n =? p = true.
Proof.
  intros n m p H1 H2.
  apply eqb_true in H1.
  apply eqb_true in H2.
  transitivity m; assumption. (* 得到n = p *)
  apply eq_eqb. assumption. (* 用逆定理完成目标证明 *)
Qed.

方法3：使用标准库的双向等价定理 #

Coq的标准库中已经提供了Nat.eqb_eq，它是一个双向的等价关系：forall n m, (n =? m) = true <-> n = m，用它可以简化整个证明流程：

Require Import Nat.

Theorem eqb_trans : forall n m p, n =? m = true -> m =? p = true -> n =? p = true.
Proof.
  intros n m p H1 H2.
  apply Nat.eqb_eq in H1. (* 把H1转成n = m *)
  apply Nat.eqb_eq in H2. (* 把H2转成m = p *)
  apply Nat.eqb_eq. (* 把目标转成n = p *)
  transitivity m; assumption. (* 证明n = p *)
Qed.

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