第102回 ProofCafe

イベント内容

萩原、アフェルト 著 「Coq/SSReflect/MathCompによる定理証明」森北出版　の4章を読んでいきます。

4.6 bigop.v

参加をご希望のかたは、管理者までお問い合わせください。

---

Coq/MathComp をセットアップしたのち、

https://github.com/suharahiromichi/coq/blob/master/csm/csm_4_6_bigop.v

をダウンロードしておいてください。 資料は改訂していますから、申し訳ありまあせんが、開始直前に再度ダウンロードしなおしてください。

また、https://github.com/suharahiromichi/coq/blob/master/common/ssromega.v　もダウンロードして同じディレクトリに置き coqc ssromega.v を実行して、ssromega.vo ができていることを確認してください。

---

問題 1.

任意のnについて、以下が成り立つことを証明してください。

2 * (\sum_(0 <= x < n.+1) x) = n * n.+1

6 * (\sum_(0 <= x < n.+1) x^2) = n * n.+1 * n.*2.+1

問題 2.

自然数 n が合成数なら、2^n - 1 も合成数であることを証明してください。

解答は説明のなかでおこないます。

以上

注意事項