私は学校で Coq を学んでいて、家でやるべき課題があります。証明すべきレンマがあります。リストの要素にゼロが含まれている場合、その要素の積は 0 です。コードを開始しましたが、先に進む方法がわからない点で立ち往生しています。Coq からのすべてのコマンドを知っているわけではありません。多くの調査を行いましたが、Proof の最後までたどり着くことができません。ここに私のコードがあります: 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.
それで、リストにゼロが含まれているかどうかをチェックする関数と、その要素の積を計算する別の関数を作成するのは良い考えだと思いました。また、(幸運にも) 2 つの数字があり、そのうちの 1 つが 0 ではなく、その積が 0 である場合、必然的にもう 1 つの数字が 0 であることを証明する補題をオンラインで見つけました (それが役立つと思いました)。 . 帰納法で証明しようと思ったのですが、うまくいきませんでした。何か案は？私は、ここが誰かに私の仕事を依頼する場所ではないことを知っています。