coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent Siles <vincent.siles AT ens-lyon.org>
- To: Adam Chlipala <adamc AT csail.mit.edu>
- Cc: Coq Club <coq-club AT inria.fr>, j.alglave AT ucl.ac.uk
- Subject: Re: [Coq-Club] not_ex_all_not seems to have trouble with multiple identifiers
- Date: Mon, 15 Oct 2012 16:54:16 +0200
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: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.
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).
- [Coq-Club] not_ex_all_not seems to have trouble with multiple identifiers, Vincent Siles, 10/14/2012
- Re: [Coq-Club] not_ex_all_not seems to have trouble with multiple identifiers, Adam Chlipala, 10/14/2012
- Re: [Coq-Club] not_ex_all_not seems to have trouble with multiple identifiers, Vincent Siles, 10/15/2012
- Re: [Coq-Club] not_ex_all_not seems to have trouble with multiple identifiers, Adam Chlipala, 10/14/2012
Archive powered by MHonArc 2.6.18.