Hatena::ブログ(Diary)

言語ゲーム このページをアンテナに追加 RSSフィード Twitter

とあるエンジニアが嘘ばかり書く日記
ホームページ | blog | twitter

2009-02-20

[] Coq で遊ぶその7: 等式と repeat

なんか Coq の事ばかり書くとどんどん日記のアクセス数が落ちて行く。。。ま、いいか。とりあえず Coq の型システムの勉強したいんだけど、その前提知識が沢山あるので仕方なく細かい部分をやっています。ただ、今まで勉強した事はどれも最初すごく難しく感じるけど、難しさ度で言うと中学生レベルです。微分積分とかに比べてよっぽど簡単。この文章が読みにくいのは私が阿呆なせいです。今日はちょっと数学らしく等式と repeat で遊んでみます。

reflexivity: 等式を証明する

数学で等式と言うと真っ先に出てくるもんですが、Coq では不思議と脇役扱いで、代わりに大活躍してるのが論理包含 -> (○なら△)と簡約(式を計算して簡単にする)でした。学校で習う簡約(計算)は等式を使って説明されますが、Coq の世界では簡約の方が等式より先みたいです。この辺は不思議な話が沢山ありそうだけど、あまりこだわらないで進みます。例えば 7 = 7 を証明します。

Coq < Lemma l7eq7 : 7 = 7 (* Lemma は Theorem コマンドの別名 *).
1 subgoal
  
  ============================
   7 = 7

こんなの当たり前すぎて証明しようが無い気もしますが、念のため = の定義を探って行きます。

Coq < Locate "_ = _".
Notation            Scope     
"x = y" := eq x y    : type_scope
                      (default interpretation)

Coq < Print eq.
Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x

Coq < Check refl_equal.
refl_equal
     : forall (A : Type) (x : A), x = x

この Inductive の意味は置いといて、どうも refl_equal という定理がマッチする気がします。

l7eq7 < apply refl_equal.
Proof completed.

l7eq7 < Qed.

という事でめでたく証明出来ました。ちなみに、apply refl_equal はよく使うので reflexivity という別コマンドが割り当てられているそうです。

rewrite: 等式を使ってゴールを書き換える。

さて、今度はちょっと難しく a = b -> b = a (a = b ならば b = a) をやってみます。rewrite コマンドを使うと、前提にある等式の左辺を右辺で置き換える形でゴールを書き換えます。逆に右辺を左辺で置き換えるには rewrite <- コマンドを使います。

Coq < Theorem eq_sym : forall (A : Type) (a b : A), a = b -> b = a.
1 subgoal
  
  ============================
   forall (A : Type) (a b : A), a = b -> b = a

eq_sym < intros A a b e.
1 subgoal
  
  A : Type
  a : A
  b : A
  e : a = b
  ============================
   b = a

eq_sym < rewrite e (* 前提にある e : a = b を使って
ゴールの a = b を b = b に変換するには rewrite コマンドを使う *).
1 subgoal
  
  A : Type
  a : A
  b : A
  e : a = b
  ============================
   b = b

eq_sym < reflexivity.
Proof completed.

eq_sym < Qed.

ライブラリにある定理の等式を使う

今度はちょっと難しく x * y + y = (x + 1) * y を証明してみます。これくらい複雑なのを証明するにはライブラリを使います。

Coq < Require Import Arith.

Coq < Theorem mult_distr_1 : forall x y: nat, x * y + y = (x + 1) * y.
1 subgoal
  
  ============================
   forall x y : nat, x * y + y = (x + 1) * y

mult_distr_1 < intros x y.
1 subgoal
  
  x : nat
  y : nat
  ============================
   x * y + y = (x + 1) * y

Arith ライブラリには沢山の便利な定理が入っています。欲しい定理を探すには _ をワイルドカードとして使って次のように SearchPattern を使います。

mult_distr_1 < SearchPattern ((_ + _) * _ = _).
mult_plus_distr_r: forall n m p : nat, (n + m) * p = n * p + m * p

mult_distr_1 < rewrite mult_plus_distr_r (* 上で探した定理を使う *).
1 subgoal
  
  x : nat
  y : nat
  ============================
   x * y + y = x * y + 1 * y

ここまで来るとあと一息です。1 * y の部分を同じように書き換えます。

mult_distr_1 < SearchPattern (1 * _ = _).
mult_1_l: forall n : nat, 1 * n = n

mult_distr_1 < rewrite mult_1_l.
1 subgoal
  
  x : nat
  y : nat
  ============================
   x * y + y = x * y + y

mult_distr_1 < reflexivity.
Proof completed.

mult_distr_1 < Qed.

pattern: ゴールの一部だけを書き換える。

次にゴールの一部だけを書き換える方法をやります。例えば x + x + x + x + x = 5 * x を証明する事を考えます。

  • x + x + x + x + x = 5 * x :: これを証明するには
  • (1 * x) + x + x + x + x = 5 * x :: 最初の x だけを 1 * x に変える (mult_1_l 使用)。
  • (1 + 1) * x + x + x + x = 5 * x :: 先ほど証明した mult_distr_1 を使ってかけ算をたし算に変える。
  • (1 + 1 + 1 + 1 + 1) * x = 5 * x :: 繰り返す。
  • 5 * x = 5 * x :: 簡約

この、「ゴールの 1 番目の x だけを書き換えますよ」と言うのに pattern x at 1 というコマンドを使います。実行後ゴールが激しく醜いλ表示になりますが、あまりそこは気にしないで良いと思います。ではやってみましょう。


Coq < Theorem regroup : forall x : nat, x + x + x + x + x = 5 * x.
1 subgoal
  
  ============================
   forall x : nat, x + x + x + x + x = 5 * x

regroup < intro x.
1 subgoal
  
  x : nat
  ============================
   x + x + x + x + x = 5 * x

regroup < pattern x at 1
(* 最初の x だけを rewrite 対象に、表示が醜くなるが気にしない *).
1 subgoal
  
  x : nat
  ============================
   (fun n : nat => n + x + x + x + x = 5 * x) x

regroup < rewrite <- mult_1_l.
(* mult_1_l: forall n : nat, 1 * n = n の右を左に書き換える *).

1 subgoal
  
  x : nat
  ============================
   1 * x + x + x + x + x = 5 * x

regroup < rewrite mult_distr_1
(* mult_distr_1 : forall x y : nat, x * y + y = (x + 1) * y を左を右に書き換え *).
1 subgoal
  
  x : nat
  ============================
   (1 + 1) * x + x + x + x = 5 * x

regroup < repeat rewrite mult_distr_1 (* repeat を使うと連続 rewrite *).
1 subgoal
  
  x : nat
  ============================
   (1 + 1 + 1 + 1 + 1) * x = 5 * x

regroup < reflexivity (* ここまで来ると簡約して証明完了 *).
Proof completed.

regroup < Qed.

こんなに単純な式に結構難しいもんです。ではおつかれさまです。


カレンダー
<< 2009/02 >>
1 2 3 4 5 6 7
8 9 10 11 12 13 14
15 16 17 18 19 20 21
22 23 24 25 26 27 28
最新コメント一覧