ずっとtrunkのemacsを自分でビルドして使ってるわけなんですが、ProofGeneralを使おうとして、byte-compileしようとするとこけます。 で、エラーメッセージを読むと interactive-p を使うな、 called-interactively-p を使えとあるので (interactive-p)を探…

テスト前なので、逃避にCoPL(http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi)やら、Anarchy Proofやらばっかりやってます。今回の問題は、いわゆる鳩ノ巣原理ですね。 自然数のリストxsがあって、length xs xsについて帰納法+ xsがnilでない…

最近全然Coqを触ってなかったので、久々にやってみました。示さないといけないのは、0からnまでの和の2倍が n * (n + 1)に等しいっていうやつで、まぁ何も考えずにnについて帰納法で示せばよいです。ただ、autoとかringとかomegaとかを使うとなぜか負けた気…