How to prove excluded middle is irrefutable in Coq?

Question

I was trying to prove the following simple theorem from an online course that excluded middle is irrefutable, but got stuck pretty much at step 1:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

Now I get:

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

If I apply H, then the goal would be P \/ ~P, which is excluded middle and can't be proven constructively. But other than apply, I don't know what can be done about the hypothesis P \/ (P -> False) -> False: implication -> is primitive, and I don't know how to destruct or decompose it. And this is the only hypothesis.

My question is, how can this be proven using only primitive tactics (as characterized here, i.e. no mysterious autos)?

Thanks.

Judie

Perhaps looking at the proof term (created with tauto and some simplification) makes some sense: Check fun (P : Prop) (H : ~ (P \/ ~ P)) => False_ind False (H (or_intror (fun H0 => H (or_introl H0)))). – Sextuplet

Answer 1

I'm not an expert on this subject, but it was recently discussed on the Coq mailing-list. I'll summarize the conclusion from this thread. If you want to understand these kinds of problems more thoroughly, you should look at double-negation translation.

The problem falls within intuitionistic propositional calculus and can thus be decided by tauto.

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  tauto.
Qed.

The thread also provides a more elaborate proof. I'll attempt to explain how I would have come up with this proof. Note that it's usually easier for me to deal with the programming language interpretation of lemmas, so that's what I'll do:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  unfold not.
  intros P f.

We are asked to write a function that takes the function f and produces a value of type False. The only way to get to False at this point is to invoke the function f.

 apply f.

Consequently, we are asked to provide the arguments to the function f. We have two choices, either pass P or P -> False. I don't see a way to construct a P so I'm choosing the second option.

  right.
  intro p.

We are back at square one, except that we now have a p to work with! So we apply f because that's the only thing we can do.

  apply f.

And again, we are asked to provide the argument to f. This is easy now though, because we have a p to work with.

  left.
  apply p.
Qed. 

The thread also mentions a proof that is based on some easier lemmas. The first lemma is ~(P /\ ~P).

Lemma lma (P:Prop) : ~(P /\ ~P).
  unfold not.
  intros H.
  destruct H as [p].
  apply H.
  apply p.
Qed.

The second lemma is ~(P \/ Q) -> ~P /\ ~Q:

Lemma lma' (P Q:Prop) : ~(P \/ Q) -> ~P /\ ~Q.
  unfold not.
  intros H.
  constructor.
  - intro p.
    apply H.
    left.
    apply p.
  - intro q.
    apply H.
    right.
    apply q.
Qed.   

These lemmas suffice to the show:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  intros P H.
  apply lma' in H.
  apply lma in H.
  apply H.
Qed.

Soukup

+1Thanks for the pointer. This works as advertised. But it's still mysterious as the mailing list said. (The interpretation in the mailing list is written with non-English characters, and the math part is really difficult to read). Any chance you could add interpretation of the big picture in English? – Judie