4

我想以某种方式限制允许构造函数在归纳定义中采用的输入类型。假设我想说定义二进制数如下：

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

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

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

而以下不是：

S (S 0)
D 0

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

4

2 回答 2

7

您可以bin用谓词定义 a 合法的含义，然后为bin服从该谓词的 s 子集命名。Program Definition然后你用andProgram Fixpoint代替Definitionand编写函数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 :=

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

于 2012-12-23T23:28:56.740 回答
1

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

从面向对象编程的角度来看，O和D是S的子类型bin，它们的构造函数类型可以在不借助逻辑谓词的情况下定义，但 Coq 本身也不支持面向对象编程。

然而，Coq 确实有类型类。所以我可能会做bin一个类型类，让每个构造函数成为一个单独的归纳类型，每个都有一个类型类的实例bin。我不确定类型类的方法是什么。

于 2012-12-23T10:12:07.443 回答