mathink/coq_omit_fun.md

## coq_omit_fun.md

      
    Raw
  

              coq_omit_fun.md
            
          
  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) l
filter (fun x => x <= 3) l

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

map `(f hoge x fuga) l
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.
というようにオプションの末尾に使いたい変数名を列挙する。
すると、 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) とすれば、求めている通りの項になる。