読者です 読者をやめる 読者になる 読者になる

refineの例

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に簡単に紹介されている。

広告を非表示にする