Coq中如何证明nat_to_bin(bin_to_nat b) = normalize b？

核心思路：用辅助引理衔接自然数与二进制的翻倍逻辑 #

你当前的卡点在于自然数加法（bin_to_nat b' + bin_to_nat b'）和二进制数的翻倍操作之间的对应关系，直接处理会非常繁琐。定义double_bin并配套证明辅助引理是更清晰的路径，以下是具体步骤：

步骤1：定义double_bin并证明兼容性引理 #

你提出的double_bin定义完全合理，它对应二进制数的左移翻倍操作。先证明两个关键引理：

引理1：double_bin与bin_to_nat的数值对应

Lemma double_bin_to_nat : forall b, bin_to_nat (double_bin b) = 2 * bin_to_nat b.
Proof.
  intros b. destruct b as [|b'|b''].
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

引理2：自然数翻倍转二进制等价于二进制数翻倍

这是衔接当前子目标的核心：

Lemma nat_to_bin_double : forall n, nat_to_bin (n + n) = double_bin (nat_to_bin n).
Proof.
  intros n. induction n as [|n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite IHn'.
    (* 这里需要依赖`incr`的基础性质，先补全以下引理 *)
    assert (incr_B0 : forall b, incr (B0 b) = B1 b).
    { intros b. simpl. reflexivity. }
    assert (incr_B1 : forall b, incr (B1 b) = B0 (incr b)).
    { intros b. simpl. reflexivity. }
    rewrite incr_B0. reflexivity.
Qed.

步骤2：利用引理推进原定理证明 #

回到原定理的归纳步骤，分情况处理：

Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  intros b. induction b as [|b'|b''].
  - (* 处理Z的情况 *)
    simpl. reflexivity. 
  - (* 处理B0 b'的情况 *)
    simpl. rewrite add_0_r. simpl.
    rewrite IHb'.
    (* 对normalize的结果分情况讨论 *)
    destruct (normalize b') as [|n|n].
    + simpl. reflexivity.
    + rewrite nat_to_bin_double. simpl. reflexivity.
    + rewrite nat_to_bin_double. simpl. reflexivity.
  - (* 处理B1 b''的情况 *)
    simpl. rewrite <- nat_to_bin_incr. (* 该引理由nat_to_bin定义直接可得：nat_to_bin (S n) = incr (nat_to_bin n) *)
    rewrite IHb''.
    (* 结合normalize的定义，B1的规范化结果是B1 (normalize b'') *)
    simpl. reflexivity.
Qed.

备选思路：直接对normalize b'分情况处理 #

如果不想定义double_bin，也可以在当前子目标直接对normalize b'做destruct：

• 当normalize b' = Z时，左右两边都是Z，直接reflexivity。
• 当normalize b' = B0 n时，需要证明nat_to_bin (4 * bin_to_nat n) = B0 (B0 n)，可通过嵌套归纳证明。
• 当normalize b' = B1 n时，需要证明nat_to_bin (2 * S (2 * bin_to_nat n)) = B0 (B1 n)，同样依赖nat_to_bin的翻倍性质。

但这种方法会重复编写翻倍逻辑，不如定义double_bin后通过引理统一处理高效。

内容的提问来源于stack exchange，提问作者luxuriant_lettuce