如何在 Fixpoint 定义 Coq 中创建条件

Question

我正在研究“软件基础”一书，并且正在研究第二章的最后一个问题。问题要求将自然数转换为二进制数，其中二进制数的定义方式如下：

  - [is] zero,
  - [is] twice a binary number, or
  - [is] one more than twice a binary number.

我的思考过程是，如果一个自然数是偶数，那么它可以表示为

double(nat_to_bin n)

但是，在我的 Fixpoint 定义中，当我尝试编写时

(evenb n' = true) => double(nat_to_bin)

我收到一个错误，因为 evenb n' 不是 nat 的构造函数。我有什么办法可以创建一个条件，使上面的行成为一个有效的函数定义，而不改变 nat 的定义？

Answer 1

没关系，我想出了一个解决方案。我可以写这个词

match (evenb n') with
| true => ....

不过花了我一段时间。