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

Question

我有时会在 Coq 中看到这种语法来表示某些 types/sets 例如在打印有关存在变量的信息时：

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

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

这是什么意思？

第一个和

一样吗

? T : Set

?

Answer 1

我可能弄错了，但第一个应该读作 "the existential variable named T is of type Set"，第二个应该读作 "the existential variable named T0 is of type Set, in a context where the variable x is of type ?T"，这意味着填充第二个洞的术语可能取决于一些名为 x.

的变量

Answer 2

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

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，但是只有假设论证（名为 ?n）的类型为 nat。或者换句话说，"under the assumption that one can infer that the type of ?n is nat from the empty context".

有时会在 "turnstile" 符号 |- 的左侧找到更多内容。

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 不可键入。

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

What's the square bracket syntax [ |- Set] in Coq?

coq