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.

这个returns错误

Not a discriminable equality.

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

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

Answer 1

Coq 的底层逻辑与 "proof irrelevance" 的公理兼容，该公理指出给定 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.

Answer 2

简答：你不能。

让我们举一个更简单的例子，我们也未能证明类似的事情：

Inductive baz : Prop :=
| baz1 : baz
| baz2 : baz.

Goal baz1 <> baz2.
  intro H.
  Fail discriminate H.
Abort.

以上操作失败并显示以下错误消息：

Error: Not a discriminable equality.

现在，让我们尝试找出 discriminate 的确切位置。

首先，我们绕个弯，证明一个很简单的命题：

Goal false <> true.
  intro prf; discriminate.
Qed.

我们也可以通过直接提供其证明项来证明上述目标，而不是使用策略来构建它：

Goal false <> true.
  exact (fun prf : false = true =>
    eq_ind false (fun e : bool => if e then False else True) I true prf).
Qed.

以上是 discriminate 策略构建的简化版本。

我们把证明项中的false、true、bool分别替换为baz1、baz2、baz，看看发生了什么：

Goal baz1 <> baz2.
  Fail exact (fun prf : baz1 = baz2 =>
    eq_ind baz1 (fun e : baz => if e then False else True) I baz2 prf).
Abort.

以上失败并显示以下内容：

The command has indeed failed with message:
Incorrect elimination of e in the inductive type baz:
the return type has sort Type while it should be Prop.
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

错误的原因是这个抽象：

Fail Check (fun e : baz => if e then False else True).

以上产生了相同的错误信息。很容易看出原因。抽象的类型是 baz -> Prop，baz -> Prop 的类型是什么？

Check baz -> Prop.   (* baz -> Prop : Type *)

从命题证明到命题的映射存在于 Type 中， 而不是 中 Prop！否则会造成宇宙不一致。

我们的结论是没有办法证明不等式，因为没有办法突破 Prop 来做到这一点——你不能只使用重写 (baz1 = baz2 ) 构建 False.

的证明

另一个论点（我看到它已经由@gallais 提出）：如果可以使用一些巧妙的技巧并在 Prop 内进行证明，那么 proof irrelevance 公理将与 Coq 的逻辑不一致：

Variable contra : baz1 <> baz2.
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
Check contra (proof_irrelevance _ baz1 baz2).    (* False *)

但是，众所周知，它是一致的，请参阅 Coq's FAQ。

您可能想看看 Universes CPDT 章节，具体 "The Prop Universe" 节。

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

Coq can't discriminate between constructors for dependently typed inductive proposition

coq

coq-tactic