不同类型函数的依赖等式证明问题及Coq中eq_rect使用建议

我正在处理一个包含两种不同索引方式的依赖类型问题，希望证明一种形式的proof irrelevance。具体来说，我尝试证明如下定理：

Theorem existT_eqrect_bool_irrel {A B} (P : A -> Type) p b (eq0 eq1 : b = true)
    (Q := fun (b : bool) => if b then P p else B) Qb :
    existT P p (eq_rect b Q Qb true eq0) =
    existT P p (eq_rect b Q Qb true eq1).
  destruct eq0.

(* Error 信息 *)
Error: Abstracting over the terms "b0" and "eq0" leads to a term
fun (b1 : bool) (eq2 : b = b1) =>
forall eq3 : b = b1,
existT P p (eq_rect b Q Qb b1 eq2) = existT P p (eq_rect b Q Qb b1 eq3)
which is ill-typed.
Reason is: Illegal application: 
The term "existT" of type
 "forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}"
cannot be applied to the terms
 "A" : "Type"
 "P" : "A -> Type"
 "p" : "A"
 "eq_rect b Q Qb b1 eq2" : "Q b1"
The 4th term has type "Q b1" which should be coercible to 
"P p".

修改时总会出现类型错误，因为泛化true后，Coq无法识别P p = Q true，而P p = Q b并不普遍成立。我测试了更小的案例，它可以直接证明：

Theorem existT_eqrect_irrel {A} (P : A -> Type) a b (eq0 eq1 : a = b) Pa :
    existT P b (eq_rect a P Pa b eq0) =
    existT P b (eq_rect a P Pa b eq1).
  destruct eq0, eq1; apply eq_refl.
Qed.

我有三个问题：

1. 能否不借助额外公理证明existT_eqrect_bool_irrel？
2. 是否存在可证明的类似形式？
3. 在Coq中通过eq_rect处理类型难度较大，有没有通用的优化建议？

问题解答 #

1. 能否不借助额外公理证明existT_eqrect_bool_irrel？ #

可以。核心是利用eq0和eq1都是b = true的证明这一前提，先通过destruct eq0将b归约为true，此时Q true会自动展开为P p，类型不匹配的问题就解决了。完整证明如下：

Theorem existT_eqrect_bool_irrel {A B} (P : A -> Type) p b (eq0 eq1 : b = true)
    (Q := fun (b : bool) => if b then P p else B) Qb :
    existT P p (eq_rect b Q Qb true eq0) =
    existT P p (eq_rect b Q Qb true eq1).
Proof.
  destruct eq0.
  (* 此时b被替换为true，Q true = P p，eq_rect的结果类型自动匹配P p *)
  rewrite (UIP_refl true eq1). (* 利用布尔类型的UIP（唯一性证明），eq1会被归约为eq_refl *)
  reflexivity.
Qed.

注：布尔类型的UIP不需要额外公理，因为bool是可判定的离散类型，Coq原生支持其证明唯一性。

2. 是否存在可证明的类似形式？ #

存在。只要满足以下条件，类似的命题都可以被证明：

• 等式右边的类型（如例子中的Q true）可以通过等式证明（如b = true）与目标类型（P p）统一；
• 等式的证明所在的类型是UIP成立的类型（如离散类型bool、nat，或所有可判定相等的类型）。

比如将bool替换为nat的类似命题：

Theorem existT_eqrect_nat_irrel {A B} (P : A -> Type) p n (eq0 eq1 : n = 0)
    (Q := fun (n : nat) => if n =? 0 then P p else B) Qn :
    existT P p (eq_rect n Q Qn 0 eq0) =
    existT P p (eq_rect n Q Qn 0 eq1).
Proof.
  destruct eq0; rewrite (UIP_refl 0 eq1); reflexivity.
Qed.

3. 处理eq_rect的通用优化建议 #

• 优先利用等式将类型归约统一：在遇到类型不匹配时，先通过destruct、rewrite或subst将等式两边的类型变量归约为相同值，让Coq自动处理类型转换；
• 善用UIP或证明唯一性：对于离散类型（如bool、nat），其等式证明是唯一的，可以直接用UIP_refl将任意等式证明转为eq_refl，简化目标；
• 避免过早泛化类型变量：不要在类型还未统一时就尝试抽象变量，先通过等式约束缩小类型范围；
• 使用rewrite代替直接destruct（按需）：如果不想直接破坏原变量，可以用rewrite eq0 in *将所有相关位置的b替换为true，再进行后续证明；
• 显式标注类型转换：如果Coq无法自动推导类型等价，可以手动用cast或eq_rect构造类型转换项，但尽量通过等式归约避免这种情况。

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