ssreflect tutorial(意訳版) [作業中]

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の標準ライブラリからインポートされます。

```coq
Require Import ssreflect ssrbool eqtype ssrnat.
```

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

```coq
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`は全部同じ意味です。

```coq
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はもっと短かく書けます。

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

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

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

```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はもっと短く書くことができます。

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

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

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

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

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

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

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

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

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

```coq
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)