coq - 处理 `{ 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(青少年类型)无法与 12(nat)进行比较。

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

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

Answer 1

您在 teenagers 中使用的模式是“subType”模式的一个实例。正如您所注意到的，{ x : nat | P x }不同于nat .目前，Coq 提供很少的支持来有效处理这些类型，但如果您限制为“行为良好”的类 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 , 你可以证明 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 }与自然数几乎相同，但有界限。