Coqで健全性と完全性の証明をしたよ

Coqでラムダ計算を証明してみた - みずぴー日記の続けて、単純型付きラムダ計算の型推論(Type reconstruction)に関する定理の証明をしてました。

そして、とうとう健全性と完全性の証明ができました! やったね!

• GitHub - mzp/lambda at c0123fd0ca42d545f9e459e89c5ba67d6cc3c41b

ただ、完全性の証明が1000行を越えてしまったので、今がんばってリファクタリングしてます。似たような証明を何度もした気がするので、きっと短かくなります。