[SOLVED] How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?

How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?

I am currently confused about how to prove the following theorem:

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).

I am stuck here:

Theorem excluded_middle2 : 
  (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).
Proof.
  intros.
  evar (Q : Prop).
  specialize H with (P : Prop) (Q : Prop).

I know that it's impossible to simply prove the law of excluded middle in coq, but I really want to know with this given theorem is it possible to prove the law of excluded middle?

Solution

Yes, you can. One way, using ssreflect, is as follows (there are probably shorter ways):

Lemma orC P Q : P \/ Q -> Q \/ P.
Proof. by case; [right | left]. Qed.

Theorem excluded_middle2 : 
 (forall P Q : Prop, (P -> Q) -> (~ P \/ Q)) -> (forall P, P \/ ~ P).
Proof.
move=> orasimply P.
have pp : P -> P by [].
move: (orasimply P P pp).
exact: orC.
Qed.