2

我正在学习这个Coq 教程，但我坚持最后的练习之一。我为自然数的二进制表示定义了一个数据类型，现在我想将自然数转换为这种表示：

Inductive bin : Type :=
  | BO : bin
  | TO : bin -> bin
  | T1 : bin -> bin.

我的第一个天真的方法是这样的：

Fixpoint divmod_2 (n : nat) :=
  match n with
  | O => (O, 0)
  | S O => (O, 1)
  | S (S n') => match (divmod_2 n') with
                | (q, u') => ((S q), u')
                end
  end.

Fixpoint to_bin (n : nat) : bin :=
  match n with
  | O => BO
  | S n' => match divmod_2 n' with
            | (q, 0) => TO (to_bin q)
            | (q, 1) => T1 (to_bin q)
            | (_, _) => BO
            end
  end.

Coq 停留在to_bin说的定义上：

Error:
Recursive definition of to_bin is ill-formed.
In environment
to_bin : nat -> bin
n : nat
n' : nat
q : nat
n0 : nat
Recursive call to to_bin has principal argument equal to "q" instead of
"n'".

所以这里的问题是：我该如何修复这个to_bin功能？
我是否必须为这里描述的有根据的递归提供证明？
我认为有一个更简单的解决方案，因为它是一个新手教程？

4

1 回答 1

4

我认为最简单的解决方案是首先为二元自然数定义一个后继函数，然后使用它来转换一元自然数的后继函数。

于 2013-02-21T21:45:46.290 回答