h_chiro https://blog.hatena.ne.jp/h_chiro/ 雑記 https://h-chiro.hatenablog.com/ Coq テスト前なので、逃避にCoPL(http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi)やら、Anarchy Proofやらばっかりやってます。今回の問題は、いわゆる鳩ノ巣原理ですね。 自然数のリストxsがあって、length xs xsについて帰納法+ xsがnilでないなら先頭の要素が0か1かそれ以上で場合わけしました。 例によって、autoとか使ってないので、長い……あと、手元(Coq8.3だったかな?)にはlt_z_Snに相当する命題がlt_0_Snっていう名前であるんですけど、サブミットするとそんな命題ねーよって言われた… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fh-chiro.hatenablog.com%2Fentry%2F20110722%2F1311357156" title=" Anarchy Proof - PHP - 雑記" 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-22 02:52:36 rich https://h-chiro.hatenablog.com/entry/20110722/1311357156 1.0 100%