使用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.

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