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

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

定義と、その展開

Coq入門 Definition Theorem Proof unfold reflexivity


Definitionコマンドを使って型や、関数を定義することができるが、証明の中で、定義に戻って展開したくなる時がある。

例えば次のような2足す関数を定義して、それを二回適用すると4になるような定理を証明したい場合を考える。

Welcome to Coq 8.1 (Feb. 2007)

Coq < Definition ss n := n + 2.
ss is defined

Coq < Theorem ssssO_is_four : ss (ss 0) = 4.
1 subgoal

  ============================
   ss (ss 0) = 4

ssssO_is_four < Proof.

ssssO_is_four <

これを証明するために ss を定義にしたがって展開したいなと思ったら、unfoldというタクティックが非常に便利である。

文法 : unfold [定義されたものの名前].

ためしにやってみよう。

ssssO_is_four < unfold ss.
1 subgoal

  ============================
   0 + 2 + 2 = 4

ssssO_is_four <

ssが展開されてプラスの形になったのがわかるだろう。
じゃあここでさらにプラスも展開してみよう '+' 記号によってあらわされるこれは、実は内部では plus 関数として扱うことができる。
この plus に関してunfoldをかけてみよう。

ssssO_is_four < unfold plus.
1 subgoal

  ============================
   4 = 4

ssssO_is_four <

じゃーん!
これで、示すべきゴールの形は大分シンプルな形になった。
ここで、 reflexivity タクティックを使うと、ゴールを示すことができる。
「ゴールがイコールの形ならば、reflexivityタクティックを使えばいい」、と覚えておこう。

ssssO_is_four < reflexivity.
Proof completed.

完成!!