Hatena::ブログ(Diary)

chiguriの生態(嘘や誇張アリ)

2012-03-22

補足:inversionやinduction

| 22:17

ちょっと説明してないのもどうかと思ったので。


述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う(inductionはかなり稀か)。

「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら怒られた」という経験がある人もいるだろう。

実はこれもまったく同じ原因である。

というのも、tacticは一般に関数や項を作るからだ。


introやapplyのように簡単なtacticは対応する項も割と簡単(関数抽象・関数適用)である。

一方、inversionは結構小難しいことをする。

しかし、小難しいことをしようが何をしようが*1必ず結果は項を作る。

そしてinversionはパターンマッチを作る。

だから怒られる。


inductionは実際には特定の関数をゴールに適用する。

しかし、その関数がパターンマッチを使うため、SetやTypeを返す関数が作成できない。

だから無理、と。


つまりは、根源はすべてパターンマッチができないことである、ということ。

*1:admitでもしない限り。

リンク元
Connection: close