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) 

它看起來像勒柯克的存在量詞轉換成通用的一個。我知道（FORALL一，P一 - > Q上） - >（（存在，P A） - > Q上）出我的一階邏輯知識有限。但是反向命題似乎不正確。如果'全部'和'存在'一個不等價，爲什麼Coq會做這樣的轉換？

確實在勒柯克「琳」與較硬的替代目標來證明呢？或者任何人都可以請說明爲什麼保持在一階邏輯中？（存在a，P a）→Q a）→a

Answer 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，這確實比您擁有的語句強。