Coq 中的 'elim' 如何处理存在量词？

Question

我对 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, P a -> Q a) -> ((exists a, P a) -> Q a) 出于我对一阶逻辑的有限了解。但相反的命题似乎是不正确的。如果 'forall' 和 'exists' 不等价，为什么 Coq 会做这样的转换？

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

Answer 1

也许缺少的关键是目标：

forall n, P n -> (Some goal)

应读作：

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

而不是：

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

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

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

Answer 2

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

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

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

直观上可以理解为

(exists x, P x) is the smallest proposition which holds whenever P x0 holds for some 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），这是一种保留良好程序提取属性的设计选择。

Coq 中的 'elim' 如何处理存在量词？

How does 'elim' in Coq work on existential quantifier?

coq

first-order-logic