The Coq mailing list

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

Thanks for the tip about firstorder, but it is not what I am curious about here.
To be a little more precise, in the following situation:

1 subgoals
A : Type
P : A -> Prop
H : ~ (exists x y z : A, P x /\ P y /\ P z)
______________________________________(1/1)
forall x y z : A, ~ (P x /\ P y /\ P z)

with does "set (H1 := not_ex_all_not _ _ H)." works fine but "apply not_ex_all_not in H" complains about the missing x ?

Best, 
V.

2012/10/14 Adam Chlipala <adamc AT csail.mit.edu>

On 10/14/2012 11:51 AM, Vincent Siles wrote:

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).

Perhaps your question is more about specific low-level tactics than about the best way to prove your examples, but I'll just point out that the built-in [firstorder] tactic proves either of these facts automatically, without appealing to axioms.