補足：inversionやinduction

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


述語のdestructの話は、計算レベルで制限されている話で、問題になりやすいのはinversionやinductionだと思う（inductionはかなり稀か）。
「ゴールがSetやTypeに属する型であるときに、述語をinversionしたら怒られた」という経験がある人もいるだろう。
実はこれもまったく同じ原因である。
というのも、tacticは一般に関数や項を作るからだ。


introやapplyのように簡単なtacticは対応する項も割と簡単（関数抽象・関数適用）である。
一方、inversionは結構小難しいことをする。
しかし、小難しいことをしようが何をしようが*1必ず結果は項を作る。
そしてinversionはパターンマッチを作る。
だから怒られる。


inductionは実際には特定の関数をゴールに適用する。
しかし、その関数がパターンマッチを使うため、SetやTypeを返す関数が作成できない。
だから無理、と。


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

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