Coq: eliminating `forall`?

2
votes

I am struggling to prove the following theorem (non-empty domain is assumed):

Theorem t (A: Set) (P: A -> Prop): (forall a: A, P a) -> (exists a: A, P a).
Proof.
  intros H.

Noramlly, having forall a: A, P a I would deduce P c, where c is a constant. I.e. forall quantifier would be eliminated. Once that done I would again deduce exists a and my simple proof will be Qeded.

However, I can't find right way to eliminate on forall in Coq.

I am new to it and I'd like to know how to eliminate forall in Coq or what's the better way to prove the above-mentioned theorem?

P.S. I have seen this answer but it seems to be unrelated to my question.

1
coqcoq-tactic

1 Answers

4
votes

Unlike other logical formalisms (e.g. Isabelle/HOL), in Coq it is perfectly possible to have an empty domain. If you want to prove your statement, you have to assume explicitly that A is not empty. Here is one possibility.

Definition non_empty (A : Type) : Prop :=
  exists x : A, True.

Theorem t (A : Set) (P : A -> Prop) :
  non_empty A ->
  (forall a : A, P a) ->
  (exists a : A, P a).
Proof.
intros [c _] H. exists c. apply H.
Qed.