言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella
トップ > coq > Coq で遊ぶその6: unfold

Coq で遊ぶその6: unfold

coq

本でもマニュアルでも大変分かりずらく解説されてある unfold を使ってみます。関数を使うという意味で unfold は apply となんだか良く似ています。

  • unfold はゴールの中の関数名を定義で置き換えます。
  • apply は前提の関数型 A->B の B がゴールにマッチする時、ゴールを A に書き換えます。

例題は本と同じ forall n p:nat, n < p -> n < S p にコメントを付けて行きます。命題の意味は、二つの自然数 n p が n < p の時 n < p + 1 という事です。

$ coqtop
Welcome to Coq 8.1pl3 (Dec. 2007)

Coq < Theorem lt_S : forall n p:nat, n < p -> n < S p.
1 subgoal
  
  ============================
   forall n p : nat, n < p -> n < S p

lt_S < intros n p H.
1 subgoal
  
  n : nat
  p : nat
  H : n < p
  ============================
   n < S p

Coq を起動して命題を入力します。forall や -> の左側の式は intro を使うと前提として証明に使う事が出来ます。次が問題なんですけど、< の付いた式について、ここから先どうすれば良いのか分かりません。そこで、< の定義を当たってみます。

lt_S < Locate "_ < _".
Notation            Scope     
"x < y" := lt x y    : nat_scope
                      (default interpretation)

lt_S < Print lt.
lt = fun n m : nat => S n <= m
     : nat -> nat -> Prop

Locate を使うと、< の本当の名前は lt である事が分かります。アンダーライン "_" で引数の位置を指定しています。さらに Print を使って、lt の定義がどうなっているのかを調べると、lt は <= を使って定義されている事が分かりました。<= に直すと証明に近づく事を期待して書き換えてみましょう。関数定義を使ってゴールを書き換えるコマンドを unfold と言います。

lt_S < unfold lt.
1 subgoal
  
  n : nat
  p : nat
  H : n < p
  ============================
   S n <= S p

分かりづらいですが、ここでは以下の変換が行われています。

  • n < S p : 元のゴール
  • lt n (S p) : わかりやすく前値記法に変えてみた。
  • (fun n m : nat => S n <= m) n (S p) : lt を定義で置き換え。こういうのをδ(delta) 簡約と言います。
  • S n <= S p : 関数適用。n := n, m := S p に代入。こういうのをβ(beta) 簡約と言います。

さて、今度はゴールに <= が残ったので今度は <= の定義を探します。

lt_S < Locate "_ <= _".
Notation            Scope     
"n <= m" := le n m   : nat_scope
                      (default interpretation)

lt_S < Print le.
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

<= の本名である le は、le_n と le_S の二つの式で定義されています。このうち、le_S : forall m : nat, n <= m -> n <= S m の意味は

  • n <= m ならば n <= m + 1 である

という意味ですが、証明の時には右から左に考えて

  • n <= m + 1 を証明する為には n <= m を証明すれば良い

という風に考える事も出来るので、これを使ってゴールを書き換えます(apply コマンド)。現在のゴールの S n <= S p (意味は n + 1 <= p + 1) は右辺にマッチするので使ってみます。

lt_S < apply le_S.
1 subgoal
  
  n : nat
  p : nat
  H : n < p
  ============================
   S n <= p

これでゴールの S が一つ取れました。ここでゴールをよく見ると、どこかで見た事のある形です。先ほどの unfold で使った lt = fun n m : nat => S n <= m の右辺とマッチします。このルールを使って前提の H : n < p を書き換える(δ簡約する)となんとゴールとぴったんこ S n <= p になります。前提の簡約は勝手に行われる事になっているので H を apply します。

lt_S < apply H.
Proof completed.

lt_S < Qed.
intros n p H.
unfold lt in |- *.
apply le_S.
apply H.
lt_S is defined

Coq < Print lt_S.
lt_S = 
fun (n p : nat) (H : n < p) => le_S (S n) p H
     : forall n p : nat, n < p -> n < S p

はいおつかれさまでした。