子集参数

你不能直接表达它。 将

Set

中的物体视为数学集是错误的。

Set

是一种数据类型，与编程语言中的类型相同（除了Coq的类型非常强大）。 Coq没有子类型¹。如果两种类型

F

和

Q

是不同的，则就数学模型而言它们是不相交的。 通常的方法是将

F

声明为完全相关的集合，并声明从

F

到ѭ5的规范注入。除了显而易见之外，您还需要指定该注入的任何有趣属性。

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

到ѭ5强制。这使得您可以在上下文所需的类型

Q

处放置类型为

F

的对象。类型推理引擎将调用

inj_F_Q

。你需要偶尔明确写出强制，因为类型推理引擎虽然非常好，但并不完美（完美在数学上是不可能的）。 Coq参考手册中有一章有关强制的内容;你应该至少浏览它。 另一种方法是用扩展属性定义你的子集，即在集合（类型）decla5ѭ上声明一个谓词

P

，并从

P

定义

F

。

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

是e等价于

{x | P x}

（这是语法糖

sig (fun x => P x)

）。你必须决定你喜欢短形式还是长形式（你需要保持一致）。使用弱金额时，

Program

白话通常很有用。 ¹ 模块语言中有子类型，但这与此无关。并且强制假冒了很多用途的子类型，但它们并不是真实的东西。