Proving False con tipi induttivi negativi in ​​Coq

Question

Il terzo capitolo di CPDT illustra brevemente perché i tipi induttivi negativi sono vietati in Coq. Se avessimo

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

allora potremmo facilmente definire una funzione

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

in modo che il termine uhoh (Abs uhoh) sarebbe non fatale, con la quale "saremmo in grado di dimostrare ogni teorema".

Capisco la parte senza terminazione, ma non capisco come possiamo provare qualcosa con esso. Come si dimostrerebbe False utilizzando term come definito sopra?

Answer 1

Leggendo la tua domanda mi sono reso conto che non capivo nemmeno l'argomento di Adam. Ma incoerenza in questo caso risulta abbastanza facilmente dal solito diagonal argument di Cantor (fonte inesauribile di paradossi e puzzle in logica). Considerate le seguenti ipotesi:

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. 

Questo è uno sviluppo generico che può essere istanziata con il tipo term definito in CPDT: T sarebbe term, x e y sarebbero due elementi di term che possiamo testare discriminare tra (es. App (Abs id) (Abs id) e Abs id). Il punto chiave è l'ultima ipotesi: supponiamo di avere una funzione invertibile g : (T -> T) -> T che, nel tuo esempio, sarebbe Abs. Usando questa funzione, suoniamo il solito trucco di diagonalizzazione: definiamo una funzione kaboom che è per costruzione diversa da ogni funzione T -> T, incluso se stessa. La contraddizione ne deriva.