12
$\begingroup$

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.
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Anton Trunov Nov 26 '16 at 17:46
  • $\begingroup$ So, apply classic. solves your goal for T0. $\endgroup$ – Anton Trunov Nov 26 '16 at 17:52
14
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Imago Nov 26 '16 at 17:37
  • 1
    $\begingroup$ @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). $\endgroup$ – gallais Nov 26 '16 at 20:11
  • $\begingroup$ @gallais Thanks for spotting that! Fixed. $\endgroup$ – Anton Trunov Nov 26 '16 at 20:18
6
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.