证明比赛声明 [英] Prove a match statement

问题描述

尝试解决一个练习，我具有以下表示整数的定义:

Trying to solve an exercise, I have the following definition that represents the integers :

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

这个想法是:

1. 两次 x 是 2 * x .
2. TwiceOne x 是 2 * x +1 .

但是，这种表示形式存在问题:数字 0 有几种表示形式.

However, this representation has a problem: there are several representations of the number 0.

因此，我需要实现一个函数，以标准化在 bin 中写入的数字.

Therefore, I need to implement a function that normalize a number writing in bin.

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

To do this I have declared the following function :

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.

现在，我想表明，如果采用类型为 bin 的 b ，我会在 nat <中翻译 b /code>，然后回到 bin ，我得到b'，它是 b 的归一化形式.这是以下定理:

And now, I want to show that if a take a b of type bin, I translate b in nat and then I come back to bin I get the b' that is the normalized of b. This is the following theorem :

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

为了证明这个定理，我对 b 进行了归纳.但是我陷入了行业

To prove this theorem I do an induction on b. But I am getting stuck in the indu

案例，因为我需要证明:

ctive case since I need to show that:

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

但是，我不知道该如何应对这场比赛.我可以从这里做什么?

However, I have no idea how to deal with this match in the goal. What can I do from here ?

由于本练习来自一本书，因此我不必使用Coq的一些高级知识.我只知道一些策略，例如 reflexivity ， simpl ， rewrite ， destruct ， assert

Since this exercise come from a book, I don't have to use some advanced things of Coq. I just know some tactics like reflexivity, simpl, rewrite, destruct, assert.

第二种规范化可能只是声明这一点:

A second normalization possible is just to declare this :

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

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

But in this case it is trivial and I don't think that is the answer expected.

推荐答案

由于这是Software Foundations的练习，因此我不会给出完整的答案，但会给出提示.

Since this is an exercise from Software Foundations, I won't give the full answer, but a hint.

这个证据确实很棘手.当您遇到类似这样的复杂证明时，通常最好将其分解为较小的引理.反过来，这可能需要重新组织定义，以使这些引理的陈述变得更简单.

This proof is indeed quite tricky. When you get in the middle of a complicated proof like this, it's usually a good idea to try to factor it into smaller lemmas. This in turn might require reorganizing your definitions so that the statements of these lemmas become simpler.

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

In your case, your definition of normalize_bin has an inner match that looks a bit too complicated, which becomes apparent once you get into that point of your proof. Can you factor that inner match in a separate definition so that you can state lemmas about that definition and use those lemmas later in your main proof?

这篇关于证明比赛声明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！