在“软件基础”中有一个练习，我一直试图正确解决一段时间，但实际上我试图写下要求的功能。这是练习的相关部分
使用二元而不是一元系统考虑自然数的不同的，更有效的表示。也就是说，不是说每个自然数都是零或自然数的后继，我们可以说每个二进制数都是
- 零，
- 两倍于二进制数，或
- 二进制数的两倍多。
（a）首先，写出对应于二进制数描述的类型bin的归纳定义。
天真的定义并不完全有效，因为你最终能够构造一个术语，这个术语将已经添加了1的数字加1或者没有任何理由将零乘以2。为了避免那些我认为我会编码某种状态转换到构造函数中以避免这些，但这有点棘手所以这是我能想到的最好的
Inductive tag : Type := z | nz | m. (* zero | nonzero | multiply by 2 *)
Inductive bin_nat : tag -> Type :=
(* zero *)
| Zero : bin_nat z
(* nonzero *)
| One : bin_nat nz
(* multiply by 2 -> nonzero *)
| PlusOne : bin_nat m -> bin_nat nz
(* nonzero | multiply by 2 -> multiply by 2 *)
| Multiply : forall {t : tag}, (t = m \/ t = nz) -> bin_nat t -> bin_nat m.
通过上面的表示，我避免了没有意义的术语问题，但现在每当我乘以2时我都要随身携带证据。我实际上不知道如何在递归函数中使用这些东西。
我知道如何构建证明和术语，它们看起来像这样
(* nonzero *)
Definition binr (t : tag) := or_intror (t = m) (eq_refl nz).
(* multiply by 2 *)
Definition binl (t : tag) := or_introl (t = nz) (eq_refl tag m).
(* some terms *)
Check Zero.
Check One.
Check (Multiply (binr _) One).
Check (Multiply (binl _) (Multiply (binr _) One)).
Check PlusOne (Multiply (binl _) (Multiply (binr _) One)).
我还可以写下我想要对应一个函数的定理的“证明”，但我不知道如何将它实际转换为函数。这是转换功能的证明
Definition binary_to_nat : forall t : tag, bin_nat t -> nat.
Proof.
intros.
einduction H as [ | | b | t proof b ].
{ exact 0. } (* Zero *)
{ exact 1. } (* One *)
{ exact (S (IHb b)). } (* PlusOne *)
{ (* Multiply *)
edestruct t.
cut False.
intros F.
case F.
case proof.
intros F.
inversion F.
intros F.
inversion F.
exact (2 * (IHb b)).
exact (2 * (IHb b)).
}
Defined.
我知道这个术语是我想要的功能，因为我可以在用它计算时验证我得到了正确的答案
Section Examples.
Example a : binary_to_nat z Zero = 0.
Proof.
lazy.
trivial.
Qed.
Example b : binary_to_nat nz One = 1.
Proof.
lazy.
trivial.
Qed.
Example c : binary_to_nat m ((Multiply (binl _) (Multiply (binr _) One))) = 4.
Proof.
lazy.
trivial.
Qed.
End Examples.
最后问题是，是否有一种简单的方法可以将上述证明术语转换为实际函数，或者我是否必须尝试对证明术语进行逆向工程？
我喜欢你使用状态和索引归纳类型表示有效二进制数的想法。然而，正如问题所表明的那样，在归纳类型上只有三个构造函数可以逃脱：零，乘以2，乘以2并加一。这意味着我们需要避免的唯一转变是将零乘以2。
Inductive tag : Type := z | nz. (* zero | nonzero *)
Inductive bin_nat : tag -> Type :=
(* zero *)
| Zero : bin_nat z
(* multiply by 2 *)
| TimesTwo : bin_nat nz -> bin_nat nz
(* multiply by 2 and add one *)
| TimesTwoPlusOne : forall {t : tag}, bin_nat t -> bin_nat nz.
然后，例如，
Let One := TimesTwoPlusOne Zero. (* 1 *)
Let Two := TimesTwo One. (* 10 *)
Let Three := TimesTwoPlusOne One. (* 11 *)
Let Four := TimesTwo Two. (* 100 *)
所以TimesTwo在二进制表示的末尾添加零，TimesTwoPlusOne添加一个。
如果你想自己尝试一下，不要再看了。
（我会把它放在剧透标签中，但显然扰流标签中的代码块很小）
增加二进制数。
Fixpoint bin_incr {t: tag} (n: bin_nat t): bin_nat nz :=
match n with
| Zero => One
| TimesTwo n' => TimesTwoPlusOne n'
| @TimesTwoPlusOne _ n' => TimesTwo (bin_incr n')
end.
用于将nat转换为二进制的辅助定义。
Definition nat_tag (n: nat): tag :=
match n with
| 0 => z
| S _ => nz
end.
将nat转换为二进制。
Fixpoint nat_to_bin (n: nat): bin_nat (nat_tag n) :=
match n with
| 0 => Zero
| S n' => bin_incr (nat_to_bin n')
end.
将二进制转换为nat。请注意，这使用符号进行乘法和自然数的加法。如果这不起作用，您可能没有打开正确的范围。
Fixpoint bin_to_nat {t: tag} (n: bin_nat t): nat :=
match n with
| Zero => 0
| TimesTwo n' => 2 * (bin_to_nat n')
| @TimesTwoPlusOne _ n' => 1 + 2 * (bin_to_nat n')
end.
我们从这些定义中得到实际函数（注意20是二进制的10100）。
Compute nat_to_bin 20.
= TimesTwo
(TimesTwo (TimesTwoPlusOne (TimesTwo (TimesTwoPlusOne Zero))))
: bin_nat (nat_tag 20)
Compute bin_to_nat (nat_to_bin 20).
= 20
: nat
另一个技术说明。我在两个版本的Coq（8.6和8.9 + alpha）上使用了这个代码，并且一个版本要求我在TimesTwoPlusOne上匹配时明确地放置标签，而另一个版本允许它保持隐含。上述代码应该适用于任何一种情况。