How to use de-morgan law in Coq to replace "not forall" by "exists"?

1
votes

I am learning the Coq language and trying to prove the following statement:

Lemma ex4: forall (X : Set) (P : X -> Prop), ~(forall x, ~ (P x)) -> (exists x, (P x)).

In the beginning of my proof:

Proof.
  intros X P A.

I arrive at the point where I have the assumptions

X : Set
P : X -> Prop
A : ~ (forall x : X, ~ P x)

I now want to apply de morgan law on A to get an assumption

B : exists x : X, ~ (~ P x) (*** Or something similar ***)

but I can't find a way to correctly use the library function. The following line

apply (not_all_ex_not P).

throws an error:

In environment
X : Set
P : X -> Prop
A : ~ (forall x : X, ~ P x)
The term "P" has type "X -> Prop" while it is expected to have type "Type".

I import the not_all_ex_not from using the command Require Import Coq.Logic.Classical.

What am I doing wrong?

1
coq

1 Answers

1
votes

Use apply not_all_ex_not in A instead (or apply (not_all_ex_not X (fun x => ~ P x)) in A).

Explanation In Coq, you need to explicitly apply type arguments to polymorphic functions and lemmas, unless they are marked as implicit. The not_all_x_not lemma has only explicit arguments, and the first argument is the argument type of the predicate, which is why your attempt did not work. The in A is needed because your goal does not syntactically match the conclusion of not_all_ex_not.