时间戳

首页 > 解决方案 > nat_to_bin 的递归定义格式不正确

binary - nat_to_bin 的递归定义格式不正确

问题描述

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

这是我的代码/方法：

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

ñ：自然

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 ) )

否则 B1 (nat_to_bin (Nat.modulo n 2 ) )

结尾 ” 。

标签： binarycoq

解决方案

为了保持良好的逻辑属性，所有在 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它本身，您还应该能够使用二进制数的简单递归将其写下来，因为它们是用外部低位写入的。

推荐阅读