Lean Proverのinaccessible termについて

最近Lean Prover (Lean 3)で原始再帰的関数について証明を書いているので、それによって得られた知見を一つ紹介する。

gist.github.com


inaccessible termとは何か

".(項)"の形のパターンはinaccesible termと呼ばれ、パターンマッチを行う際に、この部分はパターンとしてではなく、項として一致するかどうかの検査が行われる。(つまり、パターン以外の項が書ける。)
項の部分は同じパターン内ですでに定義されている変数でなければならない。項の内部で新しい変数を導入することはできない。

使用例

埋め込んだコードのprim_evalの定義(ll. 36-48)でパターンマッチを行なっているが、これのl.40, l.42で使用されている。
典型的な使用例として、同じ値が複数個出現することがわかっているパターンマッチ(l.40のマッチングではmが2回登場する)で使用できる。(パターン内で同じ変数名を複数回使うことはできない。)
また単にパターンが複雑になってしまったり、マッチさせなくても自動で推論できる場合にマッチを省略する目的でも使用できる。(l.42のマッチングでは".(_)"というパターンがあるが、これはprim_evalの第一引数はk + 1であることが推論できるため合法である。)

なお、ここでの本題とは外れるが、l.40のパターンに含まれている"@prim_rec.prec"の"@"は、@演算子と呼ばれ、implicit parameter (l.5のkとm)を陽に引数にとる、という効果を持つ。これがないとkをパターンマッチさせることができず、この場合はfの型が推論できないというエラーが出る。

参考文献

Theorem Proving in Leanの8.5 Inaccessible Terms (inaccessible terms), 2.9 Implicit Arguments, 6.8 Displaying Information (@演算子)