━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
証明支援システム Coq で学ぶ証明法
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
証明支援システムでは，数学的な主張やその証明を専用の言語で書くと，
証明の誤りを自動検出できる．「数理論理学」の講義で扱った証明を
証明支援システム Coq 用に記述した例を紹介する．
●自然演繹による証明 (述語論理)
証明支援システム Coq の核となる形式体系は，自然演繹に深い関連をもつため，
自然演繹の証明の学習にも Coq を使える．
簡単な例として，『はじめての数理論理学』 p.5 の自然演繹による証明を取り上げる．
この証明に対応する Coq 記述の例を以下に示す．
------------------------------------------------------------
Require Import Utf8.
Parameter (U : Type) (P Q : U→Prop).
Theorem natural_deduction :
(∃x, (P x ∧ ¬ Q x)) → ¬ (∀x, (P x → Q x)).
Proof.
intro H1. (* →I *)
intro H2. (* →I *)
elim H1; intros a H3. (* ∃E *)
pose (C1 := proj1 H3). (* ∧E1 *)
pose (C2 := H2 a). (* ∀E *)
pose (C3 := C2 C1). (* →E *)
pose (C4 := proj2 H3). (* ∧E2 *)
pose (C5 := C4 C3). (* →E *)
exact C5.
Qed.
------------------------------------------------------------
証明を構成するための命令を Proof. と Qed. の間に書く．
対応する自然演繹の規則名を (* *) 内の注釈に示した．
推論規則の適用により，仮定 (hypotheses) H1〜H3 を設けたり，
結論 (conclusions) C1〜C5 を導いたりしている．
この記述を開発環境 CoqIDE で対話的に作成・検証する様子を次の図に示す．
画面左が命題や証明の記述，画面右上が規則適用で得られた仮定や結論の論理式である．
冒頭に示した証明図と対応させると，証明図の下から3段積み上げて仮定を三つ設けて
(7〜9行目)，仮定から矛盾を導いた(10〜14行目)結果が表示されていることが分かる．
使った規則だけを示して途中結果を省くことで，簡潔な証明も書ける．
------------------------------------------------------------
Theorem natural_deduction_simple {U} (P Q : U->Prop) :
(exists x, (P x /\ ~ Q x)) -> ~ (forall x, (P x -> Q x)).
Proof.
intros H1 H2. elim H1. intros a [H3P H3Q].
elim H3Q. apply H2. exact H3P.
Qed.
------------------------------------------------------------
命題の証明が簡単なら，自動証明の機能を使って正しさを確認できる．
上記の命題の場合，Proof. と Qed. の間に firstorder. と書くと自動証明できる．
ここに載せたコードや以下の資料を参考に証明支援システムを実際に動かして，
体験しながら証明について深く学んでほしい．数理論理学の確認問題を Coq 用に
記述するのもよい練習になる．
●参考資料
＊Webサイト
・The ROCQ Proof Assistant (ROCQ は Coq の新名称)
https://rocq-prover.org/
・jsCoq (Coq のオンライン環境)
https://coq.vercel.app/
https://coq.vercel.app/scratchpad.html
・The ROCQ Reference Manual (ROCQ は Coq の新名称)
https://rocq-prover.org/refman/
＊文献
・"Interactive Theorem Proving and Program Development",
Y. Bertot and P. Casteran, Springer 2004.
https://www.springer.com/jp/book/9783540208549
・『Coq/SSReflect/MathComp による定理証明』，
萩原学，アフェルト・レナルド，森北出版，2018．
https://www.morikita.co.jp/books/book/3287
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
授業のホームページ
山田 俊行
https://www.cs.info.mie-u.ac.jp/~toshi/