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

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

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.

反演H根本不会改变背景.奇怪的是,如果我将foo从Prop更改为Type,那么证明就会通过,但我不能在我的实际代码中执行此操作,因为它会在其他地方引起问题.

我如何才能获得此证明？为什么这首先出现问题？

简短的回答：你做不到.

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

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

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

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

Error: Not a discriminable equality.

现在,让我们试着找出确切的歧视失败的地方.

首先,让我们绕道而行,并证明一个非常简单的陈述：

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.

以上是歧视策略构建的简化版本.

让我们用baz1,baz2,baz相应地替换false,true和bool作为证据,并看看会发生什么：

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 – >道具和什么是baz – >支柱的类型？

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

从命题证据到命题的映射都存在于Type中,而不是在Prop中！否则会导致宇宙不一致.

我们的结论是,没有办法证明不平等,因为没有办法突破Prop这样做 – 你不能只使用重写(baz1 = baz2)来建立一个虚假的证明.

另一个论点(我认为它已经被@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”一节.