nat_to_bin 的递归定义格式错误

如何解决nat_to_bin 的递归定义格式错误

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

这是我的代码/方法：

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

n0 : nat

n1 : nat

n2 : nat

递归调用 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 _) ) =>

if evenb n then B0 (nat_to_bin (Nat.div n 2 ) )

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

结束“。

解决方法

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

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

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

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

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

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