coq problems

peirce_implies_lem.v

(*

https://www.youtube.com/watch?v=7sk8hPWAMSw
http://en.wikipedia.org/wiki/Law_of_excluded_middle
http://en.wikipedia.org/wiki/Peirce_law

*)

Definition peirce := forall (p q : Prop),
  ((p -> q) -> p) -> p.

Definition lem := forall p : Prop, 
  p\/ ~ p.

Theorem peirce_implies_lem: peirce -> lem.

Proof.
  unfold peirce, lem.
  intros.
  apply H with (q := ~ (p \/ ~ p)).
  firstorder.
Qed.


(* Not so fast please.
Can we break the last two steps down a bit? *)

Definition w0 := forall (p : Prop),
  ((p -> ~ (p \/ ~ p) ) -> p) -> p.

Definition w1 := forall (p : Prop),
  (p \/ ~ p -> ~ (p \/ ~ p)) -> p \/ ~ p.


Lemma w0_implies_w1: w0 -> w1.

Proof.
  unfold w0, w1.
  firstorder. 
Qed.

(* How to prove w0_implies_w1 without 'firstorder magic'? *)


Lemma w1_implies_lem: w1 -> lem.

Proof.
  unfold w1, lem.
  intro.
  intro. 

(* How to finish proof of w1_implies_lem? *)