なんか 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.
こんなに単純な式に結構難しいもんです。ではおつかれさまです。
