4

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

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那么证明就会通过，但我不能在我的实际代码中这样做，因为它会在其他地方引起问题。

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

4

2 回答 2

5

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.
于 2016-10-27T19:16:22.167 回答
4

简短的回答：你不能。

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

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

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

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

错误：不是可区分的平等。

现在，让我们尝试找出到底哪里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和,相应地替换为 , , 看看会发生什么：boolbaz1baz2baz

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.

以上失败并出现以下情况：

该命令确实失败，并显示消息：归纳类型中的
不正确消除： 返回类型有排序而应该排序。 不允许在 sort 谓词上消除 排序的归纳对象， 因为只有在构建证明时才能消除证明。ebaz
TypeProp
Prop
Type

错误的原因是这个抽象：

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，那么证明无关公理将与 Coq 的逻辑不一致：

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

但是，众所周知，它是一致的，请参阅Coq 的常见问题解答。

您可能想查看CPDT的Universes 章节，特别是“Prop Universe”部分。

于 2016-10-27T20:34:48.380 回答