Coq で map や filter の fun を省略したい。

More than 1 year has passed since last update.

言いたいこと

  • 結果的に引数が一つの函数となる (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.

状況説明

mapfilter など、一引数函数を引数とする函数について

  1. map (fun x => f hoge x fuga) l
  2. filter (fun x => x <= 3) l

などという書き方をすることになるのだが、 Generalizable Variables オプションを使うと、これを

  1. map `(f hoge x fuga) l
  2. filter `(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

詳しくは リファレンスマニュアルの該当部 を見てもらうとして、簡単に説明すると、
`()`{} で囲まれた自由変数を含む項を、閉じた項に変換してくれる機能である。

例では型変数や型のパラメータに使っているが、もちろん普通の(?)項にも利用可能だ。
案外、こちらの使い方には思い至らないことが多いかもしれない。

implicit generalization を可能にするためのオプションが Generalizable Variables オプションとなる。

Generalizable Variables オプション

このオプションには基本的に二つの使い方がある。

一つ目は、自由変数として利用可能な変数名を指定する方法である。これは

Generalizable Variables x y foo bar.

というようにオプションの末尾に使いたい変数名を列挙する。
すると、 xfoo はもちろん、この変数名に数を繋げたもの(x1foo200 など)が自由変数として利用可能になる。

二つ目は、どんな名前でも自由変数として利用可能にするためのもので、

Generalizable All Variables.

とする。 `()`{} の中では、既知の変数であればそちらだと正しく推論されるので、その点についての心配はいらない。

しかし、この場合、タイポに注意しないと予期せぬエラーを引き起こすことになるので注意が必要だ。
例えば TypeTypr にタイポしていたりするとどこかでエラーが起きる。

証明モード中での利用

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) とすれば、求めている通りの項になる。