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

Question

I'm confused by Coq on its way dealing with existential quantification.

I have a predicate P and an assumption H

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

while the current goal is (whatever)

(Some goal)

If I want to instantiate n in H, I will do

elim H.

However after the elimination, the current goal becomes

forall n, P n -> (Some goal)

It looks like Coq converts an existential quantifier into a universal one. I know that (forall a, P a -> Q a) -> ((exists a, P a) -> Q a) out of my limited knowledge on first-order logic. But the reverse proposition seems to be incorrect. If the 'forall' one and 'exists' one are not equivalent, why Coq would do such conversion?

Does 'elim' in Coq replace the goal with a harder to prove one? Or could anyone please show why ((exists a, P a) -> Q a) -> (forall a, P a -> Q a) holds in first-order logic?

Answer 1

Maybe the missing key is that the goal:

forall n, P n -> (Some goal)

is to be read as:

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

and not as:

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

That is, the goal you are given just gives you an arbitrary n and a proof P n, which is indeed the proper way to eliminate an existential (you don't get to know the value of the witness since it could be any value that makes P true, you just get to know that there is a n and that P n holds).

On the contrary, the latter would provide you with a function that can build P n for any n you pass it, which is indeed a stronger statement than the one you have.

Answer 2

I realize this question is old but I would like to add the following important clarification:

In Coq, (and more generally, in intuitionistic logic) the existential quantifier is defined (see here) as follows

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

Intuitively this can be read as

(exists x, P x) is the smallest proposition which holds whenever P x0 holds for some x0

In fact one can easily prove the following two theorems in Coq:

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

and (provided A : Prop)

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

So a Coq goal of the form

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

is transformed (using elim) to a Coq goal of the form

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

because whenever h : forall x0, (P x0 -> G), then G is precisely justified by the proof term

(ex_ind A P G h w) : G

which works whenever G : Prop.

Note: the elimination rule above is only valid whenever A : Prop, and cannot be proved whenever A : Type. In Coq, this mean that we do not have the ex_rect eliminator.

From my understanding (see here for more details), this is a design choice to preserve good program extraction properties.