| title | tags | author | slide |
|---|---|---|---|
Coq で map や filter の fun を省略したい。 |
Coq |
mathink |
false |
- 結果的に引数が一つの函数となる
(fun x => f ... x ...)という項が`(f ... x ...)と書ける - そのためには
Generalizable Variablesオプションを使う。 - ただし、証明モード中の利用には注意が必要。
以下のコード中の Compute の結果は全て同一である。
Require Import Arith List.
Import List.ListNotations.
Open Scope list_scope.
Infix "<=b" := leb (at level 80, no associativity).
Definition testdata := [4;1;5;6;0;13;8;9;11;23;5;7;2].
Compute filter (fun x => x <=b 3) testdata.
Definition flip {X Y Z: Type}(f: X -> Y -> Z): Y -> X -> Z :=
fun y x => f x y.
Compute filter (flip leb 3) testdata.
Generalizable Variables x.
Compute filter `(x <=b 3) testdata.map や filter など、一引数函数を引数とする函数について
map (fun x => f hoge x fuga) lfilter (fun x => x <= 3) l
などという書き方をすることになるのだが、 Generalizable Variables オプションを使うと、これを
map `(f hoge x fuga) lfilter `(x <= 3) l
と書くことが出来る。
特に効果を発揮するのが二番目の例。
Notation なり Infix なりで二項演算の中置記法 <= を定義していると、引数の順序を入れ替える函数 flip f y x := f x y があったとしても flip <= 3 のようには書けない。
なので、どうしても元の関数名(たとえば leb)を使わざるを得ない。
しかし、 flip leb 3 はどう見ても可読性に欠けているので、可能なら <= を使いたい。
すると、結局 fun を使って fun x => x <= 3 と書くことになる。
ここで、 Generalizable Variables オプションによる implicit generalization を利用すると、代わりに `(x <= 3) と書いて同等の項を得ることが出来る。
単独で使っても便利な機能だが、 Notation コマンドなどと組み合わせることで、可読性の向上により貢献する機能である。
詳しくは リファレンスマニュアルの該当部 を見てもらうとして、簡単に説明すると、
`() や `{} で囲まれた自由変数を含む項を、閉じた項に変換してくれる機能である。
例では型変数や型のパラメータに使っているが、もちろん普通の(？)項にも利用可能だ。 案外、こちらの使い方には思い至らないことが多いかもしれない。
implicit generalization を可能にするためのオプションが Generalizable Variables オプションとなる。
このオプションには基本的に二つの使い方がある。
一つ目は、自由変数として利用可能な変数名を指定する方法である。これは
Generalizable Variables x y foo bar.というようにオプションの末尾に使いたい変数名を列挙する。
すると、 x や foo はもちろん、この変数名に数を繋げたもの(x1 や foo200 など)が自由変数として利用可能になる。
二つ目は、どんな名前でも自由変数として利用可能にするためのもので、
Generalizable All Variables.とする。 `() や `{} の中では、既知の変数であればそちらだと正しく推論されるので、その点についての心配はいらない。
しかし、この場合、タイポに注意しないと予期せぬエラーを引き起こすことになるので注意が必要だ。
例えば Type を Typr にタイポしていたりするとどこかでエラーが起きる。
assert などで項を直接記述するときにも同じように implicit generalization を利用したい時は、気をつけておかねばならない。
仮定部にある変数が既知のパラメータだとわからず、過剰に generalize されてしまうためである。
仮定部に y: A があり、 assert の引数として map `(x < y) l のように implicit generalization の対象となる項に y が含まれているものを与えた場合、 map (fun x => x < y) l ではなく map (fun x y => x < y) l として処理されてしまう。
これを避けるには let を使って項の中で y を束縛しておくとよい。
let y' := y in (map `(x < y') l) とすれば、求めている通りの項になる。