Hatena::Groupcoq

mzpの日記

2009-12-05

Coq + omake =さいきょう

coqcで複数ファイルをコンパイルするのって面倒ですよね。依存関係も考慮しないといけないし。

そんなときは、omakeですね!

というわけで、Coqのソースコードをコンパイルするのに必要なルールをいくつか書きました。

A.v、B.v、C.vからなる証明をコンパイルしたいときは

.DEFAULT: $(Proof A B C)

とするだけでOKです。ちゃんとA.v、B.v、C.vの間の依存関係も解析してます。

あと、omakeなので当然omake -Pで継続ビルドもできちゃいます。

ソースコード

s# ------------------------------------------------------------
# ルール部
# ------------------------------------------------------------
# コンパイル
%.vo %.glob: %.v
	coqc $<

# 依存関係の解析
# パスは適宜変更してください
.SCANNER: %.vo: %.v
	coqdep -w -coqlib /opt/local/lib/coq/ -I . $<

# 便利関数
public.Proof(files) =
	vo=$(addsuffix .vo,$(files))
	value $(vo)

# ------------------------------------------------------------
# 利用例:
# A.v B.v C.vをコンパイルしたい場合
# ------------------------------------------------------------
FILES[] =
	A
	B
	C

.DEFAULT: $(Proof $(FILES))

.PHONY: clean
clean:
	rm -f *.vo *.glob *~ *.omc .omakedb .omakedb.lock *.html

参考

The OMake build system

2009-11-26

Coqでラムダ計算を証明してみた

f:id:mzp:20091122200215j:image

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。

動機

  • let多相の実装はしたから、次は証明だろ
  • 最近、流行っているCoqを覚えたい

扱えるラムダ式

型は、Bool型と関数型のみ。

Inductive type : Set :=
  | BoolT : type
  | FunT  : type -> type -> type.

式は、変数参照、真偽値、ラムダ(関数抽象)、関数適用、if式。

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

証明した定理

型が付くなら、それは値か評価できるかのどちらか。

Theorem Progress : forall t r,
  Typed t empty_env r -> Value t \/ (exists t', Eval t t').

評価しても型は代わらない。

Theorem preservation: forall t t' tenv T,
  Typed t tenv T -> Eval t t' -> Typed t' tenv T.

あと、これを証明するのに必要な補題を何個か証明しています。

ソースコード

詳しい証明のついたソースコードはgithubにあります。

http://github.com/mzp/lambda/tree/simple-typed

参考文献

Types and Programming Languages (MIT Press)

Types and Programming Languages (MIT Press)

元ネタ。

Coqの本。Coqの中の話がメインらしいですが、ボクはタクティクスの利用例集としてぐらいしか、使えていません。

プログラミング言語の基礎理論 (情報数学講座)

プログラミング言語の基礎理論 (情報数学講座)

TAPLで納得できないところは、こっちで確認してました。特に、変数束縛が発生する場合のsubstitutionの定義でお世話になりました。

日本語なのにTAPLより難しく感じました。

絶版していて手にいれれなかったので、図書館で借りてコピーしました。

感想

  • straightforwardはやめてください。難しいよ、その証明(><)
  • 一発で正しい定義はなかなかできない。(id:mzp:20091124)
  • さらっと「変数は重複して登場しないものとする」って書かないで! 難しいよ、その証明(><)

2009-11-24

今日のCoq: InductiveなProp

定理の中で使うProp(命題)は、関数的に定義するよりも、Inductiveに定義したほうが証明が楽らしいですよ。

要約

  • Inductiveに定義したPropのほうが使いやすいらしい
  • Inductiveに定義したPropの各名前は、applyできる
  • Inductive Xを定義するとX_indが自動で定義される

前提

こんな簡単なラムダ式があると思ってください。

Inductive type : Set :=
    BoolT : type
  | FunT  : type -> type -> type.

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

Definition is_value (t : term) :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      true
  | Apply _ _  | If _ _ _ =>
      false
  end.

ダメなPropの例

true/falseを返すかわりに、True/Falseを返すだけのやつ。

Definition value (t : term) : Prop :=
  match t with
    Var _   | Bool _  | Lambda _ _ _ =>
      True
  | Apply _ _  | If _ _ _ =>
      False
  end.

イイPropの例

値とは何かを、帰納的(Inductive)に定義している。

Inductive Value  : term -> Prop :=
  | ValVar    : forall s : string, Value (Var s)
  | ValBool   : forall b : bool,   Value (Bool b)
  | ValLambda : forall (x : string) (ty : type) (body : term), Value (Lambda x ty body).

ここで与えたValVarとかいう名前は証明するときに使うので、覚えやすいのにするといいでしょう。

じゃあ、これを使って証明してみよう!(その1)

試しに、こんなんを証明してみましょう。

Theorem is_value_is_Value :
  forall t : term, is_value t = true -> Value t.

ようするに、is_value関数が正しく定義されているか証明したいわけです。

まずは、tについて場合分けします。Inductiveに定義されたデータ型は、inductionを使うよりdestructを使って場合分けしたほうがいいらしいです。

