coq - 子集参数

Question

我有一组作为参数:

Parameter Q:Set.

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

Parameter F: subset Q.

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

Answer 1

你不能直接表达。

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

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

通常的做法是声明F作为一个完全相关的集合，并从 F 声明一个规范注入(inject)至Q .除了明显之外，您还需要指定该注入(inject)的任何有趣属性。

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.

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

另一种方法是使用扩展属性定义您的子集，即声明谓词 P在片场(类型) Q并定义 F来自 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在处理弱和时，白话通常很有用。

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