教育のためにテスト問題を作成していると、正解にしても誤答にしても選択肢が「間違いなく(正解|誤答)といえるか」というのが重要問題になる。ここはCoq+OCamlで作問支援して、楽しい作問ライフを過ごしたいところ。
「Coq/SSReflect/MathCompによる定理証明」が積読状態だったのだが、力を発揮してくれる予感がする。
モーダスポーネンスとヒルベルトの公理S
From mathcomp
Require Import ssreflect.
Section ModusPonens.
Variables X Y : Prop.
Hypothesis XtoY_is_true : X -> Y.
Hypothesis X_is_true : X.
Theorem MP : Y.
Proof.
move : X_is_true.
by [].
Qed.
End ModusPonens.
Section HilbertSAxiom.
Variables A B C : Prop.
Theorem HS1 : (A -> (B -> C)) -> ((A -> B) -> (A -> C)).
Proof.
move=> AtoBtoC_is_true.
move=> AtoB_is_true.
move=> A_is_true.
apply: (MP B C).
apply: (MP A (B -> C)).
by [].
by [].
apply: (MP A B).
by [].
by [].
Qed.
End HilbertSAxiom.
これ見ただけで「間違いないですね」と言えるようになるのだろうか。
CoqIDEで動きを確認しないと、何言ってるのか分からない。
とはいえ、いったん意味が分かるとあとは「パズルゲーム」になる。
OCaml,Coq,CoqIDE,MathCompは、opamでどかどかインストールした。
いちいちコンパイルしながらインストールしていくので、かなり時間がかかる。