Coq中如何在Section内为Variable T指定具体类型定义示例树

问题场景 #

我在Coq中定义了如下Section：

Section bin_trees.

Variable T: Type.

Inductive bin_tree :=
  | Leaf : bin_tree
  | Node : T ->  bin_tree -> bin_tree -> bin_tree.

在bin_trees Section内尝试定义一个基于nat类型的示例树时，执行以下代码报错：

Definition my_nat_bin_tree := Node 3 Leaf Leaf.

错误提示：

Error: In environment
T : Type
The term "3" has type "nat"
while it is expected to have type 
"T".

疑问 #

能否为单个定义显式指定T为具体类型（如nat），比如写成Definition my_nat_bin_tree := @Node (T:=nat) 3 Leaf Leaf.？或者有没有关闭后重开Section的技巧，无需重新声明T就能引用它？

解决方案 #

1. 显式指定类型参数（你的思路可行） #

你提到的用@Node显式绑定类型参数的方法是有效的，但需要注意：当前Section内的Leaf同样依赖于全局的Variable T，所以必须同时为Leaf指定具体类型。正确写法如下：

(* 位置：bin_trees Section内 *)
Definition my_nat_bin_tree := @Node nat 3 (@Leaf nat) (@Leaf nat).

或者用命名参数的方式，可读性更强：

Definition my_nat_bin_tree := @Node (T:=nat) 3 (@Leaf (T:=nat)) (@Leaf (T:=nat)).

这两种写法都会绕过Section内的T约束，直接生成基于nat类型的二叉树。

2. 嵌套Section局部覆盖类型 #

如果不想反复写@符号，可以在当前bin_trees Section内嵌套一个小Section，局部覆盖T的取值：

Section bin_trees.

Variable T: Type.

Inductive bin_tree :=
  | Leaf : bin_tree
  | Node : T ->  bin_tree -> bin_tree -> bin_tree.

  (* 嵌套Section，局部将T指定为nat *)
  Section nat_tree_demo.
    Let T := nat.
    Definition my_nat_bin_tree := Node 3 Leaf Leaf.
  End nat_tree_demo.

End bin_trees.

嵌套Section中的Let T := nat会临时覆盖外部的Variable T，内部的Node和Leaf都会自动绑定到nat类型，关闭嵌套Section后就会回到原有的上下文环境。

3. 关闭Section后再定义示例 #

另一种更直接的方式是先关闭bin_trees Section，此时bin_tree会自动变成带类型参数的多态类型bin_tree : Type -> Type，之后直接定义示例即可：

Section bin_trees.

Variable T: Type.

Inductive bin_tree :=
  | Leaf : bin_tree
  | Node : T ->  bin_tree -> bin_tree -> bin_tree.

End bin_trees.

(* 此时bin_tree是带参数的类型，直接指定nat即可 *)
Definition my_nat_bin_tree := @Node nat 3 (@Leaf nat) (@Leaf nat).
(* 也可以用隐式参数写法，Coq会自动推断类型 *)
Definition my_nat_bin_tree' := Node (T:=nat) 3 (Leaf (T:=nat)) (Leaf (T:=nat)).

内容的提问来源于stack exchange，提问作者shooqie