依赖类型与依赖值的相等性：Coq中证明与形式化问询

让咱们一步步拆解你遇到的这几个关于Coq中依赖类型相等性的问题：

其实这个定理的证明非常直接——既然我们有n = n'的假设，只需要把其中一个参数替换成另一个，就能让两边的类型完全一致，再用reflexivity证明自反性就行。完整的证明代码如下：

Theorem equalTypes (n n': nat): n = n' -> dep n = dep n'.
Proof.
  intros H.
  rewrite H. (* 或者用`subst n'`直接替换变量，效果完全一样 *)
  reflexivity.
Qed.

这里的核心逻辑是：dep是一个带参数的归纳类型，当它的参数命题相等时，整个类型实例就天然是相等的——Coq的类型系统会认可这种参数传递带来的类型相等性。

在Coq里，类型本身也是一种项，它们属于Type（或者Set、Prop这些宇宙层级）。所以类型的相等就是我们平时用=表示的命题相等（propositional equality），和普通自然数、函数这些项的相等是同一个概念。

命题相等的底层是Leibniz相等的思想：两个对象相等，当且仅当所有能应用在其中一个对象上的性质，也能应用在另一个对象上，并且得到相同的结果。对于依赖类型来说，只要构造它们的参数命题相等，整个类型就满足命题相等——这是由归纳类型的构造规则保证的。

你说得没错，直接写mkDep n = mkDep n'会报错，因为Coq的同质相等（普通的=）要求两边的类型必须完全一致。要表达这种“参数相等时，依赖类型的居民本质相同”的命题，我们有几种常用的方法：

方法一：用类型转换把两边统一到同一类型 #

我们可以利用n = n'的假设，把其中一边的类型转换成和另一边一致。这里要用到Coq的相等归纳原理eq_rect，它可以帮我们把一个依赖类型的项，从参数为x'的类型转换到参数为x的类型（当x = x'时）。完整的定理写法和证明如下：

Theorem equalInhabitants (n n' : nat): n = n' -> @eq (dep n) (mkDep n) (eq_rect n' (fun x => dep x) (mkDep n') n H).
Proof.
  intros H.
  simpl. (* 简化eq_rect的展开结果 *)
  reflexivity.
Qed.

不过这种写法比较繁琐，日常使用中我们可以用rewrite H in *来自动调整目标和假设中的类型，让两边的类型统一后再证明。

方法二：使用异质相等JMeq #

Coq的标准库Program.Equality提供了JMeq（也叫依赖相等/异质相等），它专门用来断言不同类型的项在本质上是相等的。JMeq a b的意思是：存在某个类型T，使得a : T、b : T，并且a = b（在T的语境下）。用它来写你的定理就非常直观：

Require Import Program.Equality.

Theorem equalInhabitants (n n' : nat): n = n' -> JMeq (mkDep n) (mkDep n').
Proof.
  intros H.
  rewrite H. (* 把n'替换成n，此时mkDep n'的类型变成dep n，和左边一致 *)
  reflexivity.
Qed.

方法三：使用专门的依赖居民相等eq_dep #

还有一种更贴合场景的方式是用eq_dep，它直接描述了依赖类型居民的相等性，同时关联了参数的相等。eq_dep A P x a x' a'表示：x = x'，并且当把a的类型转换到P x'时，a和a'是相等的。用它来实现的话：

Theorem equalInhabitants' (n n' : nat): n = n' -> eq_dep nat dep n (mkDep n) n' (mkDep n').
Proof.
  intros H.
  subst n'. (* 直接替换n'为n，两边完全一致 *)
  reflexivity.
Qed.

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