I recently needed to prove the following theorem in Coq:
Module ForallExists.
Theorem forall_exists : forall D, forall P : D -> Prop,
~ (forall x : D, P x) <-> (exists x : D, ~ P x).
That is, if a property does not hold for all of the elements, then there must be an element for which the property does not hold. I don't think this is provable in Coq without classical reasoning (if I'm wrong, please correct me).
So I added classical reasoning:
Require Import Classical.
and then I went on to construct its proof:
1 subgoal
============================
forall (D : Type) (P : D -> Prop),
~ (forall x : D, P x) <-> (exists x : D, ~ P x)
The first thing I did was to split the equivalence proof into proofs of the two implications:
split.
2 subgoals
D : Type
P : D -> Prop
============================
~ (forall x : D, P x) -> exists x : D, ~ P x
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
The first implication is the one which requires classical reasoning. After introducing the antecedent into the hypothesis:
intro.
2 subgoals
D : Type
P : D -> Prop
H : ~ (forall x : D, P x)
============================
exists x : D, ~ P x
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
we want to continue by contradiction on whether such an x really exists. This is called Peirce's law
Check Peirce.
Peirce
: forall P : Prop, ((P -> False) -> P) -> P
and it comes with the Classical module. That is, if we can prove that the negation ~P of P (~P is shorthand for P -> False) implies P, then we can deduce P.
apply Peirce.
intros.
2 subgoals
D : Type
P : D -> Prop
H : ~ (forall x : D, P x)
H0 : (exists x : D, ~ P x) -> False
============================
exists x : D, ~ P x
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
As H and H0 are contradictory, we will continue by proving False using H.
exfalso.
apply H.
intros.
2 subgoals
D : Type
P : D -> Prop
H : ~ (forall x : D, P x)
H0 : (exists x : D, ~ P x) -> False
x : D
============================
P x
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
That is, it remains to be shown that P x holds (for arbitrary x). Again we reason using Peirce's law.
apply Peirce.
intros.
2 subgoals
D : Type
P : D -> Prop
H : ~ (forall x : D, P x)
H0 : (exists x : D, ~ P x) -> False
x : D
H1 : P x -> False
============================
P x
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
As H0 and H1 are contradictory, we change the goal with False and prove the contradiction.
exfalso.
apply H0.
2 subgoals
D : Type
P : D -> Prop
H : ~ (forall x : D, P x)
H0 : (exists x : D, ~ P x) -> False
x : D
H1 : P x -> False
============================
exists x0 : D, ~ P x0
subgoal 2 is:
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
The required x0 is easy to produce (it is sufficient to use x).
exists x.
assumption.
1 subgoal
D : Type
P : D -> Prop
============================
(exists x : D, ~ P x) -> ~ (forall x : D, P x)
and we are left with the second implication. This one is easier and we do not need classical reasoning for it.
intros.
unfold not.
intros.
1 subgoal
D : Type
P : D -> Prop
H : exists x : D, ~ P x
H0 : forall x : D, P x
============================
False
We first introduce everything into the hypothesis and next we produce a witness for H:
elim H.
intros.
1 subgoal
D : Type
P : D -> Prop
H : exists x : D, ~ P x
H0 : forall x : D, P x
x : D
H1 : ~ P x
============================
False
The rest is routine, as it is easy to derive the contradiction.
assert (P x).
apply H0.
contradiction.
Proof completed.
Qed.
End ForallExists.
No comments:
Post a Comment