古典論理の定理であるパースの法則（パース則）です．こんなのが証明できるなんて古典論理は(ryちなみに，二重否定除去を公理とした古典論理の証明の練習として Domino On Acid なんてのがあります．暇な人は遊んでみて下さい．*1今回は Classical モジュー…

Anarchy Proof 二題目です．矛盾からはなんでも証明できるというやつです．矛盾に対応する False は，何も規則がひとつもない inductive type として定義されています．なので，H: False という仮定があれば，inversion H するだけでなんでも証明できてしま…

McCarthy の91関数を Coq で定義しようとすると，簡単にはできないことがわかります．具体的には， structural な recursion になっていない． measure がわかったとしても，nested な recursion は Fixpoint や Function で扱えない． こんなときは以前も話…

11ヶ月ぶりの更新です．Anarchy Proof に手を出してみました．Project Euler と違って，問題の定義が Coq の形式で与えられているので非常に楽です． # 当たり前方針としては，ゴルフは全くせずに他人が読んでもわかる(かもしれない)書き方をするつもりです…