子集参数 [英] Subset parameter

问题描述

我有一个参数集：

Parameter Q:Set.

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

Now I want to define another parameter that is a subset of Q. Something like:

Parameter F: subset Q.

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

How I can define that? I guess I can add the restriction later as an axiom, but seems more natural to express it directly in the type of F.

推荐答案

您不能直接表达它。

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

It's misleading to think of objects in Set as mathematical sets. Set is the sort of datatypes, the same kinds of types that you find in programming languages (except that Coq's types are very powerful).

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

Coq doesn't have subtyping¹. If the two types F and Q are distinct, then they are disjoint, as far as the mathematical model is concerned.

通常的方法是将 F 声明为一个完全相关的集合，并从<$ c中声明规范注入$ c> F 到 Q 。您将要指定该注入的任何有趣的属性，而不是显而易见的。

The usual approach is to declare F as a completely related set, and declare a canonical injection from F to Q. You'll want to specify any interesting property of that injection, beyond the obvious.

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参考手册中有关于强制的一章。

That last line declares a coercion from F to Q. That lets you put an object of type F wherever the context requires the type Q. The type inference engine will insert a call to inj_F_Q. You will need to write the coercion explicitly occasionally, since the type inference engine, while very good, is not perfect (perfection would be mathematically impossible). There is a chapter on coercions in the Coq reference manual; you should at least skim through it.

另一种方法是使用扩展属性定义子集，即声明谓词 P Q 上的$ c>，并从 P定义 F code>。

Another approach is to define your subset with an extensional property, i.e. declare a predicate P on the set (the type) Q and define F from 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（乐趣x => P x））。您必须决定是选择短格式还是长格式（必须保持一致）。 Program 乡土语言在处理小笔款项时通常很有用。

sig is a specification, i.e. a weak sum type, i.e. a pair consisting of an object and a proof that said object has a certain property. sig P is eta-equivalent to {x | P x} (which is syntactic sugar sig (fun x => P x)). You have to decide whether you prefer the short or the long form (you need to be consistent). The Program vernacular is often useful when working with weak sums.

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

这篇关于子集参数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！