子集参数

Question

我有一个参数集:

Parameter Q:Set.

现在我想定义另一个参数,它是Q的一个子集.类似于:

Parameter F: subset Q.

我该如何定义？我想我可以稍后将限制添加为公理,但似乎更自然地直接在F的类型中表达它.

Answer 1

你不能直接表达它.

将对象Set视为数学集合会产生误导.Set是一种数据类型,在编程语言中找到的类型相同(除了Coq的类型非常强大).

Coq没有子类型¹.如果两种类型的F和Q是不同的,那么他们是不相交的,至于数学模型关注.

通常的办法是声明F作为一个完全相关的组,并从声明规范注射F到Q.除了显而易见之外,您还需要指定该注入的任何有趣属性.

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是η等价的{x | P x}(这是语法糖sig (fun x => P x)).你必须决定你喜欢短形式还是长形式(你需要保持一致).Program在使用弱金额时,白话通常很有用.

¹ _{模块语言中有子类型,但这与此无关.并且强制假冒了很多用途的子类型,但它们并不是真实的东西.}