The Coq mailing list

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

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