1

我在学校学习 Coq，我有一个家庭作业要做。我有一个引理需要证明：如果一个列表在其元素中包含零，则其元素的乘积为 0。我开始编写代码，但我陷入了不知道如何继续下去的地步。我不知道 Coq 的所有命令，我做了很多研究，但我无法找到通往证明结尾的路。这是我的代码：需要导入列表 ZArith。

Open Scope Z_scope.

Fixpoint contains_zero (l : list Z) :=
  match l with
    nil => false
  | a::tl => if Zeq_bool a 0 then true else contains_zero tl
  end.

Fixpoint product (l : list Z) :=
  match l with
    nil => 1
  | a::tl => a * product tl
  end.

Lemma Zmult_integral_r :
  forall n m, m <> 0 -> m * n = 0 -> n = 0.
Proof.
intros n m m0; rewrite Zmult_comm; apply Zmult_integral_l.
assumption.
Qed.

Lemma product_contains_zero :
  forall l, contains_zero l = true -> product l = 0.
intros l H.

所以，我认为创建一个函数来检查列表是否包含零，以及另一个来计算其元素的乘积是一个好主意。我还（幸运的是）在网上找到了一个引理，证明如果我有 2 个数字，并且我知道其中一个不是 0，并且它们的乘积是 0，那么另一个数字必然是 0（我认为这可能会有所帮助） . 我想过用归纳法做一个证明，但没有成功。有任何想法吗？我知道这不是让别人做我的工作的地方，我不是在问那个，我只是需要一个想法。

4

2 回答 2

3

1 /您不需要您提到的定理，“如果我有2个数字，并且我知道其中一个不是0，并且它们的乘积是0，那么另一个数字一定是0”。您不需要它，因为您想证明乘积为 0，您不处于想要使用乘积为零的事实的情况。

所以定理 Zmult_integral_r 对这个问题的引理没有用处。如果您必须证明 forall l, product l = 0 -> contains_zero l = true，这将很有用。

在这里，对于您的问题，您考虑的两个函数是递归的，因此通常的提示是通过归纳进行证明，然后使用策略 simpl 使函数看起来更简单。

于 2012-12-05T19:07:25.653 回答
0

将两个数字的乘积表示为一个数字，而您将支持该引理。

于 2012-12-05T18:51:41.260 回答