Theorem Prover Advent Calendar 2013 の21日目の記事です。 先月、信州大学で TPP 2013 という定理証明器ユーザの集会がありました。TPP では毎回証明の問題が事前に出題され、参加者の一部がこれを解いてきて発表するようになっています。これが TPPmark です。この記事は、TPPmark 2013 の SSReflect による解答例とその解説です。問題はhttp://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPPmark2013_Jap.pdfを参照してください。 これ以降の証明では以下のモジュールを使います。 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype path fingraph finset fingroup perm. 1
