はじめに
Retail AI Adventurers Advent Calendar 2023の19日目の投稿です。
昨日は@urakawa_jinseiさんのAirで始めるGo開発でした。
この記事のゴール
- Coq と呼ばれる証明支援器を試してみる記事です。
- 与えられた命題に対して、手作業で得られた証明とCoqの操作により得られた証明が論理的に一致していることを確認してみます。
環境構築
- Mac ユーザの方を対象にしています。
本記事で使用する命題
\forall P ((P \Rightarrow Q) \Rightarrow Q) \Rightarrow ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P
証明 | without Coq
（注意）本記事では証明の詳細には立ち入りませんので、証明を詳しく追いたい方は1を参照してください。
-
変形1
- givens
\forall P ((P \Rightarrow Q) \Rightarrow Q)- goal
((P \Rightarrow Q) \Rightarrow P) \Rightarrow P -
変形2
- givens
\forall P ((P \Rightarrow Q) \Rightarrow Q)(P \Rightarrow Q) \Rightarrow P- goal
P -
変形3(modus ponens を適用)
- givens
\forall P ((P \Rightarrow Q) \Rightarrow Q)(P \Rightarrow Q) \Rightarrow P- goal
P \Rightarrow Q -
変形4
- givens
\forall P ((P \Rightarrow Q) \Rightarrow Q)(P \Rightarrow Q) \Rightarrow PP- goal
Q -
変形4 において、givens の1行目から goal が得られるので証明終。
証明 | with Coq
（注意）本記事では Coq の使用方法の詳細には立ち入りませんので、使用方法を詳しく追いたい方は2を参照してください。
以下のコードを実行します（Coq の拡張子は .v らしいです）。
introduction.v
Goal forall (P Q: Prop), (forall P: Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.
Proof.
intros.
apply H0.
intro. (* <- ここまで実行します*)
(*
apply (H(P->Q)).
apply (H P).
Qed.
*)
以下の結果が得られました。
result
1 subgoal
P, Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
H1 : P
______________________________________(1/1)
Q
証明 | without Coqの 変形4 givens / goalと見比べてみます。
- givens（再掲）
\forall P ((P \Rightarrow Q) \Rightarrow Q)
(P \Rightarrow Q) \Rightarrow P
P
- goal（再掲）
Q
一致していることが確認できました。
残りのコードを実行すると証明完了になります。
introduction.v
Goal forall (P Q: Prop), (forall P: Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.
Proof.
intros.
apply H0.
intro.
apply (H(P->Q)).
apply (H P).
Qed.
めでたしめでたし。
まとめ
- まだ始めて1日ですが、表現したい命題をうまくコードに落とし込むためには Coq のライブラリに慣れる必要があり、習得コストはなかなか高そうです。
- 慣れると面白いかもしれません。