Leanで証明を書くとはどういうことか、DFAの形式証明で見せる
Anatomy of a Lean proof for software engineers
Sipserの教科書の問題を題材に、LeanとMathlibで言語の正規性を形式証明した記録。最下位ビットから読む加算器DFAを構成し、反転の閉包性を使って元の言語の正規性を導く。型付き言語と帰納的証明に慣れたエンジニアなら追える構成で、システムの性質を機械的に証明する実際の流れが見えてくる。
もしDFAを構成してB^Rを認識できるなら、B^Rは正規言語だと結論できる。B^Rを反転したものがBなので、正規言語の反転の閉包性を使ってBも正規だと結論でき、これで解法が完成する。