Coq 中受限的归纳类型定义答案

【问题标题】：Restricted inductive type definitions in CoqCoq 中受限的归纳类型定义
【发布时间】：2012-12-10 03:08:10
【问题描述】：

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

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

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

【问题讨论】：

标签： coq

【解决方案1】：

您可以定义bin 对谓词合法的含义，然后为服从该谓词的bins 的子集命名。然后用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 简单类型的方法可能会更容易。

【讨论】：

这似乎比其他答案更合理。我懒得写一篇了。您可以将谓词作为附加参数，但是写数字很烦人。您可以在需要时不关心和规范化。

【解决方案2】：

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

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

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

【讨论】：