coq - Coq 中单例类型单元的归纳原理是如何工作的？

Question

我正在阅读 Adam Chlipala 关于 Coq 的书，它定义了归纳类型：

Inductive unit : Set :=
  | tt.

我试图理解它的归纳原理：

Check unit_ind.
(* unit_ind
     : forall P : unit -> Prop, P tt -> forall u : unit, P u *)

我不确定我是否理解 Coq 的输出是什么意思。

1）所以检查让我看看“对象”的类型对吗？所以unit_ind有类型：

forall P : unit -> Prop, P tt -> forall u : unit, P u

正确的？

2）如何阅读该类型？我无法理解将括号或其他内容放在哪里......对于逗号之前的第一件事，我将其读作是没有意义的：

IF "for all P of type unit" THEN " Prop "

因为这个假设并不是真的或假的。所以我假设真正的第一件事是这样的：

forall P : (unit -> Prop), ...

所以 P 只是一个单位类型的函数来支持。这个对吗？

我希望这是正确的，但在这种解释下，我不知道如何阅读第一个逗号之后的部分：

P tt -> forall u : unit, P u

我本来希望在命题的开头定义所有存在的变量的量化，但这不是它是如何完成的，所以我不确定发生了什么......

有人可以帮助我正式和直观地阅读这个命题吗？我还想从概念上理解它想要表达的意思，而不仅仅是被它的细节所困扰。

标签： coq

Answer 1

让我放一些额外的（不是真的必要的）括号：

forall P : unit -> Prop, P tt -> (forall u : unit, P u)

我会将其翻译为“对于任何P类型的谓词unit，如果P持有tt，则P持有任何类型的术语unit”。

直观地说，因为tt是 type 的唯一值，所以只证明这个唯一值unit是有意义的。P

bool您可以通过尝试以相同方式解释类型的归纳原理来检查这种直觉是否适合您。

Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> (forall b : bool, P b)