依赖类型和依赖值的相等性

Question

考虑依赖类型

Inductive dep (n: nat) :=
  mkDep : dep n.

现在，考虑一个我想证明的简单定理：

Theorem equalTypes (n n': nat): n = n' -> dep n = dep n'.
Proof.
  intros.
Abort.

如何证明两个依赖类型相等？什么是类型相等的概念？

更糟糕的是，考虑这个 "theorem"（无法编译）

Theorem equalInhabitants (n n' : nat): n = n' -> mkDep n = mkDep n'.
Abort.

这个语句是错误的，因为类型 mkDep n 和 mkDep n' 不匹配。但是，从某种意义上说，这个说法是真，因为在n = n'.

的假设下，它们是相同的值]

我希望了解如何形式化和证明有关依赖类型的陈述（特别是它们的相等性及其概念）

Answer 1

How do I show that two dependent types are equal?

在这种情况下，你可以用apply f_equal; assumption或subst; reflexivity（或destruct H; reflexivity或case H; reflexivity或induction H; reflexivity或exact (eq_rect n (fun n' => dep n = dep n') eq_refl n' H)来证明).

What is a notion of type equality?

与任何其他等式相同； Print eq. 给出：

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

这表示你必须构建相等性证明的唯一特殊事实是 x = x 对任何 x。使用等式证明 eq_rect 的方法是，如果您有 x = y，要证明 y 的属性 P，就足以证明 x 的 P。在这种情况下，由于我们有 n = n'，要证明 dep n = dep n'，只需证明 dep n = dep n（其中 P := fun n' => dep n = dep n'）。

可以从更深层次的意义上提出这个问题，因为事实证明 Coq 中的类型相等是约束不足的。鉴于

Inductive unit1 := tt1.
Inductive unit2 := tt2.

你无法证明unit1 = unit2，你也无法证明unit1 <> unit2。事实上，事实证明，唯一可以证明的类型不等式 T1 <> T2 是可以证明 T1 和 T2 不是同构的情况。 Univalence 公理是 "filling in the details" of type equality 的一种方式，表示任何同构类型都相等。不过，还有其他一致的解释（例如，我认为假设 A * B = C * D -> A = C /\ B = D 是一致的，尽管这与单价相矛盾）。

Worse, consider this "theorem" (which does not compile)
Theorem equalInhabitants (n n' : nat): n = n' -> mkDep n = mkDep n'.

没错。这是因为我们在 Coq 中没有等式反射规则，judgmental/definitional 等式与命题等式不同。说明这一点的方法是 "cast" 术语 mkDep n 跨越等式证明。

Import EqNotations.
Theorem equalInhabitants (n n' : nat): forall H : n = n', rew H in mkDep n = mkDep n'.
  intros.
  subst; reflexivity.
Qed.

请注意 rew 比 = 绑定得更紧密，并且是 eq_rect 的符号。这表示对于 n = n' 的任何证明 H，术语 mkDep n，当通过 H 传输成为类型 dep n' 的术语时，等于 mkDep n'。（还要注意，我们也可以使用 destruct H 或 induction H 或 case H（但不是 apply f_equal）来代替 subst。）

依赖类型和依赖值的相等性

Equality of dependent types and dependent values

equality

coq

dependent-type