Induction に悩む

この歳になって induction に悩まされるとは思っていなかった…(半分冗談

たぶん,というかやはり,induction on inductively defined binary relation がよくわかっていない. 非形式的には今までもこの帰納法は回したことがあるが,今回形式化しようとして初めて穴に気づいて辛い思いをしている.うーむ….

定理証明支援系って,巷で言われているような使い方が本格的になされるのはまだまだまだまだ先だろうと思っているけど,こういう形式的にやらないと気づかないレベルの穴に気づかせてくれる存在としてはすでに相当実用的だよねえ.