我正在阅读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)所以check让我看一看“对象”的类型,对吗?所以unit_ind
有以下类型:
forall P : unit -> Prop, P tt -> forall u : unit, P u
对吗?
2)如何读取该类型?我很难理解在逗号之前应该把括号或something...For放在哪里,这对我来说是没有意义的:
IF "for all P of type unit" THEN " Prop "
因为假设并不是真的或假的。所以我假设真正实现的第一件事是这样:
forall P : (unit -> Prop), ...
所以P只是类型unit to prop的函数。这是正确的吗?
我希望这是正确的,但在这种解释下,我不知道如何阅读第一个逗号后面的部分:
P tt -> forall u : unit, P u
我希望在命题一开始就定义现有变量的所有量化,但这不是它是如何完成的,所以我不确定发生了什么……
有人能帮我从形式上和直观上阅读这个命题吗?我还想从概念上理解它试图表达的意思,而不仅仅是被它的细节所困扰。
发布于 2018-12-17 05:44:21
让我加一些额外的(不是真正必要的)括号:
forall P : unit -> Prop, P tt -> (forall u : unit, P u)
我会将其翻译为“对于unit
类型上的任何谓词P
,如果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)
https://stackoverflow.com/questions/53806590
复制相似问题