Jak udowodnić, że środek wykluczenia jest nieodwracalny w Coq?

Question

starałem się udowodnić następujące proste twierdzenie z an online course że wyłączonego środka jest niepodważalne, ale utknął dość dużo w kroku 1:

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

Teraz otrzymujemy:

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

Jeśli I apply H, wtedy celem będzie P \/ ~P, który jest wykluczony w środku i nie można go udowodnić w sposób konstruktywny. Ale inne niż apply, nie wiem, co można zrobić w odniesieniu do hipotezy P \/ (P -> False) -> False: implikacja -> jest prymitywne, i nie wiem jak destruct lub rozkładać go. I to jest jedyna hipoteza.

Moje pytanie brzmi: jak można to udowodnić za pomocą jedynie prymitywnej taktyki (as characterized here, tj. Bez tajemniczych auto s)?

Dzięki.

Answer 1

Nie jestem ekspertem w tej dziedzinie, ale został niedawno omówiony na Coq mailing-list. Podsumuję wnioski z tego wątku. Jeśli chcesz lepiej zrozumieć tego typu problemy, powinieneś spojrzeć na double-negation translation.

Problem mieści się w intuicjonistycznym rachunku zdań i dlatego może zostać określony przez tauto.

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

Gwint zapewnia również bardziej złożony dowód. Spróbuję wyjaśnić, jak wymyśliłbym ten dowód. Należy pamiętać, że jest to zazwyczaj łatwiej mi radzić sobie z interpretacją języka programowania lematów, więc to, co zrobię:

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

Jesteśmy wezwani, aby napisać funkcję, która pobiera funkcję f i tworzy wartość typu False. Jedynym sposobem, aby dostać się do False w tym miejscu, jest wywołanie funkcji f.

apply f. 

W związku z tym prosimy o podanie argumentów funkcji f. Mamy dwie możliwości: albo przeprowadź P lub P -> False. Nie widzę sposobu na zbudowanie P, więc wybieram drugą opcję.

right. 
    intro p. 

Znów jesteśmy na pierwszym miejscu, z tym, że mamy teraz do pracy p! Stosujemy więc f, ponieważ jest to jedyna rzecz, którą możemy zrobić.

apply f. 

I znowu, jesteśmy proszeni o dostarczenie argumentu do f. Teraz jest to łatwe, ponieważ mamy do pracy p.

left. 
    apply p. 
Qed. 

Wątek wspomina również o dowodzie opartym na łatwiejszych lematach. Pierwszy lemat to ~(P /\ ~P).

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

Drugi lemat jest ~(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. 

Te lematy wystarczyć do pokazu:

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