证明匹配语句

Question

为了解决一个练习，我有以下表示整数的定义：

Inductive bin : Type :=
| Zero : bin
| Twice : bin -> bin
| TwiceOne : bin -> bin.

这个想法是：

1. x 是 2*x 的两倍。
2. TwiceOne x 是 2*x +1。

但是，这种表示有一个问题：数字0有几种表示。

因此，我需要实现一个函数来规范化bin 中写入的数字。

为此，我声明了以下函数：

Fixpoint normalize_bin (b:bin) : bin :=
  match b with
    | Zero => Zero
    | TwiceOne x => TwiceOne (normalize_bin x)
    | Twice x => match normalize_bin x with
                   | Zero => Zero
                   | x => Twice x
                 end
  end.

现在，我想表明，如果一个 b 类型为 bin，我将 b 翻译成 nat 然后我回到 bin 我得到 b'，即标准化b。这是以下定理：

Theorem bin_to_nat_to_bin : forall (b:bin),
                              nat_to_bin (bin_to_nat b) = normalize_bin2 b.

为了证明这个定理，我对b 进行了归纳。但我被困在行业里了

ctive case，因为我需要证明：

   nat_to_bin (bin_to_nat Tb + bin_to_nat Tb) =
   match normalize_bin2 Tb with
   | Zero => Zero
   | Twice b => Twice (Twice b)
   | TwiceOne b => Twice (TwiceOne b)
   end

使用战术simpl之后。

但是，我不知道如何处理目标中的这场比赛。我可以从这里做什么？

由于这个练习来自一本书，我不必使用 Coq 的一些高级东西。我只知道一些战术，比如reflexivity、simpl、rewrite、destruct、assert。

可能的第二个规范化只是声明这一点：

Definition normalize_bin (b:bin) : bin :=
  nat_to_bin (bin_to_nat b).

但在这种情况下，这是微不足道的，我认为这不是预期的答案。

Answer 1

由于这是来自 Software Foundations 的一个练习，我不会给出完整的答案，而是给出一个提示。

这个证明确实很棘手。当您遇到这样一个复杂的证明时，尝试将其分解为较小的引理通常是个好主意。这反过来可能需要重新组织您的定义，以便这些引理的陈述变得更简单。

在您的情况下，您对normalize_bin 的定义有一个内部match，看起来有点过于复杂，一旦您进入证明的这一点，这一点就会变得很明显。您能否将内部 match 分解为一个单独的定义，以便您可以陈述有关该定义的引理并在稍后的主要证明中使用这些引理？