用 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) 将是非终止的，"we would be able to prove every theorem"。

我理解非终止部分，但我不明白我们如何用它来证明任何事情。如何使用上面定义的 term 来证明 False？

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，包括它自己。矛盾由此产生。

用 Coq 中的负归纳类型证明 False

Proving False with negative inductive types in Coq

infinite-loop

coq

non-termination