Доказательство False с отрицательными индуктивными типами в Coq

Question

В третьей главе CPDT кратко обсуждается, почему отрицательные индуктивные типы запрещены в Coq. Если бы мы имели

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

тогда мы могли бы легко определить функцию

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

так, что термин uhoh (Abs uhoh) будет не-терминатор, с помощью которого «мы сможем доказать каждую теорему».

Я понимаю часть без прерывания, но я не понимаю, как мы можем что-то доказать с ней. Как можно доказать False с использованием term, как определено выше?

Answer 1

Чтение вашего вопроса заставило меня понять, что я не совсем понял аргумент Адама. Но несогласованность в этом случае довольно легко получается из обычного кантора diagonal argument (бесконечного источника парадоксов и головоломок в логике). Рассмотрим следующие предположения:

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. 

Это родовое развитие, которое может быть инстанцированный с типом term, определенным в CPDT: T будет term, x и y бы два элемента term, что мы можем испытать различать (например, App (Abs id) (Abs id) и Abs id). Ключевым моментом является последнее предположение: мы предполагаем, что у нас есть обратимая функция g : (T -> T) -> T, которая в вашем примере будет Abs. Используя эту функцию, мы играем обычный трюк диагонализации: мы определяем функцию kaboom, которая по конструкции отличается от любой функции T -> T, включая себя. Из этого вытекает противоречие.