如何证明nat_to_bin结合了bin_to_nat b = Coq中标准化b

Question

我是新手学习Coq，参考书软件基础入门

在这句话的最后部分，有一个关于证明这一点的练习

将二进制转为自然数再转回二进制与其本身等价。

这是最后一个定理 bin_nat_bin

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with 
  | Z => 0
  | B0 (m') => 2 * bin_to_nat(m')
  | B1 (m') => S (2 * bin_to_nat(m')) 
  end.

Fixpoint nat_to_bin (n:nat) : bin :=
  match n with
  | 0 => Z
  | S n' => incr (nat_to_bin n')
  end.

Fixpoint normalize (b:bin) : bin :=
  match b with
  | Z => Z
  | B0 b' =>
    match (normalize b') with
    | Z => Z
    | b'' => B0 b''
    end
  | B1 b' => B1 (normalize b')
  end.

Theorem bin_nat_bin : forall b : bin, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
    (* FILL IN HERE *) Admitted.

起初，我尝试如下归纳b。

Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  intros b. induction b as [|b'|b''].
  - simpl. reflexivity. 
  - simpl. rewrite add_0_r. simpl.

并获得这些

1 goal
b' : bin
IHb' : nat_to_bin (bin_to_nat b') = normalize b'
______________________________________(1/1)
nat_to_bin (bin_to_nat b' + bin_to_nat b') =
match normalize b' with
| Z => Z
| B0 n => B0 (B0 n)
| B1 n => B0 (B1 n)
end

我想知道如何证明这个子目标，

如果我需要将 bin_to_nat b' 之间的 '+' 更改为构造函数 double_bin

Definition double_bin (b:bin) : bin :=
  match b with
  | Z => Z
  | m => B0 (m)
  end.

并弥合它们之间的差距（我不清楚如何做到这一点。请给我一些提示）

或者按照提示去做

提示：首先尝试证明主要陈述，看看你在哪里陷入困境，并看看是否可以找到一个引理 - 也许需要它自己的归纳证明 - 这将使主要证明取得进展。我们有一个引理用于 B0 情况（也使用 double_incr_bin），另一个引理用于 B1 情况。

您能给我一些更详细或更实用的措施或提示吗？

谢谢你。

Answer 1

最好用

normalize

和

double_bin

来定义

incr

。然后我们可以认为在从自然数转换为二进制时该属性是成立的，例如

forall m , nat_to_bin (m + m) = double_bin (nat_to_bin m).