Доказательство Ложь с отрицательными индуктивными типами в 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

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

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включая себя. Противоречие вытекает из этого.