Ltacを知りcrushを読む - chiguriの生態（嘘や誇張アリ）

これはTheorem Proving Advent Calendarの15日目の記事である。 二回目じゃないのかって？人数不足だ。気にしてはいけない。 さて、今日の記事が何に関する記事かは見れば一目瞭然。 Coqの中のtactics記述用言語Ltacについてであり、目標はあの有名なcrushを読み解くことである。 ・・・と書いたが、正直まじめに説明すると長さの関係上やっていられないので、crushの動きを簡単に知る程度にする。 なお、今回もまた内容の関係上背景をあまり長くかけないので、一通りCoqの知識を持っているものとする。 それでも無理なのだからもはやどうしようもない。 crushって何？ 有名な、といっておきながらそれか、といわれそうだが、一応説明する。 crushというのは、Coqの初級者以上*1が読むと勉強になること請け合いの、Certified Programming with