第102回 ProofCafe

Coq

イベント内容

萩原、アフェルト 著 「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 も合成数であることを証明してください。

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

以上

注意事項

※ こちらのイベント情報は、外部サイトから取得した情報を掲載しています。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。