The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  First of all, since Peirce's law is logically equivalent to classical 
logic, you need to import the Classical module of Standard Library, 
which contains double negation elimination.

NNPP: forall p : Prop, ~ ~ p -> p


I attached a file with the coq proof, that uses also double negation 
elimination, and reductio ad absurdum (through negation elimination).

I put all the steps on purpose, in order to allow you to look att every 
detail and compare it with your hand made proof. In everyday's life, the
proof script will be much shorter.

Hope this helps,
Pierre




Le 02/11/2011 07:30, Andrew Pennebaker a écrit :
> I want to prove Peirce's Law in Coq, but I'm uncertain of the Coq syntax
> for each step of the hand proof.
>
> Hand proof:
>
> Peirce's Law: ((p -> q) -> p) -> p
>
> (p -> q) -> p        ASSUMPTION
> ~(p -> q) | p        ENTAILMENT
>
>      [~(p -> q)]      ASSUMPTION
>      ~(~p | q)        ENTAILMENT
>      ~~p, ~q          DEMORGAN
>      ~~p              AND-ELIMINATION
>      p                DOUBLE NEGATION
>
>      [p]              ASSUMPTION
>      p                IDENTITY
>
> p                    EXHAUSTION
>
> ====================================
> ((p -> q) -> p) -> p
>
> Qed.
>
> Just to be sure, is my hand proof correct?
>
> Coq Questions:
>
> How do I declare the assumption (p -> q) -> p? In the tutorials, I see a
> variety of declaration syntaxes using Variables, Inductuctives,
> Definitions, Theorems, and Lemmas. If I declare one of the those, how do
> I assume it (e.g., assume that entailment means (a -> b) <-> (b | ~a)?
>
> How do I rewrite terms (e.g. using entailment or DeMorgan declarations)?
>
> How do I go through each possible cases (e.g. ~(p -> q) or p)?
>
> I suspect entailment, DeMorgan's laws, and and-elimination are each
> included in some Coq tactic library or other, and I would like to know
> how to leverage them. However, as part of the learning process, my first
> priority is figuring out how to manually implement them in what should
> be a relatively simple exercise, proving Peirce's Law.
>
> Cheers,
>
> Andrew Pennebaker
> www.yellosoft.us <http://www.yellosoft.us>

Require Import Classical.

Section Peirce_law_proof.

Variables P Q : Prop.

Lemma Peirce_law : ((P->Q)->P)-> P.
Proof.
 intro p.
 SearchPattern (~~ _ -> _). 

 
  apply NNPP.
  intro H.
  apply H.
 apply p.
 intro H0.
 
   destruct H.
 assumption.
Qed. 

End Peirce_law_proof.




Check Peirce_law.
(*
Peirce_law
     : forall P Q : Prop, ((P -> Q) -> P) -> P
*)