Call-by-name版なので簡単ですけど。ものすごく下手なソースだと思いますが、一応晒しておきます。

離散数学の授業で定理証明器のことをちょっと触れたいと思って、証明の例題に使っている上記命題をCoqで証明してみました。多分いろいろ上手くないと思うのだけれどもさらしてみます。 Require Import Classical. Require Import Arith. Require Import Omeg…

ProofWeb知らなかった。CoqとかIsabelleとかのような定理証明器をウェブ上で動かせます。インストールがいらないのでちょっと遊んでみるのに便利ですね。まあ、操作性では劣りますが。