日々の流転

λ. Agda2での複数引数のパターンマッチと definitional equality の落とし穴

以下のような関数があったとする。

f : Bool -> Bool -> Bool
f true true = true
f _ _ = false

このとき、f false x と false の間には definitional equality は成り立つが、f x false と false の間には definitional equality は成り立たないのね。 例えば、以下のようなゴールはそのままではrefine出来ない。

test : forall x -> f x false ≡ false
test x = {! ≡-refl !} -- Oops!, can't refine!

パターンマッチは構文的には全ての引数に対して同時にパターンマッチしているかのように見えるが、実際には左の引数から順に1引数毎にしかパターンマッチしていなくて、どの節を用いるかが決定できていないということだろうか。 こうなっていることには何か理由はあるのだろうけど、非常に直観に反する振る舞いだと思った。

また、単に直観に反するだけでなく実際に困ることもあって、上の例のようなものを証明するときには、先行する全ての引数について場合わけして具体化しなくてはならない。 上の例であれば以下のようにすれば良いのだけど、これは引数の個数や構築子の種類が多い場合には非常に面倒だ。

test : forall x -> f x false ≡ false
test true  = ≡-refl
test false = ≡-refl