Dowodzenie Fałszywy z ujemnymi typami indukcyjnymi w Coq

Question

Trzeci rozdział CPDT krótko omawia, dlaczego negatywne typy indukcyjne są zabronione w Coq. Gdybyśmy mieli

Inductive term : Set := 
| App : term -> term -> term 
| Abs : (term -> term) -> term. 

wtedy możemy łatwo zdefiniować funkcję

Definition uhoh (t : term) : term := 
    match t with 
    | Abs f => f t 
    | _ => t 
    end. 

więc, że termin uhoh (Abs uhoh) byłoby nie kończący, z której „będziemy w stanie udowodnić każde twierdzenie”.

Rozumiem część nieterminacyjną, ale nie rozumiem, w jaki sposób możemy to udowodnić. Jak udowodnić, False przy użyciu term, jak zdefiniowano powyżej?

Answer 1

Czytanie tego pytania uświadomiło mi, że nie całkiem rozumiem argument Adama. Ale niekonsekwencja w tym przypadku wynika dość łatwo ze zwykłego Cantana diagonal argument (niekończącego się źródła paradoksów i zagadek logicznych). Rozważmy następujące założenia:

Section Diag. 

Variable T : Type. 

Variable test : T -> bool. 

Variables x y : T. 

Hypothesis xT : test x = true. 
Hypothesis yF : test y = false. 

Variable g : (T -> T) -> T. 
Variable g_inv : T -> (T -> T). 

Hypothesis gK : forall f, g_inv (g f) = f. 

Definition kaboom (t : T) : T := 
    if test (g_inv t t) then y else x. 

Lemma kaboom1 : forall t, kaboom t <> g_inv t t. 
Proof. 
    intros t H. 
    unfold kaboom in H. 
    destruct (test (g_inv t t)) eqn:E; congruence. 
Qed. 

Lemma kaboom2 : False. 
Proof. 
    assert (H := @kaboom1 (g kaboom)). 
    rewrite -> gK in H. 
    congruence. 
Qed. 

End Diag. 

To jest ogólny rozwój, który może być tworzony z rodzaju term określonym w CPDT: T byłby term, x i y byłyby dwa elementy term że możemy testować dyskryminuje (np. App (Abs id) (Abs id) i Abs id). Kluczowym punktem jest ostatnie założenie: zakładamy, że mamy funkcję odwracalną g : (T -> T) -> T, która w twoim przykładzie byłaby Abs. Korzystając z tej funkcji, odgrywamy zwykłą sztuczkę diagonalizacji: definiujemy funkcję kaboom, która jest zbudowana inaczej niż każda funkcja T -> T, włączając samą siebie. Sprzeczność wynika z tego.