如何完成Coq中二进制数归一化函数normalize的幂等性证明

首先给出你定义的二进制类型和归一化函数：

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

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

证明思路 #

你卡住的是归纳证明中B0 b'的分支，不需要拆解b'，直接对normalize b'的结果做分类讨论，再结合归纳假设即可完成证明。
完整的证明脚本如下：

Theorem normalize_idemp :
  forall b: bin, normalize b = normalize (normalize b).
Proof.
  induction b as [| b' IHb' | c' IHc'].
  - (* 情况1：b = Z *)
    simpl. reflexivity.
  - (* 情况2：b = B0 b' *)
    simpl.
    (* 对normalize b'的结果做case分析 *)
    destruct (normalize b') eqn:E.
    + (* 子情况1：normalize b' = Z *)
      simpl. reflexivity.
    + (* 子情况2：normalize b' = B0 b0 *)
      simpl. rewrite <- IHb'. rewrite E. reflexivity.
    + (* 子情况3：normalize b' = B1 b1 *)
      simpl. rewrite <- IHb'. rewrite E. reflexivity.
  - (* 情况3：b = B1 c' *)
    simpl. rewrite IHc'. reflexivity.
Qed.

关键步骤说明 #

• 当处理B0 b'分支时，simpl后目标会出现对normalize b'的模式匹配，此时用destruct (normalize b')可以直接拆分所有可能的返回结果，避免无意义地递归拆解b'的结构。
• 拆分后每个子目标都可以直接用归纳假设IHb' : normalize b' = normalize (normalize b')做重写，结合destruct生成的等式E即可完成验证。

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