Library reflexivity

reflexivity

reflexivity は X = X という命題を証明する tactic です。 SSReflect ではふつう by [] などで済ますのであまり使いませんが、 等式の扱いの説明をするのに都合がいいので説明しましょう。

eq_refl

なんか、省略されているっぽいので Display all low-level contents を有効にして Show Proof をやり直すと、以下のようになります。

(@eq_refl nat O)

O というのは 0 です。 Coq の theories/Init/Logic.v をみると、eq は以下のように定義されています。

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

ちょっといろいろと複雑ですが、これは eq という型と eq 型の値を構成する eq_refl というコンストラクタを定義しています。 ただし、パラメータがついているので 単にひとつの型とコンストラクタを定義しているわけではありません。 About で eq 定義を調べてみましょう。 (Display implicit arguments を有効、Display notations を無効にしておきます)

eq : forall (A : Type) (_ : A) (_ : A), Prop

これをみると、eq は A という型と、A型の値ふたつを受け取って、 命題を返す関数であることがわかります。 コンストラクタの eq_refl も調べてみましょう。

eq_refl : forall (A : Type) (x : A), @eq A x x

eq_refl は A という型と A 型の値 x を受け取って @eq A x x という型の値を返す関数 であることがわかります。 カリーハワード対応により命題と型は同型なので、 eq が命題を返すというのと、 @eq A x x が型というのは同じことです。 さて、eq は 3つのパラメータをとるので、 @eq A a b というように 3つパラメータを与えれば具体的な型になります。 たとえば、@eq nat 1 2 はひとつの具体的な型です。 それに対して、コンストラクタが返す値の型は @eq A x x なので、 必ず x と y は等しくなります。 つまり、@eq_refl nat 1 という値の型は @eq nat 1 1 という型であり、 eq_refl で @eq nat 1 2 という型の値を作ることはできません。 そして、eq_refl 以外で eq 型の値を作ることはできません。 （Inductive というのは帰納ということで、帰納的に定義する、というのはそういうことです。 まじめに帰納的定義を書くときには「以上のやりかたで作れるものだけがうんたら」などと書きますよね。） ついでにいえば、リストの cons みたいな （リスト型の値を引数として受け取る）コンストラクタと違って、 eq_refl は eq 型の値を受け取る引数を持たないので、 eq 型の値を作るには eq_refl を一回使う以外の方法はありません。 結局、@eq A a b という型は、 a と b が等しい場合は eq_refl によって構成されるただひとつの値を持ちます。 そして、a と b が等しくない場合はまったく値をもちません。 この性質により、@eq A a b という型に対してその型に適合する値を作れるならば、 a と b は等しいということがいえるわけです。 つまり、a と b が等しいという命題や証明を eq 型で実現できるわけです。

さて、ここで問題は「等しい」というのはいったいどういう意味か、という点です。 まぁ、最初の 0 = 0 のように、完全に同じ形であれば等しいのはそうでしょうが、 異なる形でも等しいことはないのでしょうか。 たとえば、2 + 4 = 5 + 1 はどうでしょうか。 ということで、試してみましょう。

(@eq_refl nat (5 + 1))

どうやら問題なく証明できてしまうようです。 証明項は (@eq_refl nat (5 + 1)) です。 どうも、reflexivity は等式の右辺を eq_refl の引数にする感じです。 そうでない証明項は許されるのか、exact で証明項を与えて試してみましょう。

(@eq_refl nat 6)

とくに問題なく証明できました。 つまり、eq_refl 6 という項は @eq nat (2 + 4) (5 + 1) という型の値として正しく受け付けられるというわけです。 「eq_refl は A という型と A 型の値 x を受け取って @eq A x x という型の値を返す関数」 と上で述べましたが、ここで eq_refl の引数として指定した x は 6 です。 したがって、eq_refl 6 は @eq nat 6 6 型の値なわけですが、 Coq はここで、この型が @eq nat (2 + 4) (5 + 1) 型と等しいかどうか確認します。 具体的には、計算を進めて同じ項になるかどうかを確認します。 2 + 4 や 5 + 1 は変数が入っていないので計算を最後まで行うことができ、その結果は 6 です。 そのため、Coq は @eq nat 6 6 型と @eq nat (2 + 4) (5 + 1) 型が等しいことを確認でき、 erefl 6 が @eq nat (2 + 4) (5 + 1) 型の要素であることを判断できます。 この、「計算を進めて同じ項になる」ようなものを convertible といいます。 正確な定義は Coq Reference Manual, 4.3 Conversion rules に書いてあります。 計算を進めても等しさを確認できない場合もあります。

ここでは n という自然数の変数があって、n + 1 と 1 + n が等しいことを証明しようとしています。 ところが、残念なことに、reflexivity は失敗します。 Coq で n + 1 と 1 + n がどこまで計算を進められるか、Compute というコマンドで 実際に計算を行って確かめてみましょう。

     = (fix Ffix (x x0 : nat) {struct x} : nat :=
          match x with
          | 0 => x0
          | S x1 => S (Ffix x1 x0)
          end) n 1
     : nat

n + 1 というのは、なにか fix とかいうもので始まる関数が展開されて、 そこで止まってしまいました。 この関数は加算の関数で、最初の引数が 0 かそれ以外かで場合分けを行って計算を行います。 ところが、最初の引数は変数の n であり、これが 0 かどうかは不明です。 そのため、計算がここで止まってしまうのです。 逆に、最初の引数が変数ではなく、具体的な自然数が与えられれば、計算を進めることができます。 1 + n はその例であり、こちらはもっと計算が進みます。

     = S n
     : nat

1 + n では、かなり単純な項になるまで計算が進んでいます。 というわけで、n + 1 と 1 + n では、計算を進めても同じ項にたどり着けないので、 reflexivity は失敗してしまうのです。

あと、いちおう注意しておくと、 reflexivity は完全に計算を進めるわけではありません。

(@eq_refl nat (2 ^ 100))

2 ^ 100 というのは 2 の 100乗で、本当に計算しようとすると、メモリがあふれてしまいます。 （Coq の自然数はペアノの自然数なので、2^100 を計算すると、 S を 2^100 個メモリに並べる必要がありますが、 これを素朴に実装すると 64ビットのメモリ空間でも足りません。 そして、Coq はいまのところ素朴に実装しているのです。 どうにかしてほしいところですが。） しかし、ここの reflexivity でメモリがあふれないことからわかるように、 計算を進めなくても同じ項であることがわかるなら、それは問題なく判断してくれます。