Coqを勉強していたら、refineタクティクというものに出会った。一緒にSpecif moduleのsigの記述もあったので最初は混乱していたものの、何となく把握してきた。使い方は次のような感じ。 Definition pred (n : nat) : n>0 -> nat. refine (match n with | 0 …