(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。 そんなときは、Show Scriptコマンドで整形すると…