is_value_is_Value < destruct t.
5 subgoals

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

Value (Var s)が登場するまで、適当にintroを使ってやります。

is_value_is_Value < Show 1.

  s : string
  ============================
   is_value (Var s) = true -> Value (Var s)

is_value_is_Value < intro.
5 subgoals

  s : string
  H : is_value (Var s) = true
  ============================
   Value (Var s)

subgoal 2 is:
 is_value (Bool b) = true -> Value (Bool b)
subgoal 3 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 4 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 5 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ここで、さっき定義したValVarが使えます。

is_value_is_Value < Check ValVar.
ValVar
     : forall s : string, Value (Var s)

というわけで、これをapplyすれば証明が完了します。

is_value_is_Value < apply ValVar.
4 subgoals

  b : bool
  ============================
   is_value (Bool b) = true -> Value (Bool b)

subgoal 2 is:
 is_value (Lambda s t t0) = true -> Value (Lambda s t t0)
subgoal 3 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 4 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

あとは、BoolとLambdaについても同様に証明できます。

is_value_is_Value < intro; apply ValBool.
3 subgoals

  s : string
  t : type
  t0 : term
  ============================
   is_value (Lambda s t t0) = true -> Value (Lambda s t t0)

subgoal 2 is:
 is_value (Apply t1 t2) = true -> Value (Apply t1 t2)
subgoal 3 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro; apply ValLambda.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

ApplyとIfについては、simplで簡約すると前提がFalseになります。これをintroで仮定に移動させて、discriminateを使ってやれば証明できます。

is_value_is_Value < Show.
2 subgoals

  t1 : term
  t2 : term
  ============================
   is_value (Apply t1 t2) = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl.
2 subgoals

  t1 : term
  t2 : term
  ============================
   false = true -> Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < intro.
2 subgoals

  t1 : term
  t2 : term
  H : false = true
  ============================
   Value (Apply t1 t2)

subgoal 2 is:
 is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < discriminate.
1 subgoal

  t1 : term
  t2 : term
  t3 : term
  ============================
   is_value (If t1 t2 t3) = true -> Value (If t1 t2 t3)

is_value_is_Value < simpl;intro; discriminate.
Proof completed.

じゃあ、これを使って証明してみよう!(その2)

じゃあ、逆向きも証明してみましょう。

Theorem Value_is_value :
  forall t : term, Value t -> is_value t = true.

で、これをtについて場合分けしても全然ハッピーになりません。

Inductiveで何かを定義した場合には、xxx_indが自動で定義されます。

Value_is_value < Check Value_ind.
Value_ind
     : forall P : term -> Prop,
       (forall s : string, P (Var s)) ->
       (forall b : bool, P (Bool b)) ->
       (forall (x : string) (ty : type) (body : term), P (Lambda x ty body)) ->
       forall t : term, Value t -> P t

これをapplyすると、いい感じのsubgoalがでてきます。あとはreflexivityだけで証明でいます。

Value_is_value < apply Value_ind.
3 subgoals

  ============================
   forall s : string, is_value (Var s) = true

subgoal 2 is:
 forall b : bool, is_value (Bool b) = true
subgoal 3 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true
Value_is_value < reflexivity.
2 subgoals

  ============================
   forall b : bool, is_value (Bool b) = true

subgoal 2 is:
 forall (x : string) (ty : type) (body : term),
 is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
1 subgoal

  ============================
   forall (x : string) (ty : type) (body : term),
   is_value (Lambda x ty body) = true

Value_is_value < reflexivity.
Proof completed.

2009-11-23

今日の証明: reverse (reverse xs) = xs

最近Coqが流行してるので、ボクも流れに乗ってみました。

今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。

Theorem RevReflect :
  forall {A : Type} {xs : list A},
  reverse (reverse xs) = xs.

そののために、appendを定義したり、Lemmaを証明したりしてます。

状況に応じて、TheoremやLemma、Fact、Remark、Corollary、Propositionを使い分けるのがクールらしいですよ。参考

あとReverseAppendを証明するときは、全部introsしちゃうのじゃなくて、xを残しとくという覚えたてのテクニックを使ってます。引数の順番大事!

Require Import List.

Fixpoint append {A : Type} (xs : list A) (ys : list A) :=
  match xs with
    | nil => ys
    | x::xs => x :: (append xs ys)
  end.

(* append を演算子に *)
Infix "+++" := append (at level 50).

Fixpoint reverse {A : Type} (xs : list A) :=
  match xs with
  | nil   => nil
  | x::xs => (reverse xs) +++ (x::nil)
  end.

Lemma ReverseAppend {A : Type} (xs : list A) (x : A) :
  reverse (xs +++ (x::nil)) = x::(reverse xs).
Proof.
intros A xs.
induction xs.
 reflexivity.

 intros.
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
Qed.

Theorem RevReflect :
  forall {A : Type} {xs : list A},
  reverse (reverse xs) = xs.
Proof.
intros.
induction xs.
 reflexivity.

 simpl in |- *.
 rewrite ReverseAppend in |- *.
 rewrite IHxs in |- *.
 reflexivity.
Qed.