小ネタです。 Abstract Rewriting Systemにおいて、「停止性と弱合流性(局所合流性)を持つ書き換え系は合流性を持つ」という定理があります*1。 この証明は、書き換え系の停止性から整礎帰納法を使って示すのが一般的です。 整礎帰納法はCoqでどうやるんだろ…

一年前くらいにCoqを触り始めて、Software FoundationやCPDTなどを読みながら細々とCoqの勉強を続けています。 Coqを使うための環境としては、CoqIDEやProofGeneralなどが有名ですが、 前者はUIが充実していなくて使いにくく、後者はEmacsなので普段Vimを使…

Coqやソフトウェア検証の入門書として知られるSoftware Foundation(以下SF)シリーズのvol.1，Logical Foundationを読むグループを学科で立ち上げて，3年生が始まる前の春休みに皆で読んでいた。3年生の前期が始まると忙しくて中断してしまったが，夏休みに入…