1

“软件基础”中有一个练习，我一直在尝试正确解决一段时间，但实际上我在尝试写下所要求的功能方面遇到了困难。这是练习的相关部分

考虑使用二进制而不是一元系统的自然数的不同、更有效的表示。也就是说，与其说每个自然数要么是零要么是自然数的后继，我们可以说每个二进制数要么是

  • 零，
  • 二进制数的两倍，或
  • 一个二进制数的两倍多。

(a) 首先，写出对应于二进制数描述的类型 bin 的归纳定义。

幼稚的定义不太适用，因为您最终能够构建将 1 加到已经加了 1 的数字或无缘无故地将 0 乘以 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.

所以最后的问题是，有没有一种简单的方法可以以简单的方式将上述证明项转换为实际函数，还是我必须尝试对证明项进行逆向工程？

4

1 回答 1

3

我喜欢您使用状态和索引归纳类型表示有效二进制数的想法。然而，正如问题所表明的那样，在归纳类型上只使用三个构造函数是可能的：零、乘以 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，而另一个版本允许它保持隐式。上面的代码在任何一种情况下都应该有效。

于 2018-12-15T04:17:23.267 回答