Come dimostrare l'esclusione di mezzo è inconfutabile in Coq?

Question

Stavo cercando di dimostrare il seguente semplice teorema da an online course che escludeva centrale è inconfutabile, ma è rimasto bloccato praticamente al passo 1:

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

Ora ho:

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

Se io apply H, quindi l'obiettivo sarebbe P \/ ~P, che è escluso al centro e non può essere provato in modo costruttivo. Ma diverso da apply, non so cosa si possa fare riguardo all'ipotesi P \/ (P -> False) -> False: l'implicazione -> è primitiva, e non so come fare a destruct o scomporla. E questa è l'unica ipotesi.

La mia domanda è, come può essere provato usando solo tattiche primitive (as characterized here, cioè senza misterioso auto s)?

Grazie.

Answer 1

Non sono un esperto in materia, ma è stato recentemente discusso su . Riassumo le conclusioni di questo thread. Se vuoi capire meglio questo tipo di problemi, dovresti dare un'occhiata a double-negation translation.

Il problema rientra nel calcolo proposizionale intuizionista e può quindi essere deciso da tauto.

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

Il thread fornisce anche una prova più elaborata. Cercherò di spiegare come mi sarebbe venuta in mente questa prova. Si noti che di solito è più facile per me a che fare con l'interpretazione linguaggio di programmazione di lemmi, in modo che è quello che farò:

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

Ci viene chiesto di scrivere una funzione che prende la funzione f e produce un valore di tipo False. L'unico modo per arrivare a False a questo punto è invocare la funzione f.

apply f. 

Di conseguenza, ci viene chiesto di fornire gli argomenti alla funzione f. Abbiamo due scelte, o passare P o P -> False. Non vedo un modo per costruire un P quindi sto scegliendo la seconda opzione.

right. 
    intro p. 

siamo di nuovo al punto di partenza, se non che ora abbiamo un p lavorare con! Quindi applichiamo f perché è l'unica cosa che possiamo fare.

apply f. 

E ancora, ci viene chiesto di fornire l'argomento f. Questo è facile ora, però, perché abbiamo un p con cui lavorare.

left. 
    apply p. 
Qed. 

Il thread menziona anche una prova basata su alcuni lemmi più semplici. Il primo lemma è ~(P /\ ~P).

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

Il secondo lemma è ~(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. 

Questi lemmi sono sufficienti per lo spettacolo:

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