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.

这会返回错误

Not a discriminable equality.

inversion H根本不会改变上下文。奇怪的是，如果我改变 foo来自Prop至Type然后证明就通过了，但我不能在我的实际代码中这样做，因为它会在其他地方引起问题。

我怎样才能通过这个证明？为什么这首先会出现问题？

Answer 1

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

如果您希望能够区分两个构造函数，则需要将 foo 设为归纳型 Type 而不是 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.