我对 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, Pa -> Q a)在一阶逻辑中成立？
也许缺少的关键是目标：
forall n, P n -> (Some goal)
应读作：
forall n, (P n -> (某个目标))
而不是：
(forall n, P n) -> (Some goal)
也就是说，给你的目标只是给你一个任意n和一个证明P n，这确实是消除存在的正确方法（你不知道见证的价值，因为它可能是任何使P真实的价值，你只是知道有一个n并且P n成立）。
相反，后者将为您提供一个可以为您传递P n的任何人构建的功能n，这确实是一个比您拥有的更强大的陈述。
我意识到这个问题很老，但我想添加以下重要说明：
在 Coq 中（更一般地说，在直觉逻辑中）存在量词定义如下（参见此处）
(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), thenG都被证明项精确地证明了
(ex_ind A P G h w) : G
任何时候都有效G : Prop。
注意：上面的排除规则只在任何时候有效A : Prop，不能在任何时候证明A : Type。在 Coq 中，这意味着我们没有ex_rect消除器。
据我了解（有关更多详细信息，请参见此处），这是保留良好程序提取属性的设计选择。