The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Andrew,

As first, Peirce's Law is not provable in the core of the system Coq. To
prove it you have to import the module Classical (module for classical
propositional reasoning).

But then it is provable directly using tactic tauto:

Coq < Theorem Peirce : forall p q : Prop, ((p -> q) -> p) -> p.
1 subgoal

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

Peirce < Require Import Classical.

Peirce < intros;
Peirce < tauto.
Proof completed.

Regarding your uncertainty in Coq, I think you'll still need to contact
Bertot-Casteran book or Coq's Reference Manual.

Best regards,

Marko Malikoviæ

> 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
>


-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------