TODO多めのまま公開します。別に書いてた下書きが消えたので。

定理証明のコンテストシステムを作って、今日の夕方に第1回のコンテストを開催していた。https://t.co/8vi0dWszRW
— あしぃ (@asi1024) 2019年8月18日

これです。

定理証明コンテストとは,

定理証明支援系を用いて与えられた定理に対して証明を与えるコンテストです。

現在コンテストサイトに実装されている支援系はCoqです。

Coqで解く問題の見た目はこんなかんじです。

Definition task := forall n m, n * S m = n + n * m.

Theorem solution: task.
Proof.
  unfold task.
  (* FILL IN HERE *)
Qed.

これはn×(m+1)とn+(n×m)が任意の自然数n,mについて等しいことを示せというものです。

FILL IN HEREの部分にCoqの言葉で証明を与えます。

この問題を通そう

環境準備

Coqのインストールをしたのち，Coqをインタラクティブに使うツールを用意します。

ツールにはEmacs+ProofGeneralが最も標準的です。 WindowsではCoqIDEを使う方法もあります。

vscodeとその拡張vscoqを使う方法も存在したのですが, 現在バグだらけで使い物になりません。昔のvscodeのバージョンを用いると使えるらしいですが, その方法をおすすめすることはできません。

Emacs+Spacemacs+ProofGeneral導入記事は後で書くことにします。TODO

~~ここでは他の選択肢として，macでvscode+vscoqを用いる方法を説明します。~~

初めに brew install coq でcoqを入れます。そしてここが肝心ですが，vscodeの拡張であるvscoqはすでに更新がされておらず，最新のvscodeでは正常に動作しません。なので2年前ぐらいのvscodeをダウンロードして利用しましょう。

Visual Studio Code January 2018

vscodeでvscoq拡張をインストールします。

~~そうして*.vファイルを開くと，次の証明画面が出ます。~~

TODO

定義

というわけでこの命題を示しましょう。

forall n m, n * S m = n + n * m.

定理の証明にはまず定義を観察することが大事です。

ドキュメントに定義があります。

Standard Library | The Coq Proof Assistant

https://coq.inria.fr/library/Coq.Init.Datatypes.html#lab1084

また, Coq上でも定義を見ることができます。 TODO

初めに，自然数の定義が次のように帰納的定義がされています

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

natという集合は，次の2つのコンストラクタから生み出されるものである。

コンストラクタ"O"は無引数でnatである。
コンストラクタ"S"はnatを引数に取ることでnatである。

と読みます。

例えばOやS (S O)なんかがnatで有ることがわかります。

そして, これが我々の良く知る自然数であるところの0や2に対応しています。

実際に，0や2もcoqで書くことができ，これはcoqではそれぞれOとS (S O)のエイリアスです。

また，+ の定義はaddという関数の糖衣構文で

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (p + m)
  end

where "n + m" := (add n m) : nat_scope.

掛け算の定義はmulという関数の糖衣構文で

Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end

where "n * m" := (mul n m) : nat_scope.

と再帰的に定義されています。

matchは関数型言語ではおなじみのパターンマッチです。

その項のコストラクタによって場合分けを行い, その先の項を返します。

match 項 with
  | コンストラクタ1 引数1 => 項1
  | コンストラクタ2 引数2 => 項2
end

計算の例を示すと，

2+1を計算する例は

S (S O) + S O
= add (S (S O)) (S O)
= match (S (S O)) with
    | 0 => (S O)
    | S p => S (p + (S O))
  end
= S(S O + S O)
...
= S(S(O + S O))
...
= S(S(S(O))

ここで，S (S (S O)) + S Oは(S (S (S O))) + (S O)と読むことに注意してください。演算子のほうが関数適用っぽいものより優先度が弱いです。

2*3を計算する例は,

S (S O) * S (S (S O))
= mult (S (S O)) (S (S O))
= S (S (S O)) + S O * S (S (S O))
= S (S (S O)) + S (S (S O)) + O * S (S (S O))
= S (S (S O)) + S (S (S O)) + O
...
= S (S (S (S (S (S O)))))

という感じです。

Coqは便利で，具体的な例の計算ならやってくれます。

Theorem ex_2_plus_1_eq_3: S (S O) + S O = S (S (S O)).
Proof.
  simpl.  (* S (S O) + S O の部分を計算してくれる *)
  reflexivity. (* 両辺が同じ項の=となっているゴールを達成する *)
Qed.

これで2 + 1が3であることを形式的に示すことができました!

証明tactic

ex_2_plus_1_eq_3の例では, 実際に証明を行っています。 coqでは定理の証明を次の形で書きます。

Threom 名前: 命題.
Proof.
  証明tacticの列
Qed.

Proof.のあとに続くのは証明のtacticというものです。これは, 証明の状態を変化させます。

証明の状態とは, 証明するべきものである｢ゴール｣の列です。ゴールとは次の形で表されます。

仮定の列 |- 結論

｢仮定の列から結論を導く｣ことを要求するものがゴールです。

始めに Theorem で示したい命題を与えると,

|- 命題

このように, 仮定の列が空で, 命題が結論となったゴールが1つだけ状態から始まります。このゴールに対してtacticを適用することで, ゴールを変えたり, 達成したり, 増やしたりします。そして, これらゴールをすべて達成すると, 証明を完遂したことになります。

Coqのインタラクティブツールで普通右側に表示されている状態は, この状態を表しています。

tacticをStep実行してみましょう

Theorem ex_2_plus_1_eq_3: S (S O) + S O = S (S (S O)).
Proof.
  simpl.
  reflexivity.
Qed.

例交えてやる。　TODO

taciticの一覧はここにあります TODO

証明

さて, 初めに示した命題の証明を行いたいと思います。

Definition task := forall n m, n * S m = n + n * m.

Theorem solution: task.
Proof.
  unfold task.
  (* FILL IN HERE *)
Qed.

TODO

自動証明tactic

実はCoqのtacticは力強く, この程度の命題であれば自動で解いてくれる強いtaciticがあります。

自動証明tacticはゴールに対してtacticを適用するかを定義することで作られています。

例えばこの例では, ringというtacticを用いれば自動で行ってくれます。他にも, auto, eauto, omegaといったtacticがあります。

しかしこれらは, 証明してくれる命題の範囲がそれほど広くないです。それぞれのtacticの証明戦略を理解した上で, その証明を自分でもできるときに限って使うのが良いです。

僕が示せなかった証明を振り返る

長くなってきたので後編へ移ります。

Coqの勉強法はこれが一番有名らしいです。

わたしはこれやった https://t.co/lzg6cOnIPy
— そすうぽよ@技術書典く54D (@_primenumber) 2019年8月21日

また京大の五十嵐先生の講義テキストも便利です。 Computation and Logic: Winter Semester 2018

最後に宣伝なのですが, 証明コンテストTopProverは出れば出るだけ得するレートの付き方をするらしいです。是非参加して証明力を高めましょう。

wassup?

新ブログ→memo.wass80.xyz

定理証明コンテストに参加した [WIP]