Coq 中的“elim”如何作用于存在量词？答案

【问题标题】：How does 'elim' in Coq work on existential quantifier?Coq 中的“elim”如何作用于存在量词？
【发布时间】：2015-06-03 02:10:06
【问题描述】：

我对 Coq 处理存在量化的方式感到困惑。

我有一个谓词 P 和一个假设 H

P : nat -> Prop
H : exists n, P n

而当前的目标是（随便）

(Some goal)

如果我想在 H 中实例化 n，我会这样做

elim H.

不过淘汰后，现在的目标就变成了

forall n, P n -> (Some goal)

看起来 Coq 将存在量词转换为全称量词。我知道 (forall a, Pa -> Q a) -> ((exists a, Pa) -> Q a) 出于我对一阶逻辑的有限了解。但相反的命题似乎是不正确的。如果 'forall' 和 'exists' 不等价，为什么 Coq 会做这样的转换？

Coq 中的“elim”是否用更难证明的目标代替了目标？或者谁能说明为什么 ((exists a, P a) -> Q a) -> (forall a, P a -> Q a) 在一阶逻辑中成立？

【问题讨论】：

【解决方案1】：

也许缺少的关键是目标：

forall n, P n -> (Some goal)

读作：

forall n, (P n -> (某个目标))

而不是：

(forall n, P n) -> (Some goal)

也就是说，给你的目标只是给你一个任意的n 和一个证明P n，这确实是消除存在的正确方法（你不知道见证的价值，因为它可以是使P 为真的任何值，您只需知道存在n 并且P n 成立。

相反，后者将为您提供一个函数，该函数可以为您传递的任何n 构建P n，这确实是一个比您拥有的更强大的声明。

【讨论】：

如果 P 只适用于两个 nat 值但只有一个可以推断（某个目标）怎么办？如果将目标转换为“forall”风格，我必须证明这两种情况都是正确的。那么 Coq 是否进行了积极的转换？
@xywang 不。当你消除存在量词时，你会得到一个抽象的、任意的nat。你对它是哪一个一无所知，只是P 持有它。所以你只需要知道there exists a nat on which P holds 来证明Some goal。如果您需要知道是哪个nat 来证明Some goal，那么您的定理陈述过于笼统，您需要比存在假设提供的更多信息。

【解决方案2】：

我知道这个问题很老，但我想补充以下重要说明：

在 Coq 中（更一般地，在直觉逻辑中）存在量词被定义（参见 here）如下

(exists x, (P x)) := forall (P0 : Prop), ((forall x, (P x -> P0)) -> P0)

直观上可以理解为

(exists x, P x) 是当P x0 对某些x0 成立时成立的最小命题

事实上，在 Coq 中可以很容易地证明以下两个定理：

forall x0, (P x0 -> (exists x, P x))    (* the introduction rule -- proved from ex_intro *)

和（提供A : Prop）

(exists x : A, P x) -> {x : A | P x}    (* the elimination rule -- proved from ex_ind *)

所以表单的 Coq 目标

H1...Hn, w : (exists x, P x) |- G

被转换（使用 elim）到形式的 Coq 目标

H1...Hn, w : (exists x, P x) |- forall x0, (P x0 -> G)

因为只要h : forall x0, (P x0 -> G)，那么G 就被证明项精确地证明了

(ex_ind A P G h w) : G

只要G : Prop 有效。

注意：上面的排除规则只在A : Prop时有效，在A : Type时不能证明。在 Coq 中，这意味着我们没有 ex_rect 消除器。

据我了解（有关更多详细信息，请参阅here），这是一种保留良好程序提取属性的设计选择。

【讨论】：