处理 `{ x : nat | 形式的（子）类型的最佳方式x >= 13 /\ x <= 19 }`?

Question

Coq 让我定义这个：

Definition teenagers : Set := { x : nat | x >= 13 /\ x <= 19 }.

还有：

Variable Julia:teenagers.

但不是 :

Example minus_20 : forall x:teenagers, x<20.

或：

Example Julia_fact1 : Julia > 12.

这是因为 Julia（类型 teenagers）无法与 12（nat）进行比较。

Q: 我应该如何通知 Coq Julia 的支持类型是 nat 以便我可以写任何关于她的有用信息？

Q': 我对青少年的定义似乎是一个死胡同；它比建设性更具陈述性，我似乎已经失去了 nat 的归纳特性。我怎样才能显示它的居民？如果没有办法，我还是可以坚持使用nat，使用Prop和函数。（这里是菜鸟，自学不到一周Pierce's SF）。

Answer 1

您在 teenagers 中使用的模式是 "subType" 模式的一个实例。正如您所注意到的，{ x : nat | P x } 不同于 nat。目前，Coq 几乎没有提供有效处理这些类型的支持，但如果您限制为 "well-behaved" class 的 P，您实际上可以以合理的方式工作。 [这真的应该成为 Coq FAQ 顺便说一句]

从长远来看，您可能希望对此模式使用特殊支持。 math-comp 库 subType 接口提供了这种支持的一个很好的例子。

描述这个界面超出了你原来的问题，所以我将以一些评论结束：

在您的 minus_20 示例中，您想要使用青少年数据类型的 第一个投影 。尝试 forall x : teenagers, proj1_sig x < 20。如果您将投影声明为 Coercion:

，Coq 可以尝试自动插入此类投影

Require Import Omega.

Definition teenagers : Set :=
  { x : nat | x >= 13 /\ x <= 19 }.

Coercion teen_to_nat := fun x : teenagers => proj1_sig x.

Implicit Type t : teenagers.

Lemma u t : t < 20.
Proof. now destruct t; simpl; omega. Qed.

正如您正确观察到的，{ x : T | P x } 在 Coq 中与 x 不同。原则上，您不能将推理从 T 类型的对象转移到类型 { x : T | P x } 的对象，因为您还必须另外推理类型 P x 的对象。但是对于P的宽class，可以证明teen_to_nat投影是单射的，即：
```
forall t1 t2, teen_to_nat t1 = teen_to_nat t2 -> t1 = t2.
```
然后，可以将对基类型的推理转移到子类型。另见：

[edit]: 我在 math-comp 中添加了几个典型的子类型示例，因为我认为它们很好地说明了这个概念：

大小列表或 n.-tuples。长度为 n 的列表在 math-comp 中表示为一对单个列表加上大小证明，也就是说 n.-tuple T = { s : seq T | size s == n}。由于单射性和强制性，您可以在元组上使用所有常规列表函数，它们工作正常。
有界自然数或序数：类似地，类型 'I_n = { x : nat | x < n } 与自然数几乎相同，但有界。

处理 `{ x : nat | 形式的（子）类型的最佳方式x >= 13 /\ x <= 19 }`?

Best way to handle (sub) types of the form `{ x : nat | x >= 13 /\ x <= 19 }`?

coq