Proving a theorem using induction in COQ

Question

I am learning Coq at school, and I have an assignment to do for home. I have a lemma to proove: If a list contains a zero among its elements, then the product of its elements is 0. I started my code, and I am stuck in a point where I do not know how to go on. I do not know all the commands from Coq, I did a lot of research, but I cannot manage to find my way to the end of the Proof. Here is my code: Require Import List 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.

So, I thought that it would be a good idea to create a function that checks if the list contains a zero, and another one to calculate the product of its elements. I have also found (luckily) a lemma online that prooves that if I have 2 numbers , and I know that one of them is not 0, and their product is 0, then necessarily the other number is 0 (I thought that might help). I thought about doing a proof by induction, but that didn't work out. Any ideas? I know that this is not the place to ask someone to do my work , I AM NOT ASKING THAT, I just need an idea.

Yves Yves · Accepted Answer · 2012-12-05T19:07:25

1/ You do not need the theorem that you mention, " if I have 2 numbers , and I know that one of them is not 0, and their product is 0, then necessarily the other number is 0". You don't need it because you want to prove that the product is 0, you are not in a situation where you want to use the fact that the product is zero.

So the theorem Zmult_integral_r is not useful for the lemma in this question. It would be useful if you had to prove forall l, product l = 0 -> contains_zero l = true.

Here, for your problem, the two functions that you consider are recursive, so the usual hint is to do a proof by induction, and then to use the tactic simpl to make the functions look simpler.

Proving a theorem using induction in COQ

2 Answers