Hatena::Groupcoq

mzpの日記

2010-06-26

Ex 3.1

Inductive truth := Yes | No | Maybe.

Definition not (t : truth) :=
  match t with
    | Yes => No
    | No  => Yes
    | Maybe => Maybe
  end.

Definition and (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,Yes) => Yes
    | (No,No) => No
    | _   => Maybe
  end.

Definition or (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,_)  => Yes
    | (_,Yes)  => Yes
    | (No,No)  => No
    | _ => Maybe
  end.

Lemma and_comm : forall (t1 t2 t3 : truth),
  and t1 (and t2 t3) = and (and t1 t2) t3.
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_r : forall (t1 t2 t3 : truth),
  and t1 (or t2 t3) = or (and t1 t2) (and t1 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_l : forall (t1 t2 t3 : truth),
  and (or t1 t2) t3 = or (and t1 t3) (and t2 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Ex 3.2

Inductive binop : Set :=
| Plus
| Times.

Definition var := nat.

Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp
| Var   : var   -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (assign : var -> nat) (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote assign e1) (expDenote assign e2)
    |  Var v  => assign v
  end.

Fixpoint const_fold (e : exp) : exp :=
  match e with
    | Binop b e1 e2 =>
      match (const_fold e1, const_fold e2) with
        | (Const x, Const y) => Const ((binopDenote b) x y)
        | (x,y) => Binop b x y
      end
    | _ => e
  end.

Theorem preserve : forall e assign,
  expDenote assign e = expDenote assign (const_fold e).
Proof.
intros.
induction e; simpl; try tauto.
rewrite IHe1, IHe2.
destruct (const_fold e1); destruct (const_fold e2); reflexivity.
Qed.

DannyApenoDannyApeno2017/06/20 22:43Attention Required! | Cloudflare
<a href=http://acheterdufrance.com/>Show more>>></a>

TimothyTeNTimothyTeN2017/07/01 23:47301 Moved Permanently
<a href=https://www.viagrapascherfr.com/>Click here>>></a>

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-25

Coqのおかげで見つけれたバグ

最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。

で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。

というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。

バグを含んだSubstitution

まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。

(* subst *)
Inductive Subst : term -> term -> string -> term -> Prop :=
  | SVar1    : forall (s x : string) (t : term),
      x = s  -> Subst (Var x) t s t
  | SVar2    : forall (s x : string) (t : term),
      x <> s -> Subst (Var x) (Var x) s t
  | SBool    : forall (s : string) (b : bool) (t : term),
      Subst (Bool b) (Bool b) s t
  | SLambda1 : forall (x s : string) (body1 body2 t : term) (ty : type),
      x <> s -> Subst body1 body2 s t ->
      	Subst (Lambda x ty body1) (Lambda x ty body2) s t
  | SLambda2 : forall (x s : string) (body t : term) (ty : type),
      x = s  -> Subst (Lambda x ty body) (Lambda x ty body) s t
  | SApply   : forall (t1 t2 s1 s2 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst (Apply t1 t2) (Apply s1 s2) x t
  | SIf      : forall (t1 t2 t3 s1 s2 s3 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst t3 s3 x t ->
      	Subst (If t1 t2 t3) (If s1 s2 s3) x t.

正しい定義

そして、こちらがTAPL(asin:0262162091)に載っている正しい定義です。

f:id:mzp:20091104203722p:image

間違っていたところ

で、どこが間違っていたかと言うとFV(s)に関する条件が抜けていました。これのせいで、substitutionが不正になって、結果としてSubstitution lemmaの証明ができませんでした。これが無いと、weaking Lemmaを適用できないんだよね。

f:id:mzp:20091104203904p:image

そのときのTwitterのログ

みずぴー
@mzp
えー、substitution lemma無理だって。これ成り立たねーよ(2009-11-03 19:00:54) link
みずぴー
@mzp
どう考えてもsubstitution lemmaの証明、無理だって。きっと"変数が重複しない"という約束のおかげで、暗黙の前提があるに違いない(2009-11-03 20:54:36) link
みずぴー
@mzp
一晩一晩考えたけsubstitution lemmaが成立しない、ってのはウソな気がしてきた(←当然)。でも、証明ができないってのは依然とそのまま(2009-11-4 08:00:48) link
みずぴー
@mzp
そろそろでかける時間だけど、もうちょっとTAPLの証明を追いかけたいし、iPhoneの同期も終ってないので、まだ家にいる(2009-11-4 08:02:22) link
みずぴー
@mzp
あーーーー、証明できない理由がわかった。substitutionの定義が間違ってるんだ!!(2009-11-4 08:10:17) link
みずぴー
@mzp
TAPLだと「λx.t」のxは常にユニークである、という約束のおかげで、substitutionの定義が簡単になってるのか(2009-11-4 08:11:07) link
みずぴー
@mzp
ん?そんなこともないか。単にボクの実装ミスだ > substitutionの定義(2009-11-4 08:15:16) link
みずぴー
@mzp
今のボクの状態: substitution lemmaの証明ができない-> よく見たらsubstitutionの定義が間違っていた -> ちゃんとsubstitutionを定義するのが難しい! http://github.com/mzp/lambda(2009-11-04 09:51:20) link

ちなみに

書いているCoqのコードはGitHubにあります。

http://github.com/mzp/lambda

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を使ってやれば証明できます。

 (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.