The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi List, 

Using the lemma of Classical_Pred_Set.v,  Lemma not_ex_all_not : forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
I wanted to prove  (a more complicated lemma but it boils down to)

Lemma foo (A:Set) (P : A -> Prop) : ~(exists x, exists y, exists z, (P x /\ P y  /\ P z)) -> forall x y z, ~(P x /\ P y  /\ P z).

I was surprised that 
intros A P H.
apply not_ex_all_not in H.

didn't work, the error is "Error: Unable to find an instance for the variable n."

If I try with eapply, I get a new H of the shape  "~ (exists y, exists z, (P ?3498 /\ P y /\ P z))"  instead of a 
"forall x, ~ (exists y, exists z, (P x /\ P y /\ P z))"  as I expected.

I don't understand why Coq doesn't produce a forall and wants to instantiate 
it directly.

I managed to prove it by doing one "forall" at a time with the following script:

intros A P H x y.
apply not_ex_all_not.
revert y.
apply not_ex_all_not.
revert x.
apply not_ex_all_not.

Is this a bug or did I do something wrong ?

Best,
V (using Coq 8.3pl4 (June 2012))