http://hal.archives-ouvertes.fr/docs/00/40/77/78/PDF/RT-367.pdf のざっくりした訳

方針

• 正確な訳にするよりも、意味がつかめる訳に。(時間がないので)
• パラグラフは崩さない
• 訳語の統一とかはあとで考える
• tacticもtacticsもタクティクスと訳してしまってるのは、あとでなんとかします。

イントロダクション

ssreflectはCoqをベースにした言語です

SSreflectはCoqをベースにした証明を行なうための形式言語です。Coqを定義言語と使いつつ、追加のタクティクス(推論や長い証明を書くのに便利なやつ)を提供します。 また既にこの拡張は非常に効果的であると実証されています。(参考: ssreflectを利用した4色定理の証明)

ssreflectの追加したタクティクスはほとんどありません。ただし各タクティクスを組合せることで、様々な状況に対して適用することができます。また各タクティスクを組合せると、証明のコードがペンと紙による証明と同じくらい短かくなることがあります。

対話的な証明の構築

Coqを使うと対話的に証明を構築できます。 subgoalとかそういうやつ。

(※Legacy Coqとあまり違いが見えないので、省略)

チュートリアルの構成

2節はCoqチュートリアル(v8.1)をssreflectに書き直したやつです。
3節はユークリッド分割に関する例を示します。実際に試しながら読むのお勧めします。また説明は直感的なものなので、もっと形式的な説明はリファレンスマニュアルを読んでください。

Coqチュートリアル(ssreflect版)

以下のファイルはssreflectの標準ライブラリからインポートされます。

Require Import ssreflect ssrbool eqtype ssrnat.

ヒルベルトの公理 S

練習のためにステップバイステップでヒルベルトの公理Sを証明してみましょう。

Section HilbertSaxiom.

Variables A B C : Prop.

Lemma HilbertS : (A -> B -> C) -> (A -> B) -> A -> C.
Proof.
move=> hAiBiC hAiB hA.
move : hAiBiC.
apply.
  by [].
by apply : hAiB.
Qed.

コマンド Section HilbertSaxiom は、あとで閉じられるCoqのセクションを始めます。

コマンド Variable A B C : Prop は命題変数A,B,C(型はProp)を仮定します。 これらの変数は今のセクション HilbertSaxiomの中で使えます。

上の補題は HilbertS と呼ばれます。 (A -> B -> C) -> (A -> B) -> A -> CにおけるA -> B -> CはA -> (B -> C) という意味です。 これは「Aが成り立ち、Bが成り立つならば、Cが成り立つ」という意味です。

正確に言うと、これは(A /\ B) -> C(AとBが成り立つならばCが成り立つ)とは違います。 が、2つの文は等価です。

証明の中でのコマンド move=> hAiBiC hAiB hA は証明スタック(ゴール)の上にある仮定、すなわちA -> B -> Cをコンテキストに導入し、 hAiBiCと名付けます。 そして残り2つのゴールの仮定に対しても同じことをします。 これはCoqのコマンドのintros hAiBiCi hAiB hAと同じことをします。

コマンド move=> hAiBiC hAiB hA TooManyは、仮定の数が違うので失敗します。

タクティクスmove=>は2つに分割できる。 moveはタクティックですが、=>は tactical(※訳要検討)と呼ばれます。 moveタクティクスは実際には効果を持っていません。 Coqのタクティクス intros はtactical => によってのみ実行されます。
ここで、ssreflectは証明がでかくなっても大丈夫なように、読み易い変数名を使うことが多いです。

コロン:もまたtacticalです。 これは=>の逆です。なので、 move: hAiBiC は仮定からhAiBiCを取り除いて、ゴールの一番左に置きます。 もし仮定 hAiBiC がコンテキストになければ、タクティクスは失敗します。 対応するCoqのコマンドは revert hAiBiCと同じです。

同様にmove : (hAiBiC)はCoqのコマンド generalize hAiBiC と同じです。 これはコンテキスト中の仮定を消しません。

The tactic apply tries to see the right-hand side of the goal (i.e. the proof stack without its top) as an instance/-consequence of the left-hand side (i.e. the top of the proof stack), and it asks the user to provide missing arguments.

これによって今のケースに対する2つのサブゴールが生成されます。

次のタクティクス by []の前のインデントは、2つのサブゴールがここで証明されることを示しています。

タクティクス by [] で証明できるということは、現在のサブゴールがトリビアルということです。

by []はもっと一般的な文法である by [tactic1 | tactic2]の特殊な形です。 これはtattic1を試して失敗したら、次にtactic2を試して....とやっていき成功した段階でゴールをトリビアルに解けるかどうかを試します。 全部失敗したらタクティクス自体が失敗します。 こんな感じの今のサブゴールを解くことができなければ失敗するタクティクスはterminatorと呼ばれます。 by [] のあとに、サブゴールが1個しか残ってないので、インデントを元に戻せます。 インデントと terminatorはでかい証明を読み易くします。

コマンド apply : hAiB は move: hAiB. apply. の略記です。 これはCoqのセミコロン;と同じように move: hAiB; apply.と書くこともできます。

Coqのtactic1; tactic2.と同じようにtactic1によって生成された全部のサブゴールに対してtactic2が実行されます。それか失敗します。

証明の最後の単語はQedです。 これで証明全体が検証します。 これはステップバイステップで実行される検証よりも信頼度が高いです。 ステップバイステップのやつはタクティクス全体の正しさに依存してますが、QedでやられるやつはCoqのちっこいカーネルの正しさのみに依存してます。

