Coq中norm_bin_B0_out定理证明求助：带排除前置条件的destruct使用

最近在学习《Software Foundations》归纳章节的五星进阶习题（binary_inverse的c部分）时，不少人会卡在norm_bin_B0_out定理的证明上，先还原一下问题背景：

定义与待证定理 #

首先我们有二进制数的归纳定义和规范化函数：

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

Fixpoint norm_bin (input :bin): bin := 
  match input with 
  | Z => Z 
  | B0 Z => Z 
  | B1 restInput => B1 (norm_bin restInput) 
  | B0 restInput=> 
      match norm_bin restInput with 
      | Z => Z 
      | _ => B0 (norm_bin restInput) 
      end 
  end.

需要证明的定理是：

Theorem norm_bin_B0_out : forall b, norm_bin b <> Z -> norm_bin (B0 b) = B0 (norm_bin b).

最初的困境 #

一开始尝试对b进行destruct时，会遇到b = Z的情况，但此时norm_bin Z = Z，和前置条件norm_bin b <> Z矛盾，却不知道怎么高效处理这个分支，导致证明卡壳。

核心解决思路 #

问题的关键在于不要直接对b做归纳或case分析，而是对norm_bin b的结果进行case分析。因为前置条件已经明确norm_bin b <> Z，我们可以通过destruct norm_bin eqn:f来枚举norm_bin b的所有可能形态，直接排除掉norm_bin b = Z的矛盾情况，剩下的合法形态再对应处理即可。

完整证明代码 #

最终的证明过程如下：

Theorem norm_bin_B0_out : forall b, norm_bin b <> Z -> norm_bin (B0 b) = B0 (norm_bin b).
Proof.
  intros b H. simpl.
  destruct norm_bin eqn:f.
  - simpl in H. tauto. (* 排除norm_bin b = Z的矛盾情况 *)
  - simpl. destruct b. { discriminate. } { reflexivity. } { reflexivity. }
  - destruct b. { discriminate. } { reflexivity. } { reflexivity. }
Qed.

简单解释每一步：

1. intros b H：引入全称量词变量b和前置条件H；
2. simpl：展开norm_bin (B0 b)的定义；
3. destruct norm_bin eqn:f：对norm_bin b的结果做case分析，生成三个分支（Z、B0 n、B1 n）；
4. 第一个分支中，H变为Z <> Z，用tauto自动处理矛盾；
5. 剩下的两个分支里，norm_bin b是规范化后的非零二进制数，此时对b做case分析后，所有合法情况都可以通过reflexivity直接验证等式成立，矛盾情况用discriminate排除。

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