Coq 无法区分依赖类型归纳命题的构造函数

Question

我创建了这个示例类型来演示我遇到的问题：

Inductive foo : nat -> Prop :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

现在很清楚foo_1 0 <> foo_2 0，但我无法证明这一点：

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H.

这将返回错误

不是可歧视的平等。

inversion H根本不会改变上下文。奇怪的是，如果我foo从Prop改为 ，Type那么证明会通过，但我不能在我的实际代码中这样做，因为它会导致其他地方出现问题。

我怎样才能得到这个证明？为什么这首先是有问题的？

Answer 1

Coq 背后的逻辑与“证明无关性”公理兼容，该公理指出给定的任何两个证明Prop都是相等的。因此，无法证明您制定的陈述。

如果您希望能够区分这两个构造函数，则需要foo使用 inductiveType而不是Prop. bar然后被接受为有效证明。

Inductive foo : nat -> Type :=
| foo_1 : forall n, foo n
| foo_2 : forall n, foo n.

Lemma bar : foo_1 0 <> foo_2 0.
Proof. unfold not. intros H. discriminate H. Qed.