# Proving tautology with coq

Currently I have to learn Coq and don't know how to deal with an or :

As an example, as simple as it is, I don't see how to prove:

Theorem T0: x \/ ~x.


I would really appreciate it, if someone could help me.

For reference I use this cheat sheet.

Also an example of a proof I have in mind: Here for double negation:

Require Import Classical_Prop.

Parameters x: Prop.

Theorem T7: (~~x) -> x.
intro H.
apply NNPP.
exact H.
Qed.

• NNPP's type is forall p:Prop, ~ ~ p -> p., so it's cheating to use it to prove T7. When you import Classical_Prop you get Axiom classic : forall P:Prop, P \/ ~ P. – Anton Trunov Nov 26 '16 at 17:46
• So, apply classic. solves your goal for T0. – Anton Trunov Nov 26 '16 at 17:52

You cannot prove it in "vanilla" Coq, because it is based on intuitionistic logic:

From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not valid logical rules.

There are several ways you can deal with a situation like this.

• Introduce the law of excluded middle as an axiom:

Axiom excluded_middle : forall P:Prop, P \/ ~ P.


There is no more need to prove anything after this point.

• Introduce some axiom equivalent to the law of excluded middle and prove their equivalence. Here is just a few examples.

• Double negation elimination is one such axiom:

Axiom dne : forall P:Prop, ~~P -> P.

• Peirce's law is another example:

Axiom peirce : forall P Q:Prop, ((P -> Q) -> P) -> P.

• Or use one of the De Morgan's laws:

Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -> P \/ Q.

• Thank you a lot so far. I am not familiar with everything you have written, but will check though. I use the coqIde and in fact also got a proof for double negation, I added it to the problem description for more clarity later on. I expected there to be an analogous way for the problem given above. Maybe I should have included one example. – Imago Nov 26 '16 at 17:37
• @AntonTrunov you need to add some parenthesis to your Axiom peirce: as it stands it is not Peirce's law (and is in fact trivial to prove). – gallais Nov 26 '16 at 20:11
• @gallais Thanks for spotting that! Fixed. – Anton Trunov Nov 26 '16 at 20:18

As others informed you, your tautology is not a tautology unless you assume classical logic. But since you're doing tautologies on decidable truth values, you could use bool instead of Prop. Then your tautology holds:

Require Import Bool.

Lemma how_about_bool: forall (p : bool), Is_true (p || negb p).
Proof.
now intros [|].
Qed.