如何證明被排除的中間在Coq中是無可辯駁的？

Question

我試圖從an online course即排除中間是無可辯駁的證明了如下簡單的定理，但在步驟1中卡住了相當多：

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

現在，我得到：

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

如果我apply H，那麼目標將是P \/ ~P，這被排除在外，並且不能被建設性地證明。但除了apply，我不知道可以做什麼關於假設P \/ (P -> False) -> False：暗示->是原始的，我不知道如何destruct或分解它。這是唯一的假設。

我的問題是，如何才能證明僅使用原始策略（as characterized here，即沒有神祕的auto s）？

謝謝。

Answer 1

我不是這方面的專家，但最近在Coq mailing-list上討論過。我將總結這個主題的結論。如果你想更徹底地理解這些問題，你應該看看double-negation translation。

該問題屬於直覺主義命題演算，因此可由tauto決定。

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

該線程還提供了更詳細的證明。我會試着解釋我將如何提出這個證明。請注意，它通常是容易，我應對引理的編程語言解釋，所以這就是我會做：

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

我們被要求寫一個函數，該函數f和生產類型的值False。此時到達False的唯一方法是調用函數f。

apply f. 

因此，我們被要求爲函數f提供參數。我們有兩種選擇，通過P或P -> False。我沒有看到構建P的方法，所以我選擇了第二個選項。

right. 
    intro p. 

我們又回到原點，只是我們現在有一個p一起工作！ 所以我們應用f，因爲這是我們唯一能做的事情。

apply f. 

再次，我們被要求提供參數f。但現在這很容易，因爲我們有一個p來處理。

left. 
    apply p. 
Qed. 

該線程還提到了基於一些更簡單的引理的證明。第一個引理是~(P /\ ~P)。

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

第二引理是~(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. 

這些引理足以顯示：

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