証明はもっと短かくなります。補題を書く前に仮定を宣言するのはいいことです。すると今のセクションの間で使えます。なお、Coq的にはVariable、 Variables、Hypothesis、Hypothesesは全部同じ意味です。

Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).

Lemma HilbertS2 : C.
Proof.
apply : hAiBiC; first by apply : hA.
exact : hAiB.
Qed.

この証明でコマンド apply : hAiBiC; first by apply : hAはまずapply: HAiBiCを実行したのち、生成された最初のザブゴールにby apply: hAを実行します。 tactical first は selectorと呼ばれます。もし first がなければ、Coqは両方のサブゴールにapply : hAを実行し、2つめのサブゴールで失敗します。

terminator by がなくても、証明は成功します。 ssreflect的には、サブゴールを終わらせるタクティクスはterminator(sub-Qed)にするのがお約束です。証明の構造に関するこういう情報は、証明を読みやすくするだけでなく、変更にも強くします。Indeed, consider one given theorem relying on a prior development (i.e. definitions and lemmas). When the software or the prior development changes (new version or new formalism) the previous proof of the theorem may not be valid any longer. In order to patch the proof, one may want to start modifying the old proof where the interpreter first rejects the old proof. However, the first rejected step may not be the first step where the proof script deviates from the intended proof. Deviation may have occurred long before the place where an error is detected, and irrelevant steps may still be approved by the interpreter by chance, which interferes with debugging. On the contrary, terminators fail if they don’t finish the current subgoal, thus avoiding approval of irrelevant proof steps. This facilitates debugging. (よくわかんないけど、変更するときに便利だよ、って書いてある気がする。)

コマンド exact: hAiB.はmove: hAiB; exact.の略記です。 ここでterminator exactはapplyとby []の組み合わせの1種です。

Hilbertの公理Sはもっと短かく書けます。

Lemma HilbertS3 : C.
Proof. by apply: hAiBiC; last exact: hAiB. Qed.

証明は最初にapply: hAiBiC.を実行したのち、exact : hAiB.をapply: hAiBiCで生成されたサブゴールのうち最後のやつに対して実行します。 そのあとbyによって残っているサブゴールを終わらせます。

先に進む前に、小さいCoqのオブジェクトや項から、より大きいオブジェクトや項をどうやって作るかを説明しておきます。あと、それらの型がどうなるかも説明します。 以下の変数がすでに仮定されてるものとします。

Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).

ここで、項(hAiB hA)は型Bを持ちます。(伝統的な数学的な記法だと、f(x)っぽい感じでhAiB(hA)となります。) 項の型はCheck (hAiB hA).で確かめることができます。

また項(hAiBiC hA)は型A->Bを持ちます。 そして、項((hAiBiC hA) (hAiB hA))は型Cを持ちます。またこれはhAiBiC hA (hAiB hA)と書くことができます。

ヒルベルトの公理Sはもっと短く書くことができます。

Lemma HilbertS4 : C.
Proof.
exact : (hAiBiC _ (hAiB _)).
Qed.

上記の項(hAiBiC _ (hAiB _))は2つのプレースホルダー_で表現される穴が含まれています。 でも、まだ十分な情報を含んでいるので、ssreflect(Coq)はその穴を推論できます。この証明はHilbertS3に似てます。 HilbertS3の証明では明示されている項が、この証明では推論されています。

もっともっと短かい証明もあります。

Lemma HilbertS5 : C.
Proof.
exact : hAiBiC (hAiB _).
Qed.

上記の証明で、(hAiB _)はBをゴールCの上に追加します。 このとき、必要となる引数Aはあとでなんらかの方法で提供される必要がある。 そのあとゴールの上にhAiBiCの仮定を追加し、それを適用します。 そのあとAを証明します。 exact terminatorはトリビアルな証明ができます。

証明された補題は、以下のように証明に使うことができます。

Lemma HilbertS6 : C.
Proof.
exact : HilbertS5.
Qed.

HilbertS5は画面上には表示されていませんが、コンテキストには属しています。

ヒルベルトの公理Sのそれぞれの証明を比較してみましょう。

Print HilbertS5.
Print HilbertS2.
Print HilbertS.
Check HilbertS.
End  HilbertSaxiom.

Print HilbertS5.

コマンドPrint HilbertS5.はHilbertS5のproof term(証明項?)を表示します。 proof termとは、Qedのときに検証されたオブジェクトのことです。 このオブジェクトは hAiBiC hA (hAiB hA) みたいな感じになってます。

これの型はCです。別の言い方をすると、hAiBiC hA (hAiB hA) は命題Cの証明です。 HilbertS2を表示させると、2つのオブジェクトが同じことがわかります。 証明項が同じでも構築方法が異なっているということです。HilbertSの証明項は他のやつよりでかいです。 それは仮定がセクションやコンテキストの変数として与えられているのでなく、直接含まれているからです。

コマンドCheck HilbertS.はHilbertSの型を表示します。Checkは与えられた補題がどういうやつだったかを思いだすのに使えます。

コマンドEnd HilbertSaxiomでCoqのセクションを閉じたあと、そのセクションの変数は使えなくなります。 つまりセクション内で証明された補題は、使われた変数が含まれます。 なので、コマンドPrint HilbertS5が以前と違った出力になります。 補題HilbertSと補題HilbertS5は同じ証明項を持ちます。

Logic connectives

(WIP)