nat_to_bin 的递归定义格式不正确

Question

我目前正在阅读软件基础系列的第一卷。在其中一个练习中，我应该编写一个函数，将自然数（一元形式）转换为等效的二进制数。

这是我的代码/方法：

Inductive bin : Type := 
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Fixpoint nat_to_bin (n:nat) : bin := 
  match n with
  | 0 => Z
  | 1 => B1 Z
  | 2 => B0 (B1 Z)
  | m => match evenb(m) with 
         | true => B0 (nat_to_bin (Nat.div m 2))
         | false => B1 (nat_to_bin (Nat.modulo m 2)) 
        end
  end.

我正在使用https://jscoq.github.io/scratchpad.html 进行这些练习。 现在我收到此错误消息：

nat_to_bin 的递归定义格式不正确。在环境中 nat_to_bin : nat -> bin

n : 自然

n0 : 自然

n1：自然

n2：自然

对 nat_to_bin 的递归调用的主要参数等于“Nat.div n 2 " 而不是以下变量之一： "n0" "n1" "n2" 。 递归定义为：“fun n : nat => match n with

| 0 => Z

| 1 => B1 Z

| 2 => B0 (B1 Z)

| S (S (S _) ) =>

如果 evenb n 那么 B0 (nat_to_bin (Nat.div n 2 ) )

else B1 (nat_to_bin (Nat.modulo n 2 ) )

结束“。

Answer 1

为了保持良好的逻辑属性，所有可在 Coq 中定义的函数都是终止的。为了强制执行这一点，对固定点定义有一个限制，就像您尝试做的那样，称为保护条件。这个限制大致就是递归调用只能在函数参数的子项上进行。

在您的定义中不是这种情况，您将nat_to_bin 应用于术语(Nat.div n 2) 和(Nat.modulo n 2)，它们是应用于n 的函数。尽管您可以在数学上证明它们总是小于n，但它们不是n 的子项，因此您的函数不遵守保护条件。

如果你想以你正在做的方式定义nat_to_bin，你需要求助于有根据的归纳，这将使用nat上的顺序的有根据来允许你调用你的函数在任何条件下，您都可以证明小于n。然而，这个解决方案相当复杂，因为它会迫使你做一些不那么容易的证明。

相反，我建议采用另一种方式：在本书的上面，建议定义一个函数incr : bin -> bin，它将二进制数加一。您可以使用它通过对n 的简单递归来定义nat_to_bin，如下所示：

Fixpoint nat_to_bin (n:nat) : bin := 
  match n with
  | 0 => Z
  | S n' => incr (nat_to_bin n')
  end.

至于incr 本身，您也应该能够使用二进制数的简单递归将其写下来，因为它们是用低位外部写入的。