Coqを勉強していたら、refineタクティクというものに出会った。
一緒にSpecif moduleのsigの記述もあったので最初は混乱していたものの、何となく把握してきた。
使い方は次のような感じ。
Definition pred (n : nat) : n>0 -> nat. refine (match n with | 0 => _ | S m => (fun _ => m) end). auto. Qed. Definition example_refine: forall (n : nat), {m : nat | m = S n}. refine (fun n => exist _ (S n) _). reflexivity. Qed.
refineタクティクはゴールと同じ型を持つものを証明として与えるものらしい。
ただ与えるものにはプレースホルダ（_）があってもよくて、プレースホルダを与えるためのサブゴールが自動的に生成されるらしい。
ちなみに二番目の証明は
Definition example_refine: forall (n : nat), {m : nat | m = S n}. refine (fun n => exist _ _ _).
のようにexistにあたえるものすべてをプレースホルダにしても同じように証明できるみたい。多分
?678 = S n
とかいうサブゴールがでて、「何じゃこりゃ？」という感じになるとは思うけど。
さらにちなみに、existや{m : nat | m = S n}のような記述の説明については、http://coq.inria.fr/doc/Reference-Manual005.html#specif-syntaxに簡単に紹介されている。
