Library ssr_discharge

move:

SSReflect で、move=> H は証明対象の命題から前提に移すものですが、 逆に、前提から証明対象の命題に移すのは move: H を使います。 正確には、move: というのは move というなにもしない tactic に : という tactical をつけたもので、 他の tactic にも : をつけられるのですが、その点については気にしないことにします。

?Goal

先ほどのセクションの説明と同じく、P -> P の証明ですが、 最初に Show Proof とすると、?Goal と表示され、 証明項はまったくできていないことがわかります。

(fun H : P => ?Goal)

move=> H で、H : P を前提に移したところで Show Proof とすると、(fun H : P => ?Goal) となり、 引数Hを受け取る関数抽象が構築されることがわかります。

[eta ?Goal]

ここで move: H として、H : P を証明対象に戻したところで Show Proof とすると、 eta ?Goal と表示されます。 Display notations を無効にして Show Proof をやりなおすと、 (fun H : P => ?Goal H) と表示されます。 まずわかることは「戻す」というのは証明項が元に戻るわけではないことです。 実際には ?Goal が ?Goal H に変化する、つまり、戻したものを引数とする関数呼び出しが構築され、 関数部分が新しいゴールとなります。

(fun H : P => (fun H0 : P => (fun H1 : P => ?Goal H1) H0) H)

意味もなく move=> H と move: H を繰り返してみると、証明項は (fun H : P => (fun H0 : P => (fun H1 : P => ?Goal H1) H0) H) となります。関数抽象と関数呼び出しが増えていることが分かります。 Coq が表示する前提と証明する命題は変わりませんが、 内部では証明項が（意味もなく）膨らんでいるわけです。 ここで、?Goal の外側には H, H0, H1 の束縛がありますが、 前提にこれらは表示されていません。 これは、Coq がすべての束縛を前提に表示するわけではなく、 move: は指定した前提を前提から表示しないようにするためです。 指定した前提を表示したままにするには、カッコでくくります。 その動作を確認する前に、証明を最初からやり直すため、Restart コマンドを使います。

?Goal

Restart の後で Show Proof とすると、?Goal とだけ表示され、 今まで構築した証明項が消えていることが確認できます。

ここでは、H が前提に表示されたままになっています。

ここで、さらに move=> H としようとすると、失敗します。 (Fail というのはコマンドを実行して失敗することを確認するコマンドです) これは証明すべき命題 P -> P の左側を前提に H という名前で移す指示ですが、 H という名前はすでに前提に存在するので、Error: H is already used. というエラーになります。

ここで Ha という別の名前を使えば問題なく成功します。

[eta [eta [eta [eta ?Goal]]]]

eta で表示されると中身がよくわからないので Display notations を無効にすると、 以下のようになります。

(fun H : P =>
 (fun Ha : P => (fun Hb : P => (fun Hc : P => ?Goal Hc) Hb) Ha) H)

このように move: と move=> を数回くり返して Show Proof とすると、 move: に指定した Ha, Hb, Hc を引数とする関数適用が構築されていることがわかります。 ところで、move: が関数適用を構築し、指定されたものを引数にするのであれば、 べつに引数にするのはべつにすでにある前提でなければならない理由はないことに 気がついたでしょうか。 実際、move: ではそのような関数適用を構築することも可能です。

nat -> P -> P

このように、move: 0 として 0 を指定すると、証明すべき命題は P -> P から nat -> P -> P に変化します。 指定した 0 はどこにいってしまったのかというと、Show Proof でわかります。

(?Goal 0)

つまり、証明項は関数適用として構築され、その引数は move: に指定した 0 になっています。 ?Goal の型はまず 0 を引数としてとるので、nat の値を引数に関数型となります。 そのため、証明すべき命題は nat -> ... となっているのです。 このように前提ではないものを move: に指定したときは、前提から取り除きようがありませんから 前提は変わりません。 move: に複雑な式を指定する場合はかっこでくくります。

(?Goal (1 + 2))

ここでは 1 + 2 を move: に与えていて、証明項に構築された関数適用では、 引数が 1 + 2 になっていることがわかります。 move: にかっこでくくったものを指定した場合、move: はそれを前提から取り除きません。 複雑な式（外側で束縛された変数以外の何か）であればそもそも前提にないので取り除けませんし、 前提のいずれか（外側で束縛された変数）であっても取り除きません。 むしろ、かっこでくくらずに前提を指定したときのみ、前提に表示しないように取り除く、 と考えるのが適切でしょう。 move: の動作は確認できたので証明を終りましょう。 ここでは Abort で証明を中断する、つまり証明項を完成させずに終ることにします。