The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

Thanks Marko (and sorry Adam)!

I'd like to prove Peirce's Law a bit more explicitly than tauto, in fact I'd like to be as explicit in my hand proof just to learn the ins and outs of Coq.

The first step in the hand proof is rewriting H: (p -> q) -> p to H: ~(p -> q) \/ p using the alternate definition of implication.

$ coqtop
Welcome to Coq 8.3pl2 (April 2011)

Coq < Require Import Classical.


Coq < Lemma peirces_law : forall (p q : Prop), ((p -> q) -> p) -> p.
1 subgoal

  
  ============================

   forall p q : Prop, ((p -> q) -> p) -> p

peirces_law < Proof.

peirces_law < intros.
1 subgoal

  
  p : Prop

  q : Prop
  H : (p -> q) -> p

  ============================
   p

peirces_law < apply imply_to_or.
Toplevel input, characters 6-17:

> apply imply_to_or.
>       ^^^^^^^^^^^

Error: Impossible to unify "~ ?1 \/ ?2" with "p".

What am I doing wrong?

I think Coq is attempting to rewrite the goal (p) using imply_to_or, but I want Coq to rewrite H.

Cheers,

Andrew Pennebaker

www.yellosoft.us