さらに Coq

朝6時ごろ起床.

朝は線形代数のお話を聞く.絶賛 Coq に没頭中なので,かなり細かいところばかりに目がいってしまいよろしくない.が,まあ 1 年生相手だったらちょっとうるさいぐらい論理の訓練をしてもらった方が良いだろうということで許してほしい.

んで,第三リスト準同型定理というのがあって,それを形式化した.第三リスト準同型定理というのが面白くて,foldl でもかけるし foldr でも書ける関数は homomorphism であるという話だ.日本語の解説は,まあ拙記事でよろしければ以下の記事がある.

qiita.com

んで,これを Coq で形式化したいのであるが,補題1つをのぞいてうまくいった.うまくいかない補題というのは,拙記事の補題2にあたるものだが,これはまあ真面目にやると「帰納的可算」あたりの形式化が超難しいだろうし,さらに元論文の merge sort の導出だって補題2を使わず具体的に  h を与えているので実用的に重要というわけでもなし,ということで仕方あるまいという気がする.