coq - Coq 中的受限归纳类型定义

Question

我想以某种方式限制在归纳定义中允许什么样的输入构造函数。说我想说定义二进制数如下:

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

这里的想法是 D 通过在末尾添加一个零来将一个非零数字加倍，而 S 将一个以零作为最后一位的数字并将最后一位数字变成一。这意味着以下是合法数字:

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

而以下不会:

S (S 0)
D 0

有没有办法以干净的方式在归纳定义中强制执行此类限制？

Answer 1

您可以定义 bin 的含义谓词合法，然后为 bin 的子集命名s 服从那个谓词。然后你用 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 :=

但是 this简单类型的方法可能会更容易。