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 :=

但这种简单的方法可能会更容易.