How to prove that excluded mean is incontrovertible in Coq?

Question

I tried to prove the following simple theorem from an online course that excluded the middle, incontrovertibly, but got very stuck in 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 target will be P \/ ~P , which is excluded from the middle and cannot be proved constructively. But besides apply , I don’t know what can be done regarding 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 proved using only primitive tactics ( as described here , i.e. there are no mysterious auto s)?

Thanks.

Answer 1

I am not an expert on this, but it was recently discussed on the Coq mailing list . I will summarize from this topic. If you want to understand these issues in more detail, look at the double negation translation .

The problem falls into the intuitionistic propositional calculus and therefore can be defined by tauto .

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

The stream also contains more detailed evidence. I will try to explain how I could come up with this evidence. Please note that it is usually easier for me to deal with the interpretation of a programming language in a programming language, so what I will do:

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

We are invited to write a function that takes a function f and returns a value of type False . The only way to get to False at this point is to call f .

  apply f. 

Therefore, we will be asked to provide arguments to the function f . We have two options: go through P or P -> False . I do not see a way to build P , so I choose the second option.

  right. intro p. 

We will return to the square, except that now we have P ! Therefore, we apply f , because this is the only thing we can do.

  apply f. 

And again we will be asked to provide the argument f . This is easy, however, because we have P to work with.

  left. apply p. Qed. 

The flow also mentions a proof based on some simpler lemmas. The first lemma ~(P /\ ~P) .

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

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

 Lemma lma' (PQ: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 are sufficient to show:

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