定義と、その展開

Coq入門 Definition Theorem Proof unfold reflexivity


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

例えば次のような２足す関数を定義して、それを二回適用すると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.

完成！！