coq - 子集参数

Question

我有一组作为参数：

Parameter Q:Set.

现在我想定义另一个参数，它是 Q 的一个子集。比如：

Parameter F: subset Q.

我该如何定义？我想我可以稍后将限制添加为公理，但直接用 F 的类型表示它似乎更自然。

Answer 1

你不能直接表达。

Set将对象视为数学集合是一种误导。Set是一种数据类型，与您在编程语言中发现的类型相同（除了 Coq 的类型非常强大）。

Coq 没有子类型¹。如果这两种类型F和Q是不同的，那么就数学模型而言，它们是不相交的。

通常的方法是声明为一个完全相关的集合，并声明一个从toF的规范注入。除了明显之外，您还需要指定该注入的任何有趣属性。FQ

Parameter Q : Set.
Parameter F : Set.
Parameter inj_F_Q : F -> Q.
Axiom inj_F_Q_inj : forall x y : F, inj_F_Q x = inj_F_Q y -> x = y.
Coercion inj_F_Q : F >-> Q.

最后一行声明了从Fto的强制转换Q。这使您可以将 type 对象放在F上下文需要 type 的任何位置Q。类型推理引擎将插入对inj_F_Q. 您偶尔需要显式地编写强制转换，因为类型推理引擎虽然非常好，但并不完美（完美在数学上是不可能的）。Coq 参考手册中有一个关于强制的章节；你至少应该浏览一下。

另一种方法是使用扩展属性定义您的子集，即P在集合（类型）上声明谓词Q并定义Ffrom P。

Parameter Q : Set.
Parameter P : Q -> Prop.
Definition G := sig P.
Definition inj_G_Q : G -> Q := @proj1_sig Q P.
Coercion inj_G_Q : G >-> Q.

sig是一种规范，即弱和类型，即由一个对象和该对象具有特定属性的证明组成的对。sig P是 eta 等价于{x | P x}（它是语法糖sig (fun x => P x)）。您必须决定是喜欢短格式还是长格式（您需要保持一致）。在处理弱和时，Program白话通常很有用。

¹ _{模块语言中有子类型，但这与这里无关。强制可以很好地伪造子类型，可以用于许多用途，但它们不是真实的。}