coq - Coq 中的方括号语法 [ |- Set] 是什么？

Question

我有时会在 Coq 中看到这种语法来表示某些类型/集合，例如打印有关存在变量的信息:

?T : [ |- Set]
?T0 : [ x : ?T |- Set ]

我不知道如何搜索这个语法。

这是什么意思？

是否和第一个一样

? T : Set

?

Answer 1

假设我们有一个特定类型的术语。

Variable B : nat -> nat.
Check B.
(*
B
     : nat -> nat
 *)

如果我们使用 B 创建另一个术语，它可能会或可能不会进行类型检查，即 B true 是不可类型的。

Fail Check B true.
(*
 Error message:
 The term "true" has type "bool" while it is expected to have type "nat".
 *)

Coq 允许在术语中使用通配符，然后尝试找出类型本身。

Check B _.
(*
B ?n
     : nat
where
?n : [ |- nat]
 *)

这里 Coq 说 B _ 的类型是 nat，但是 only假设论证(名为 ?n)的类型为 nat。或者换句话说，“假设可以从空上下文中推断出 ?n 的类型是 nat”。

有时在“旋转门”符号 |- 的左侧会发现更多内容。

Variable x:nat.
Check _ x.
(*
?y x
     : ?T@{x:=x}
where
?y : [ |- forall x : nat, ?T] 
?T : [x : nat |- Type] 
*)

下划线以上称为?y，(?y x)的类型是一个依赖类型?T，它依赖于x。 ?T 只能在 x 是 nat 的上下文中输入(到 Type)。如果 x 不是 nat，则 ?T 不可键入。