我正在学习这个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
功能?
我是否必须为这里描述的有根据的递归提供证明?
我认为有一个更简单的解决方案,因为它是一个新手教程?