Coqでもあのニンジャパターンマッチが使えるぜ

Coqでペア(2つ組)を束縛するlet式のときにはOCamlと同様に束縛する側にパターンを書くことができる。

let(x,y):=(1,2)in...

しかし、これが3つ組になるとエラーとなる。

let(x,y,z):=(1,2,3)in...

Error: Destructing let on this type expects 2 variables.

これはCoqのNinjaパターンマッチが2つ組だけしか考慮していないというわけではない。

let(変数名1,...,変数名n):=式1in...

という式は実は一般的に単一コンストラクタを持つすべてのInductive型で使用できることができ、それは次の内容と等価になる。

match式1with|コンストラクタ(変数名1,...,変数名n)=>...end

これはタプル以外でも使えるという利点がある一方で、入れ子になるパターンでは使えないという不便な点もある。上での3つ組でのエラーはちょうどその場合ではまっているということである(Coqの(1,2,3)は内部では((1,2),3)と扱われる)。

これだと不便だという事で、入れ子になったパターンマッチに対応した構文が用意されている。3つ組でのNinja パターンマッチをしたい場合は次のように書けば良い。

let'(x,y,z):=(1,2,3)in...

それでは、良いニンジャパターンマッチを！

参考: https://coq.inria.fr/distrib/current/refman/Reference-Manual004.html