什么时候归纳类型的构造函数是穷举的？

Question

对于像自然数nat这样的简单归纳类型，很容易证明两个构造函数（零和后继）给出所有可能的自然数，

Lemma nat_destruct (n : nat) : n = O \/ exists m : nat, n = S m.
Proof.
  destruct n. left. reflexivity. right. exists n. reflexivity.
Qed.

但是我听说相等性证明并不是那么简单。只有一个等式构造函数eq_refl，但 Coq 无法证明这一点

eq_destruct : forall (A : Type) (x : A) (prEq : x = x), prEq = eq_refl

究竟是什么阻碍了这个证明？可能第一个问题是相等不仅仅是一个类型，而是一个类型族eq : forall A : Type, A -> A -> Prop。是否有一个更简单的类型族，这样的证明是不可能的？可能有 1 个或 2 个参数而不是 3 个？

Answer 1

我在blog post 中写过这个问题。通常，当您在不具有可判定相等性的类型上定义类型族时，就会出现这种情况。例如，考虑以下类型：

Inductive foo : Type -> Type :=
| Foo : foo unit.

不可能证明（我很确定）foo unit 的每个居民都是Foo 的形式。

这种现象在证明条款的层面上更容易看到。当你破坏这样一个族的一个词时，你必须对这个族的索引进行泛化。如果类型具有可判定的相等性，则只能将此索引与已知形状相关联，例如 unit。