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

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

Ninja.v

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

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

Ninja.v

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

Error: Destructing let on this type expects 2 variables.

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

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

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

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

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

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

Ninja.v

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

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