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只是类型单位到prop的函数.它是否正确？

我希望这是正确的,但根据这种解释,我不知道如何在第一个逗号后阅读该部分:

P tt -> forall u : unit, P u

我原本期望存在的变量的所有量化都在命题的开头定义,但那不是它的完成方式,所以我不确定是怎么回事......

有人能帮助我正式和直观地阅读这个命题吗？我还想从概念上理解它想要说的是什么,而不仅仅是被它的细节所打扰.

Answer 1

让我加一些额外的(不是必要的)括号:

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

"对于任何谓语我将它翻译为P过unit,如果类型,P持有tt,然后P类型的任何条款持有unit".

直观地说,因为tt它是唯一的类型值unit,所以只证明P这个唯一值是有意义的.

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

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