如何定义“类型包含”？

[zh] Coq 中文
1

我想定义“整数类型”。但是遇到了障碍
虽然，正数、负数和零并不是同一类型，
但是，正整数、负整数和零都是整数。
但是Coq似乎不允许类型之间的包含关系。
如何定义“整数”？有这样的功能吗？

1 Like
2

不甚理解你描述的“包含关系”，但Coq标准库有定义整数Z：

Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

更多函数支持收录于ZArith库。

1 Like
3

（不好意思，中文不是我的母语）
@Lys 懂的比我多得多，但是看你的疑问我觉得可能值得强调，用coq这种系统，一个数学来的“理想”有很多不同的定义……没有“最好”的，不过有的定义的代表性更好，或者认为更好用。比如，上述的Z的定义很正常，但是还能做其他的（比如你自己定的（neg nat, zero, pos nat））——这个要看你面对什么样的证明……其实，他们理想下是“一样”，但是做证明的时候有的定义更好用。我敢来这里用我非常差的中文说这句是因为我自己最近在学习coq，而学习过程中反复看同一个概念，就是没有“完美”的定义……不同的情况下有的定义更方便有的非常不方便。比如，lys分享的Z可能更容易extract到比较快的ocaml（software foundation里面有一个不错的解释）……但是我觉得用那个定义作证明会麻烦一点

请原谅我中文不好

1 Like
4

谢谢你的回答！
没想到这个小问题会耗了那么久的时间……
我想写出这样的定义，这样证明会方便些：

  • 0 对应 O
  • 1 对应 (S O)
  • 2 对应 (S (S O))
  • -1 对应 (K O)
  • -2 对应 (K (K O))

这样定义会十分统一且写证明也方便
如果Coq无法如此统一的定义整数
证明和一些函数可能就要多写点代码来处理……

如果真的不行，那么我只能多写点代码了

5

可修改类型定义使你的表达式变得合法：

Inductive int :=
| O
| S (n : int)
| K (n : int).

上述定义的弊端是一个整数存在多种表示，例如O和S (K O)均对应0。为避免此种情况，需要将整数定义为依存型（dependent type）：

Variant signal :=
| zero
| positive
| negative.

Inductive int : signal -> Set :=
| O : int zero
| S : int zero + int positive -> int positive
| K : int zero + int negative -> int negative.

但经验表明引入依存型通常使证明更加复杂。

1 Like
7

不好意思了……可能要麻烦一下
按照这个定义
Compute (S O).
报错：
The term “O” has type “int zero” while it is expected to have type
"(int zero + int positive)%type".

8

后一种类型定义下，1只能写为S (inl O)了。

9

我觉得最好还是顺着类型系统里面类型本身没有包含关系这个事实走，而不是一定要逆过来。对于你这样的需求我们一般是用另一个 A -> Prop 这样的 predicate 来表示的，而不是写在类型本身里面。

你可以试试用 sig，用一个类型 A 和一个对应的 A -> Prop 来表示一个受限制的类型。比如 { x: Z | x >= 0 } 就可以表达非负整数，这里可以理解为 Z 限定了这个值的形式，而 x >= 0 限定了它的性质。其实观察 sig 的定义就知道它是一个 Z 和一个 >= 的证明绑定起来。

还有一个办法是不绑定，需要 x 非负整数的时候多接收一个参数 x >= 0，效果是一样的。

对于前者我写了一个例子，你可以参考一下，也可以参考 Program 的文档。

Require Import ZArith Lia Program.

Open Scope Z_scope.

Definition Znat := { x : Z | x >= 0 }.
Definition Zpos := { x : Z | x > 0 }.

(* Manual construction *)

Lemma three_ge_zero : 3 >= 0.
Proof. lia. Qed. (* lia is a solver *)

Definition three_manual : Znat := exist _ 3 three_ge_zero.

(* Tactic *)

Definition three_tactic : Znat.
Proof.
  unfold Znat.
  exists 3.
  lia.
Qed.

(* Program *)
Program Definition three_program : Znat := 3.
(* Proof is automatic *)

(* Functions *)

Program Definition add_pos_nat (a : Zpos) (b : Znat) : Zpos := a + b.

Next Obligation.
  (*
  1 subgoal
  a : Zpos
  b : Znat
  ______________________________________(1/1)
  ` a + ` b > 0
  *)
  destruct a, b.
  cbn. lia.
Qed.
2 Likes
10

除了上述那些方法，类型包含还可以通过 implicit coercion 来模拟，比如定义 positive 和 Z，然后定义一个函数 pos_to_Z 从 positive 转换为 Z，并把这个函数定义为 implicit coercion（见：https://coq.inria.fr/refman/addendum/implicit-coercions.html ）
这种方式相比于使用 dependent types 的方法，好处是避免了 dependent types（在 Coq 中涉及 dependent types 的证明有时比较麻烦），坏处是有一个需要一定计算量的函数在那里，如果你需要经常从 pos 转到 Z，而且你在乎性能（比如你要导出 Coq 为 OCaml），那么这个方法性能可能会差一点（差多少取决于你的 pos_to_Z 函数）。

还有种方法是用 Data Type a la carte（http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf ）的方式来定义类型，不过这个有点复杂。

1 Like