CODEWITHSUNDEEP
coqtheorem-proving
Nayr
Nayr

Reputation: 55

Lost on this exercise

I have to proof this:

Variable A : Set.
Variable P : A -> Prop.
Variables R : A -> A -> Prop.

Lemma pool : (forall x:A, ~P x) -> ~(exists x:A, ~ P x).

So far I've done:

intros.
unfold not.
intros.
elim H0.
destruct H0.
intros.
exact x0.

Then I have to proof False. I have no idea what to do. Is this non-provable? Can you put me in the right direction? Or am I missing something here?

EDIT: Ptival, you're a great help...I noticed a mistake on the question and when I tried to edit the question, I accidentally hit the delete button, panicked and hit backspace. :(

Upvotes: 1

Views: 115

Answers (1)

Ptival
Ptival

Reputation: 9437

(Oh well, answering again :P)

I believe your theorem is still flawed (unless A is an empty set...).

Did you mean:

Lemma pool : (forall x:A, ~P x) -> ~(exists x:A, P x).

In that case, it is doable, and here is how you could start:

Proof.
  intros A E.
  destruct E as [x P].

The rest is very easy and up to you to figure out if that is indeed the goal you wanted in the first place.

Upvotes: 1

Related Questions