h_chiro https://blog.hatena.ne.jp/h_chiro/ 雑記 https://h-chiro.hatenablog.com/ Coq 最近全然Coqを触ってなかったので、久々にやってみました。示さないといけないのは、0からnまでの和の2倍が n * (n + 1)に等しいっていうやつで、まぁ何も考えずにnについて帰納法で示せばよいです。ただ、autoとかringとかomegaとかを使うとなぜか負けた気分になるので、使わずに地道に頑張りました。golfしないといけないのに、全くgolfしてない・・・ 後半の方は、a + b + c + d = c + b + a + dみたいな等式を書き換えしてるだけなので、もうちょっと縮むかもしれないですね。 Require Import Definitions. Require Impor… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fh-chiro.hatenablog.com%2Fentry%2F20110709%2F1310229080" title=" Anarchy Proof - Sum of Natural Numbers - 雑記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-07-09 01:31:20 rich https://h-chiro.hatenablog.com/entry/20110709/1310229080 1.0 100%