具有存在目标的普遍假设中的 Coq 箭头类型

Posted

技术标签:

【中文标题】具有存在目标的普遍假设中的 Coq 箭头类型【英文标题】:Coq arrow type in universal hypotesis with existential goal 【发布时间】:2013-09-26 16:50:49 【问题描述】:

我有以下定理要证明:

Goal (exists x, ~P x) <-> ~(forall x, P x).

分手后

unfold not. split.

第一个含义很简单,基本上我们必须使用存在量词中的forall引入的x

intros. destruct H. apply H. apply (H0 x).

但是另一方面我不能这样继续下去,我认为应该有一个我找不到的想法。有什么建议吗?

【问题讨论】:

【参考方案1】:

好吧,这个问题确实被卡住了:我相信它在直觉逻辑中是无法证明的。

问题在于,如您所见,要通过反向推理取得进展,您需要立即提供见证,而要通过前向推理取得进展,您需要掌握一个荒谬的假设。所以这个目标卡住了。

问题是全称量词的否定并没有给你否定属性的存在见证。

一旦你引入了经典公理,就有很多方法可以证明它。这是一个带有排中律的笨拙的例子:

Parameter T : Type.
Parameter P : T -> Prop.

Axiom EM : forall (A : Prop), A \/ ~ A.

Goal (exists x, ~P x) <-> ~(forall x, P x).
Proof.
  split; intro H.
  destruct H as [x H]. intro A. apply H. easy.
  destruct (EM (exists x, ~ P x)) as [?|NE].
  easy.
  elim H. intro x. destruct (EM (P x)) as [Px|NPx].
  easy.
  elim NE. exists x. easy.
Qed.

【讨论】:

以上是关于具有存在目标的普遍假设中的 Coq 箭头类型的主要内容,如果未能解决你的问题,请参考以下文章

反转在 Coq 中产生意外的存在

在 Coq 假设中拆分析取 (\/)

在 Coq 证明语言中,“没有更多的子目标,但存在未实例化的存在变量”?

使用 Coq 证明存在量词

coq 中的存在实例化和泛化

如何在 Coq 中使用归纳类型处理案例