Coq 中的受限归纳类型定义

Question

我希望能够限制归纳定义中构造函数所允许的输入类型。比如说，我想要这样定义二进制数：

Inductive bin : Type :=
  | O : bin
  | D : bin -> bin
  | S : bin -> bin.

这里的思想是通过在末尾添加零来使非零数字加倍，而S则将以零结尾的数字的最后一位变为1。这意味着以下数字是合法的：

S 0
D (S 0)
D (D (S 0))

以下内容不符合要求：

S (S 0)
D 0

有没有一种干净的方法在归纳定义中实施这样的限制？

- pki

Answer 1

你可以用谓词定义一个 "bin" 的合法性，并给符合该谓词的 "bin" 子集命名。然后，你可以使用 Program Definition 和 Program Fixpoint 来编写函数，而不是使用 Definition 和 Fixpoint。对于递归函数，你还需要一个度量标准来证明函数的参数大小会随着函数的调用而减小，因为这些函数不再具有结构递归性。

Require Import Coq.Program.Program.

Fixpoint Legal (b1 : bin) : Prop :=
  match b1 with
  | O       => True
  | D O     => False
  | D b2    => Legal b2
  | S (S _) => False
  | S b2    => Legal b2
  end.

Definition lbin : Type := {b1 : bin | Legal b1}.

Fixpoint to_un (b1 : bin) : nat :=
  match b1 with
  | O    => 0
  | D b2 => to_un b2 + to_un b2
  | S b2 => Coq.Init.Datatypes.S (to_un b2)
  end.

Program Definition zer (b1 : lbin) := O.

Program Fixpoint succ (b1 : lbin) {measure (to_un b1)} : lbin :=

但是，这种简单类型化方法可能更容易。

- user1861759

---

这个答案似乎比其他答案更合理。我太懒了，没写一个。你可以将谓词作为附加参数，但是编写数字很麻烦。你可以不在意，在需要时进行规范化处理。 - Ptival

Answer 2

这可以通过归纳递归定义来完成，但不幸的是 Coq 不支持这些。

从面向对象编程的角度来看，O、D 和 S 是 bin 的子类型，它们的构造函数类型可以不使用逻辑谓词进行定义，但 Coq 也没有本地支持面向对象编程。

然而，Coq 有类型类。因此，我可以将 bin 设为一个类型类，并使每个构造函数成为单独的归纳类型，每个类型都具有 bin 类型类的实例。但我不确定类型类的方法是什么。

- Robin Green