Coq destruct 带有排除的前提条件

Question

我正在使用 softwarefoundations book 学习 Coq，但在 induction chapter 中的最后一个任务上卡住了 - 练习：5 星，高级 (binary_inverse) 部分 c。

鉴于下一个定义。

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).

我试过destruct b，但是不能解决b = Z的情况，根据条件norm_bin b <> Z，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.
  - simpl. destruct b.
    { discriminate. }
    { reflexivity. }
    { reflexivity. }
  - destruct b.
    { discriminate. }
    { reflexivity. }
    { reflexivity. }
Qed.

我不知道 norm_bin 可以被破坏。那是个问题。

Answer 1

当你有一个否定的假设H（例如~A），但你知道你可以证明否定的公式（你可以证明A），那么执行的好步骤是@987654324 @，这导致你必须证明A的目标。

在检查了这不是 SF 书中的练习之后，我决定再帮助你一些。

norm_bin (B0 b) 语句中的公式符合simpl 策略的符号执行计算条件。这样做。

在这一步之后，您会看到一个包含 2 个匹配语句的表达式。其中一个是b 上的匹配语句，另一个是norm_bin b 上的匹配语句。然后，您的下一步可以是b 上的destruct，但也可以是norm_bin 上的destruct。尝试两条路线，但如果您选择后者，请使用eqn: destruct 策略的变体。

如果您希望下一步是对b 进行破坏，那么问题是您会得到一个将norm_bin 应用于(B0 (B0 ...) 的表达式。使用此公式在目标上使用 simpl 会导致计算量过多。您需要通过使用 change 而不是 simpl 来驯服这一点，并为自己编写您认为最能满足您需求的中间计算。