coq: elimination of forall quantifier

4
votes

I want to prove the following theorem:

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).

I already got the following piece of the proof:

Proof.
intro.
intro.
destruct H.
left.
assumption.

But now I am in a situation I don't know what to do. The following things are at my disposal:

A : Set
q : Prop
p : A -> Prop
H : forall x : A, p x
x : A

And I would like to prove the following subgoal:

q \/ p x

How can I eliminate the forall quantifier in the given premise

forall x : A, p x

that is: How can I plug in my concrete x : A so that I can deduce: p x ?

2
coqcoq-tactic

2 Answers

2
votes

You can instantiate the universally quantified x in H with specialize (specialize (H x)).

0
votes

Probably the simplest?

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).
intro H.

elim H.
intros Hl x.
left.
exact Hl.

intros Hr x.
right.
apply Hr.