如何在 Coq 中声明某种归纳类型的常量？

【问题标题】：How to declare constant of some inductive type in Coq?如何在 Coq 中声明某种归纳类型的常量？
【发布时间】：2023-10-10 20:16:01
【问题描述】：

我关注https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v 并在那里定义了归纳类型（参数化的高阶抽象语法 - 此处使用 PHOAS）：

(** Closed Terms *)
  Inductive ClosedT : Term -> Prop :=
  | cl_cte: forall C, ClosedT (Cte C)
  | cl_fc1: forall n t1, ClosedT t1 -> ClosedT (FC1 n t1)
  | cl_fc2: forall n t1 t2, ClosedT t1 -> ClosedT t2 -> ClosedT (FC2 n t1 t2).

我的问题是 - 如何使用构造函数 cl_cte 将常量 John 定义为 ClosedT 类型？

还有一个问题：在某些情况下，我想定义更多类型，例如John : Person 和 Bruno : Tortoise 所以 - 我应该创建新类型，例如ClosedT_Tortoise 新类型？ ClosedT 是构建对象逻辑的基本类型，所以，也许我不应该继续使用多分类逻辑？

据我了解，我正在使用的线性逻辑的这种形式化应用于另一个 Coq 项目http://subsell.logic.at/bio-CTC/，并且可能在那里定义了常量。但是浏览源我找不到它们。

【问题讨论】：

标签： logic coq

【解决方案1】：

严格来说，您的问题表述不当：ClosedT 不是一个类型，而是由Term 类型的元素索引的一系列命题。根据该文件，我认为ClosedT t 意味着术语t : Term 已关闭，并且您想要执行以下操作：

定义一个常量类型T，它有一个元素John : T。
使用T 实例化开发的定义。为此，您需要将T 包装在Eqset_dec_pol 类型的模块中，同时证明T 具有可判定的相等性，并将出现在文件开头的函子Syntax_LL 应用于此模块。
使用Term 的Cte“构造函数”将John 嵌入术语的语法中。（这不是 Coq 正确意义上的构造函数，而只是一个方便的包装器，用于构建 Term 类型的元素。）
证明这个词是封闭的；即证明ClosedT (Cte John)。这应该只是应用构造函数cl_cte 的问题。

这或多或少符合您想要做的事情吗？

【讨论】：