infinite-loop - 在Coq中使用负归纳类型证明False

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

阅读您的问题使我意识到，我也不太理解亚当的论点。但是在这种情况下，不一致很容易由Cantor惯用的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.

这是一个通用开发，可以使用CPDT中定义的 term类型实例化: T将是 term， x和 y将是 term的两个元素，我们可以测试它们之间的区别(例如 App (Abs id) (Abs id)和 Abs id)。关键是最后一个假设:我们假设我们有一个可逆函数 g : (T -> T) -> T，在您的示例中为 Abs。使用该函数，我们将执行通常的对角化技巧:我们定义一个 kaboom函数，该函数的构造与每个函数 T -> T(包括其自身)都不同。由此产生矛盾。