处理 `{ 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) 进行比较。

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

Q'：我对青少年的定义似乎是个死胡同；它比建设性更具声明性，我似乎失去了 nat 的归纳属性。我怎样才能显示它的居民？如果没有办法，我仍然可以坚持 nat 并使用 Prop 和函数。 （这里是新手，用Pierce's SF自学不到一周）。

Answer 1

您在teenagers 中使用的模式是“subType”模式的一个实例。正如您所指出的，{ x : nat | P x } 与 nat 不同。目前，Coq 几乎没有提供有效处理这些类型的支持，但如果您限制为 P 的“行为良好”类，您实际上可以以合理的方式工作。 [顺便说一句，这应该真的成为 Coq 常见问题解答]

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

描述这个接口超出了你原来的问题，所以我将以几个 cmets 结束：

• 在您的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的大类，可以证明teen_to_nat投影是单射的，即：

  forall t1 t2, teen_to_nat t1 = teen_to_nat t2 -> t1 = t2.
  

  然后，对基本类型的推理可以转移到子类型。另见：Inductive subset of an inductive set in Coq

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

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