CoqのProgram機構の紹介 〜型を活用した安全なプログラミング〜 by Hiroki Tokunaga

Coqには、証明付きプログラミングを容易にする Program 機構があります。本LTでは、この Program 機構の概要とその利用例を紹介します。

この機能を紹介する題材として、インデックスを用いたリストの要素取得を取り上げます。Coq において、指定したインデックスにあるリストの要素を取得する場合、通常は option 型を返すか、指定したインデックスに要素がない場合に備えて、あらかじめデフォルト値を渡す必要があります。しかし、指定したインデックスがリストの長さ未満ならば、毎回 Some が返ってくることは明らかです。

本LTでは、Program 機構を活用し、インデックスがリストの長さ未満であることが前提の場合に、option 型を用いず、またデフォルト値を与えることなくリストの要素を取得できることを紹介します。「Coqにこんな機能があるのか！」と興味を持ってもらえたら幸いです。